diff --git a/sledge/TODO.org b/sledge/TODO.org index c382a04ed..4b77e1c78 100644 --- a/sledge/TODO.org +++ b/sledge/TODO.org @@ -23,7 +23,6 @@ and sort terms ** ? remove src typ from Convert ** ? distribute addition over multiplication for e.g. ((%12 + 1) * 8) to ((%12 * 8) + 8) -** ? conflate null and 0 ** add config to pp e.g. Exp.t as sexps ** add check for variable non-occurrence to Exp.rename ** define version of map that transforms args of Struct_rec diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml index 13179fbd1..ef1ecb068 100644 --- a/sledge/src/llair/exp.ml +++ b/sledge/src/llair/exp.ml @@ -71,7 +71,6 @@ module T0 = struct | Label of {parent: string; name: string} | App of {op: t; arg: t} (* pointer and memory constants and operations *) - | Null | Splat | Memory | Concat @@ -161,7 +160,7 @@ module T = struct | Var {name; id} -> pf "%%%s_%d" name id | Nondet {msg} -> pf "nondet \"%s\"" msg | Label {name} -> pf "%s" name - | Null -> pf "null" + | Integer {data; typ= Pointer _} when Z.equal Z.zero data -> pf "null" | Splat -> pf "^" | Memory -> pf "⟨_,_⟩" | App {op= App {op= Memory; arg= siz}; arg= bytes} -> @@ -262,8 +261,7 @@ let invariant ?(partial = false) e = | Integer {data; typ= Integer {bits}} -> assert_arity 0 ; assert (Z.numbits data <= bits) - | Var _ | Nondet _ | Label _ | Null | Integer _ | Float _ -> - assert_arity 0 + | Var _ | Nondet _ | Label _ | Integer _ | Float _ -> assert_arity 0 | Convert {dst; src} -> ( match args with | [Integer {typ}] -> assert (Typ.equal src typ) @@ -441,8 +439,8 @@ let fv e = fold_vars e ~f:Set.add ~init:Var.Set.empty let var x = x let nondet msg = Nondet {msg} |> check invariant let label ~parent ~name = Label {parent; name} |> check invariant -let null = Null |> check invariant let integer data typ = Integer {data; typ} |> check invariant +let null = integer Z.zero Typ.ptr let bool b = integer (Z.of_bool b) Typ.bool let float data = Float {data} |> check invariant @@ -846,7 +844,7 @@ let update ~rcd ~elt ~idx = app3 Update rcd elt idx let struct_rec key = let memo_id = Hashtbl.create key in - let dummy = Null in + let dummy = null in Staged.stage @@ fun ~id elt_thks -> match Hashtbl.find memo_id id with diff --git a/sledge/src/llair/exp.mli b/sledge/src/llair/exp.mli index e1eb61159..e490fe51f 100644 --- a/sledge/src/llair/exp.mli +++ b/sledge/src/llair/exp.mli @@ -30,11 +30,12 @@ type t = private (** Address of named code block within parent function *) | App of {op: t; arg: t} (** Application of function symbol to argument, curried *) - | Null (** Pointer value that never refers to an object *) | Splat (** Iterated concatenation of a single byte *) | Memory (** Size-tagged byte-array *) | Concat (** Byte-array concatenation *) - | Integer of {data: Z.t; typ: Typ.t} (** Integer constant *) + | Integer of {data: Z.t; typ: Typ.t} + (** Integer constant, or if [typ] is a [Pointer], null pointer value + that never refers to an object *) | Float of {data: string} (** Floating-point constant *) | Eq (** Equal test *) | Dq (** Disequal test *) diff --git a/sledge/src/llair/typ.ml b/sledge/src/llair/typ.ml index 1f43fafee..53da05688 100644 --- a/sledge/src/llair/typ.ml +++ b/sledge/src/llair/typ.ml @@ -104,6 +104,7 @@ let struct_ = let bool = integer ~bits:1 let siz = integer ~bits:64 +let ptr = pointer ~elt:(integer ~bits:8) (** Queries *) diff --git a/sledge/src/llair/typ.mli b/sledge/src/llair/typ.mli index 27d9c74f5..a321b928d 100644 --- a/sledge/src/llair/typ.mli +++ b/sledge/src/llair/typ.mli @@ -36,6 +36,7 @@ include Invariant.S with type t := t val bool : t val siz : t +val ptr : t val function_ : return:t option -> args:t vector -> t val integer : bits:int -> t val float : bits:int -> enc:[`Extended | `IEEE | `Pair] -> t