Trim explored paths and enable collections-c for owi conc

src/cmd/cmd_sym.ml

@@ -54,8 +54,10 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
   let result = List.fold_left (run_file ~unsafe ~optimize) pc files in
   let thread = Thread_with_memory.init () in
   let res_queue = Wq.init () in
+  let path_count = ref 0 in
   let callback v =
     let open Symbolic_choice_intf in
+    incr path_count;
     match (fail_mode, v) with
     | _, (EVal (Ok ()), _) -> ()
     | _, (EVal (Error e), thread) -> Wq.push (`Error e, thread) res_queue
@@ -115,8 +117,9 @@ let cmd profiling debug unsafe optimize workers no_stop_at_failure no_values
     else results
   in
   let* count = print_and_count_failures 0 results in
+  Fmt.pr "Completed paths: %d@." !path_count;
   if count > 0 then Error (`Found_bug count)
   else begin
-    Fmt.pr "All OK";
+    Fmt.pr "All OK@.";
     Ok ()
   end

src/concolic/concolic_choice.ml

@@ -84,7 +84,7 @@ let ( let+ ) = map
 let abort =
   M
     (fun st ->
-      (Ok (), { st with pc = Assert (Symbolic_value.Bool.const false) :: st.pc })
+      (Ok (), { st with pc = Assume (Symbolic_value.Bool.const false) :: st.pc })
       )
 
 let add_pc (c : Concolic_value.V.vbool) =
@@ -94,7 +94,7 @@ let add_pc_to_thread (st : thread) c = { st with pc = c :: st.pc }
 
 let no_choice e =
   let v = Smtml.Expr.simplify e in
-  match Smtml.Expr.view v with Val _ -> true | _ -> false
+  not (Smtml.Expr.is_symbolic v)
 
 let select (vb : Concolic_value.V.vbool) =
   let r = vb.concrete in

src/concolic/concolic_value.ml

@@ -141,9 +141,7 @@ module T_pair (C : Value_intf.T) (S : Value_intf.T) = struct
       match (C.Ref.get_func ref.concrete, S.Ref.get_func ref.symbolic) with
       | Null, Null -> Null
       | Type_mismatch, Type_mismatch -> Type_mismatch
-      | Ref_value c, Ref_value s ->
-        assert (equal_func_intf c s);
-        Ref_value c
+      | Ref_value c, Ref_value _s -> Ref_value c
       | _ -> assert false
 
     let get_externref ref ty_id : _ Value_intf.get_ref =

src/concolic/concolic_wasm_ffi.ml

@@ -111,14 +111,16 @@ module M :
     | Val (Num (I32 v)) -> Choice.return v
     | _ ->
       Log.debug2 {|alloc: cannot allocate base pointer "%a"|} Expr.pp v.symbolic;
-      Choice.bind (abort ()) (fun () -> assert false)
+      assert false
+  (* Choice.bind (abort ()) (fun () -> assert false) *)
 
   let ptr (v : Value.int32) : int32 Choice.t =
     match view v.symbolic with
     | Ptr { base; _ } -> Choice.return base
     | _ ->
       Log.debug2 {|free: cannot fetch pointer base of "%a"|} Expr.pp v.symbolic;
-      Choice.bind (abort ()) (fun () -> assert false)
+      assert false
+  (* Choice.bind (abort ()) (fun () -> assert false) *)
 
   let exit (_p : Value.int32) : unit Choice.t = abort ()
 

src/symbolic/symbolic_memory.ml

@@ -149,9 +149,10 @@ let extract v pos =
   | Val (Num (I64 i)) ->
     let i' = Int64.(to_int @@ logand 0xffL @@ shr_s i @@ of_int (pos * 8)) in
     value (Num (I8 i'))
-  | Cvtop (_, Zero_extend 24, ({ node = Symbol _; _ } as sym))
-  | Cvtop (_, Sign_extend 24, ({ node = Symbol _; _ } as sym))
-    when Smtml.Ty.equal (Ty_bitv 8) (ty sym) ->
+  | Cvtop
+      ( _
+      , (Zero_extend 24 | Sign_extend 24)
+      , ({ node = Symbol { ty = Ty_bitv 8; _ }; _ } as sym) ) ->
     sym
   | _ -> make (Extract (v, pos + 1, pos))
 

src/symbolic/symbolic_value.ml

@@ -200,6 +200,7 @@ module I32 = struct
   let to_bool (e : vbool) =
     match view e with
     | Val (Num (I32 i)) -> Bool.const @@ Int32.ne i 0l
+    | Ptr _ -> Bool.const true
     | Cvtop (_, OfBool, cond) -> cond
     | _ -> make (Cvtop (ty, ToBool, e))
 

test/c/collections-c/dune

@@ -2,4 +2,5 @@
  (deps
   %{bin:owi}
   (package owi)
-  (source_tree files)))
+  (source_tree files)
+  run-subdir.sh))