[sledge] Represent null pointer as zero integer of pointer type

Reviewed By: mbouaziz

Differential Revision: D12854505

fbshipit-source-id: c1467c937

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

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 _ ->
+  | Var _ | Nondet _ | Label _ | Integer _ | Float _ -> assert_arity 0
-      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

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 *)

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 *)
 

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