Add new Loc expression to model abstract locations (#382)

Author: filipeom

src/smtml/dune

@@ -28,6 +28,7 @@
   interpret
   interpret_intf
   lexer
+  loc
   log
   logic
   mappings

src/smtml/expr.ml

@@ -10,6 +10,7 @@ and expr =
       { base : Bitvector.t
       ; offset : t
       }
+  | Loc of Loc.t
   | Symbol of Symbol.t
   | List of t list
   | App of Symbol.t * t list
@@ -33,6 +34,7 @@ module Expr = struct
   let equal (e1 : expr) (e2 : expr) : bool =
     match (e1, e2) with
     | Val v1, Val v2 -> Value.equal v1 v2
+    | Loc a, Loc b -> Loc.compare a b = 0
     | Ptr { base = b1; offset = o1 }, Ptr { base = b2; offset = o2 } ->
       Bitvector.equal b1 b2 && phys_equal o1 o2
     | Symbol s1, Symbol s2 -> Symbol.equal s1 s2
@@ -58,8 +60,9 @@ module Expr = struct
     | Concat (e1, e3), Concat (e2, e4) -> phys_equal e1 e2 && phys_equal e3 e4
     | Binder (binder1, vars1, e1), Binder (binder2, vars2, e2) ->
       Binder.equal binder1 binder2 && list_eq vars1 vars2 && phys_equal e1 e2
-    | ( ( Val _ | Ptr _ | Symbol _ | List _ | App _ | Unop _ | Binop _ | Triop _
-        | Relop _ | Cvtop _ | Naryop _ | Extract _ | Concat _ | Binder _ )
+    | ( ( Val _ | Ptr _ | Loc _ | Symbol _ | List _ | App _ | Unop _ | Binop _
+        | Triop _ | Relop _ | Cvtop _ | Naryop _ | Extract _ | Concat _
+        | Binder _ )
       , _ ) ->
       false
 
@@ -68,6 +71,7 @@ module Expr = struct
     match e with
     | Val v -> h v
     | Ptr { base; offset } -> h (base, offset.tag)
+    | Loc l -> h l
     | Symbol s -> h s
     | List v -> h v
     | App (x, es) -> h (x, es)
@@ -107,6 +111,7 @@ let rec ty (hte : t) : Ty.t =
   match view hte with
   | Val x -> Value.type_of x
   | Ptr _ -> Ty_bitv 32
+  | Loc _ -> Ty_app
   | Symbol x -> Symbol.type_of x
   | List _ -> Ty_list
   | App (sym, _) -> begin match sym.ty with Ty_none -> Ty_app | ty -> ty end
@@ -135,6 +140,7 @@ let rec is_symbolic (v : t) : bool =
   match view v with
   | Val _ -> false
   | Symbol _ -> true
+  | Loc _ -> false
   | Ptr { offset; _ } -> is_symbolic offset
   | List vs -> List.exists is_symbolic vs
   | App (_, vs) -> List.exists is_symbolic vs
@@ -153,7 +159,7 @@ let get_symbols (hte : t list) =
   let tbl = Hashtbl.create 64 in
   let rec symbols (hte : t) =
     match view hte with
-    | Val _ -> ()
+    | Val _ | Loc _ -> ()
     | Ptr { offset; _ } -> symbols offset
     | Symbol s -> Hashtbl.replace tbl s ()
     | List es -> List.iter symbols es
@@ -186,6 +192,7 @@ let rec pp fmt (hte : t) =
   match view hte with
   | Val v -> Value.pp fmt v
   | Ptr { base; offset } -> Fmt.pf fmt "(Ptr %a %a)" Bitvector.pp base pp offset
+  | Loc l -> Fmt.pf fmt "(loc %a)" Loc.pp l
   | Symbol s -> Fmt.pf fmt "@[<hov 1>%a@]" Symbol.pp s
   | List v -> Fmt.pf fmt "@[<hov 1>[%a]@]" (Fmt.list ~sep:Fmt.comma pp) v
   | App (s, v) ->
@@ -247,7 +254,7 @@ module Set = struct
     let tbl = Hashtbl.create 64 in
     let rec symbols hte =
       match view hte with
-      | Val _ -> ()
+      | Val _ | Loc _ -> ()
       | Ptr { offset; _ } -> symbols offset
       | Symbol s -> Hashtbl.replace tbl s ()
       | List es -> List.iter symbols es
@@ -281,6 +288,8 @@ let value (v : Value.t) : t = make (Val v) [@@inline]
 
 let ptr base offset = make (Ptr { base = Bitvector.of_int32 base; offset })
 
+let loc l = make (Loc l)
+
 let list l = make (List l)
 
 let app symbol args = make (App (symbol, args))
@@ -574,7 +583,7 @@ let rec concat (msb : t) (lsb : t) : t =
 
 let rec simplify_expr ?(in_relop = false) (hte : t) : t =
   match view hte with
-  | Val _ | Symbol _ -> hte
+  | Val _ | Symbol _ | Loc _ -> hte
   | Ptr { base; offset } ->
     let offset = simplify_expr ~in_relop offset in
     if not in_relop then make (Ptr { base; offset })

src/smtml/expr.mli

@@ -20,6 +20,7 @@ and expr = private
       { base : Bitvector.t  (** Base address. *)
       ; offset : t  (** Offset from base. *)
       }
+  | Loc of Loc.t  (** Abstract location *)
   | Symbol of Symbol.t  (** A symbolic variable. *)
   | List of t list  (** A list of expressions. *)
   | App of Symbol.t * t list  (** Function application. *)
@@ -90,6 +91,9 @@ val value : Value.t -> t
     address and offset. *)
 val ptr : int32 -> t -> t
 
+(** [loc l] constructs an abstract location *)
+val loc : Loc.t -> t
+
 (** [list l] constructs a list expression with the given list of expressions *)
 val list : t list -> t
 

src/smtml/expr_raw.ml

@@ -9,6 +9,7 @@ include (
             { base : Bitvector.t
             ; offset : t
             }
+        | Loc of Loc.t
         | Symbol of Symbol.t
         | List of t list
         | App of Symbol.t * t list
@@ -50,6 +51,8 @@ include (
 
       val ptr : int32 -> t -> t
 
+      val loc : Loc.t -> t
+
       val list : t list -> t
 
       val symbol : Symbol.t -> t

src/smtml/expr_raw.mli

@@ -16,6 +16,7 @@ and expr = private
       { base : Bitvector.t  (** Base address. *)
       ; offset : t  (** Offset from base. *)
       }
+  | Loc of Loc.t  (** Abstract location *)
   | Symbol of Symbol.t  (** A symbolic variable. *)
   | List of t list  (** A list of expressions. *)
   | App of Symbol.t * t list  (** Function application. *)
@@ -86,6 +87,9 @@ val value : Value.t -> t
     address and offset. *)
 val ptr : int32 -> t -> t
 
+(** [loc l] constructs an abstract location *)
+val loc : Loc.t -> t
+
 (** [list l] constructs a list expression with the given list of expressions *)
 val list : t list -> t
 

src/smtml/loc.ml

@@ -0,0 +1,20 @@
+(* SPDX-License-Identifier: MIT *)
+(* Copyright (C) 2023-2024 formalsec *)
+(* Written by the Smtml programmers *)
+
+type t = int
+
+let fresh =
+  let next = ref 0 in
+  fun () ->
+    let id = !next in
+    incr next;
+    id
+
+let compare = Int.compare
+
+let equal a b = compare a b = 0
+
+let hash a = a
+
+let pp = Fmt.int

src/smtml/loc.mli

@@ -0,0 +1,11 @@
+type t
+
+val fresh : unit -> t
+
+val compare : t -> t -> int
+
+val equal : t -> t -> bool
+
+val hash : t -> int
+
+val pp : t Fmt.t

src/smtml/mappings.ml

@@ -787,7 +787,7 @@ module Make (M_with_make : M_with_make) : S_with_fresh = struct
         let ctx, vars = encode_exprs ctx vars in
         let ctx, body = encode_expr ctx body in
         (ctx, M.exists vars body)
-      | List _ | Binder _ ->
+      | List _ | Binder _ | Loc _ ->
         Fmt.failwith "Cannot encode expression: %a" Expr.pp hte
 
     and encode_exprs ctx (es : Expr.t list) : symbol_ctx * M.term list =

src/smtml/rewrite.ml

@@ -58,7 +58,7 @@ let rewrite_ty unknown_ty tys =
 let rec rewrite_expr (type_map, expr_map) hte =
   debug "rewrite_expr: %a@." (fun k -> k Expr.pp hte);
   match Expr.view hte with
-  | Val _ -> hte
+  | Val _ | Loc _ -> hte
   | Ptr { base; offset } ->
     let base = Bitvector.to_int32 base in
     Expr.ptr base (rewrite_expr (type_map, expr_map) offset)