update for latest encoding that uses Hc for hashconsing

dune-project

@@ -47,12 +47,12 @@
   (bisect_ppx
    (and
     :with-test
-    (>= "2.5")
+    (>= 2.5)
     :dev))
   (ocb
    (and
     :with-test
-    (>= "0.1")
+    (>= 0.1)
     :dev))
   (odoc :with-doc)
   (crunch :dev)
@@ -61,7 +61,7 @@
   (mdx
    (and
     :with-test
-    (>= "2.1")))
+    (>= 2.1)))
   (crowbar :with-test)
   (graphics :dev)
   (tiny_httpd :dev)
@@ -70,5 +70,6 @@
   xmlm
   pyml
   re2
+  (hc (>= 0.3))
   dune-site)
  (sites (share pyc) (share binc) (share libc)))

owi.opam

@@ -38,6 +38,7 @@ depends: [
   "xmlm"
   "pyml"
   "re2"
+  "hc" {>= "0.3"}
   "dune-site"
 ]
 build: [

src/cmd_sym.ml

@@ -2,7 +2,7 @@ open Syntax
 module Expr = Encoding.Expr
 module Value = Symbolic_value.S
 module Choice = Symbolic.P.Choice
-module Solver = Thread.Solver
+open Hc
 
 (* TODO: make this a CLI flag *)
 let print_solver_time = false
@@ -64,12 +64,12 @@ let symbolic_extern_module : Symbolic.P.extern_func Link.extern_module =
 let summaries_extern_module : Symbolic.P.extern_func Link.extern_module =
   let open Expr in
   let i32 v =
-    match v.e with
+    match v.node.e with
     | Val (Num (I32 v)) -> v
     | _ -> Log.err {|alloc: cannot allocate base pointer "%a"|} Expr.pp v
   in
   let ptr v =
-    match v.e with
+    match v.node.e with
     | Ptr (b, _) -> b
     | _ -> Log.err {|free: cannot fetch pointer base of "%a"|} Expr.pp v
   in
@@ -176,8 +176,10 @@ let run_file ~unsafe ~optimize (pc : unit Result.t Choice.t) filename =
     simplify_then_link_then_run ~unsafe ~optimize pc script
 
 let get_model solver pc =
-  assert (Solver.check solver pc);
-  match Solver.model solver with None -> assert false | Some model -> model
+  assert (Thread.Solver.check solver pc);
+  match Thread.Solver.model solver with
+  | None -> assert false
+  | Some model -> model
 
 let mkdir_p_exn dir =
   let rec get_intermediate_dirs d acc =
@@ -217,7 +219,7 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure workspace
   if debug then Log.debug_on := true;
   mkdir_p_exn workspace;
   let pc = Choice.return (Ok ()) in
-  let solver = Solver.create () in
+  let solver = Thread.Solver.create () in
   let result = List.fold_left (run_file ~unsafe ~optimize) pc files in
   let thread : Thread.t = Thread.create () in
   let results = Choice.run_and_trap ~workers result thread in

src/dune

@@ -72,6 +72,7 @@
   bos
   dune-site
   encoding
+  hc
   integers
   menhirLib
   ocaml_intrinsics

src/symbolic.ml

@@ -3,13 +3,11 @@
 (* Copyright © 2021 Pierre Chambart *)
 
 open Types
-module Def_value = Concrete_value
+open Hc
 module Solver = Thread.Solver
 
 module P = struct
-  module Value = struct
-    include Symbolic_value.S
-  end
+  module Value = Symbolic_value.S
 
   type memory = Symbolic_memory.M.t
 
@@ -34,7 +32,7 @@ module P = struct
   type thread = Thread.t
 
   module Choice = Symbolic_choice.MT
-  module Extern_func = Def_value.Make_extern_func (Value) (Choice)
+  module Extern_func = Concrete_value.Make_extern_func (Value) (Choice)
 
   let select (c : vbool) ~(if_true : Value.t) ~(if_false : Value.t) :
     Value.t Choice.t =
@@ -56,11 +54,9 @@ module P = struct
 
   type env = extern_func Link_env.t
 
-  type func = Def_value.Func.t
+  type func = Concrete_value.Func.t
 
-  module Func = struct
-    include Extern_func
-  end
+  module Func = Extern_func
 
   module Global = struct
     type t = global
@@ -113,21 +109,21 @@ module P = struct
       Choice.with_thread (fun thread ->
           let (S (solver_mod, solver)) = Thread.solver thread in
           let module Solver = (val solver_mod) in
-          match a.e with
-          | Val _ | Ptr (_, { e = Val _; _ }) -> a
+          match a.node.e with
+          | Val _ | Ptr (_, { node = { e = Val _; _ }; _ }) -> a
           | Ptr (base, offset) ->
             (* TODO: can we remove this check? We should be in a SAT branch *)
             assert (Solver.check solver @@ Thread.pc thread);
             let concrete_offest = Solver.get_value solver offset in
-            let cond = Relop (Eq, offset, concrete_offest) @: a.ty in
+            let cond = Relop (Eq, offset, concrete_offest) @: a.node.ty in
             (* TODO: this should go to the pc *)
             Solver.add solver [ cond ];
-            Ptr (base, concrete_offest) @: a.ty
+            Ptr (base, concrete_offest) @: a.node.ty
           | _ ->
             (* TODO: can we remove this check? We should be in a SAT branch *)
             assert (Solver.check solver @@ Thread.pc thread);
             let concrete_addr = Solver.get_value solver a in
-            let cond = Relop (Eq, a, concrete_addr) @: a.ty in
+            let cond = Relop (Eq, a, concrete_addr) @: a.node.ty in
             (* TODO: this should go to the pc *)
             Solver.add solver [ cond ];
             concrete_addr )
@@ -140,7 +136,7 @@ module P = struct
           let pc = Thread.pc thread in
           let (S (solver_mod, solver)) = Thread.solver thread in
           let module Solver = (val solver_mod) in
-          match a.e with
+          match a.node.e with
           | Val (Num (I32 _)) -> Ok a
           | Ptr (base, offset) -> (
             match Hashtbl.find m.chunks base with

src/symbolic_choice.ml

@@ -5,6 +5,7 @@
 open Encoding
 open Choice_intf
 open Symbolic_value
+open Hc
 
 exception Assertion of Expr.t * Thread.t
 
@@ -13,7 +14,7 @@ let check sym_bool thread =
   let pc = Thread.pc thread in
   let no = S.Bool.not sym_bool in
   let no = Expr.simplify no in
-  match no.e with
+  match no.node.e with
   | Val True -> false
   | Val False -> true
   | _ ->
@@ -59,7 +60,7 @@ end = struct
 
   let select b ({ Thread.pc; solver = S (solver_module, s); _ } as thread) =
     let v = Expr.simplify b in
-    match v.e with
+    match v.node.e with
     | Val True -> M.return (true, thread)
     | Val False -> M.return (false, thread)
     | Val (Num (I32 _)) -> assert false
@@ -79,7 +80,7 @@ end = struct
         M.cons (true, thread1) (M.return (false, thread2)) )
 
   let fix_symbol (e : Expr.t) pc =
-    match e.e with
+    match e.node.e with
     | Symbol sym -> (pc, sym)
     | _ ->
       let sym = Symbol.("choice_i32" @: Ty_bitv S32) in
@@ -108,7 +109,7 @@ end = struct
     let sym_int = Expr.simplify sym_int in
     let orig_pc = pc in
     let pc, symbol = fix_symbol sym_int pc in
-    match sym_int.e with
+    match sym_int.node.e with
     | Val (Num (I32 i)) -> M.return (i, thread)
     | _ ->
       let module Solver = (val solver_module) in
@@ -309,21 +310,21 @@ module MT = struct
   let ( let* ) = bind
 
   let select (cond : S.vbool) =
-    match cond.e with
+    match cond.node.e with
     | Val True -> Retv true
     | Val False -> Retv false
     | _ -> Choice cond
   [@@inline]
 
   let select_i32 (i : S.int32) =
-    match i.e with Val (Num (I32 v)) -> Retv v | _ -> Choice_i32 i
+    match i.node.e with Val (Num (I32 v)) -> Retv v | _ -> Choice_i32 i
 
   let trap t = Trap t
 
   let with_thread f = Ret (St (fun t -> (f t, t))) [@@inline]
 
   let add_pc (c : S.vbool) =
-    match c.e with
+    match c.node.e with
     | Val True -> Retv ()
     | Val False -> Empty
     | _ -> Ret (St (fun t -> ((), { t with pc = c :: t.pc })))

src/symbolic_memory.ml

@@ -10,6 +10,7 @@ module M = struct
   module Expr = Encoding.Expr
   module Ty = Encoding.Ty
   open Expr
+  open Hc
 
   let page_size = Value.const_i32 65_536l
 
@@ -32,7 +33,7 @@ module M = struct
     }
 
   let i32 v =
-    match v.e with
+    match v.node.e with
     | Val (Num (I32 i)) -> i
     | _ -> Log.err {|Unsupported symbolic value reasoning over "%a"|} Expr.pp v
 
@@ -94,16 +95,15 @@ module M = struct
 
   (* TODO: don't rebuild so many values it generates unecessary hc lookups *)
   let merge_extracts (e1, h, m1) (e2, m2, l) =
+    let ty = e1.node.ty in
     if m1 = m2 && Expr.equal e1 e2 then
-      if h - l = Ty.size e1.ty then e1 else Extract (e1, h, l) @: e1.ty
+      if h - l = Ty.size ty then e1 else Extract (e1, h, l) @: ty
     else
-      Expr.(
-        Concat (Extract (e1, h, m1) @: e1.ty, Extract (e2, m2, l) @: e1.ty)
-        @: e1.ty )
+      Expr.(Concat (Extract (e1, h, m1) @: ty, Extract (e2, m2, l) @: ty) @: ty)
 
   let concat ~msb ~lsb offset =
     assert (offset > 0 && offset <= 8);
-    match (msb.e, lsb.e) with
+    match (msb.node.e, lsb.node.e) with
     | Val (Num (I8 i1)), Val (Num (I8 i2)) ->
       Value.const_i32 Int32.(logor (shl (of_int i1) 8l) (of_int i2))
     | Val (Num (I8 i1)), Val (Num (I32 i2)) ->
@@ -119,7 +119,8 @@ module M = struct
       Value.const_i64 Int64.(logor (shl (of_int i1) offset) i2)
     | Extract (e1, h, m1), Extract (e2, m2, l) ->
       merge_extracts (e1, h, m1) (e2, m2, l)
-    | Extract (e1, h, m1), Concat ({ e = Extract (e2, m2, l); _ }, e3) ->
+    | ( Extract (e1, h, m1)
+      , Concat ({ node = { e = Extract (e2, m2, l); _ }; _ }, e3) ) ->
       let ty : Ty.t = if offset >= 4 then Ty_bitv S64 else Ty_bitv S32 in
       Concat (merge_extracts (e1, h, m1) (e2, m2, l), e3) @: ty
     | _ ->
@@ -139,25 +140,25 @@ module M = struct
 
   let load_8_s m (a : int32) =
     let v = loadn m (i32 a) 1 in
-    match v.e with
+    match v.node.e with
     | Val (Num (I8 i8)) -> Value.const_i32 (Int32.extend_s 8 (Int32.of_int i8))
     | _ -> Cvtop (ExtS 24, v) @: Ty_bitv S32
 
   let load_8_u m (a : int32) =
     let v = loadn m (i32 a) 1 in
-    match v.e with
+    match v.node.e with
     | Val (Num (I8 i)) -> Value.const_i32 (Int32.of_int i)
     | _ -> Cvtop (ExtU 24, v) @: Ty_bitv S32
 
   let load_16_s m (a : int32) =
     let v = loadn m (i32 a) 2 in
-    match v.e with
+    match v.node.e with
     | Val (Num (I32 i16)) -> Value.const_i32 (Int32.extend_s 16 i16)
     | _ -> Cvtop (ExtS 16, v) @: Ty_bitv S32
 
   let load_16_u m (a : int32) =
     let v = loadn m (i32 a) 2 in
-    match v.e with
+    match v.node.e with
     | Val (Num (I32 _)) -> v
     | _ -> Cvtop (ExtU 16, v) @: Ty_bitv S32
 
@@ -166,15 +167,16 @@ module M = struct
   let load_64 m (a : int32) = loadn m (i32 a) 8
 
   let extract v pos =
-    match v.e with
+    match v.node.e with
     | Val (Num (I32 i)) ->
       let i' = Int32.(to_int @@ logand 0xffl @@ shr_s i @@ of_int (pos * 8)) in
       Val (Num (I8 i')) @: Ty_bitv S8
     | Val (Num (I64 i)) ->
       let i' = Int64.(to_int @@ logand 0xffL @@ shr_s i @@ of_int (pos * 8)) in
       Val (Num (I8 i')) @: Ty_bitv S8
-    | Cvtop (ExtU 24, ({ e = Symbol _; ty = Ty_bitv S8 } as sym))
-    | Cvtop (ExtS 24, ({ e = Symbol _; ty = Ty_bitv S8 } as sym)) ->
+    | Cvtop (ExtU 24, ({ node = { e = Symbol _; ty = Ty_bitv S8 }; _ } as sym))
+    | Cvtop (ExtS 24, ({ node = { e = Symbol _; ty = Ty_bitv S8 }; _ } as sym))
+      ->
       sym
     | _ -> Extract (v, pos + 1, pos) @: Ty_bitv S8