From 192de5fbf554efb3b8768dcf7212394d62d144e2 Mon Sep 17 00:00:00 2001 From: Filipe Marques Date: Thu, 7 Nov 2024 11:04:52 +0000 Subject: [PATCH] Bump smtml to 0.3.1 --- dune-project | 2 +- owi.opam | 2 +- src/concolic/concolic_wasm_ffi.ml | 12 +++--- src/symbolic/symbolic_choice.ml | 4 +- src/symbolic/symbolic_memory_concretizing.ml | 39 ++++++++++---------- 5 files changed, 29 insertions(+), 30 deletions(-) diff --git a/dune-project b/dune-project index 6554bf673..c423bd2b1 100644 --- a/dune-project +++ b/dune-project @@ -52,7 +52,7 @@ ocaml_intrinsics (prelude (>= 0.3)) sedlex - (smtml (>= 0.2.3)) + (smtml (>= 0.3.1)) uutf xmlm (processor (>= 0.2)) diff --git a/owi.opam b/owi.opam index 780cbad01..4196a9672 100644 --- a/owi.opam +++ b/owi.opam @@ -29,7 +29,7 @@ depends: [ "ocaml_intrinsics" "prelude" {>= "0.3"} "sedlex" - "smtml" {>= "0.2.3"} + "smtml" {>= "0.3.1"} "uutf" "xmlm" "processor" {>= "0.2"} diff --git a/src/concolic/concolic_wasm_ffi.ml b/src/concolic/concolic_wasm_ffi.ml index 17b44bf53..289aaaf8f 100644 --- a/src/concolic/concolic_wasm_ffi.ml +++ b/src/concolic/concolic_wasm_ffi.ml @@ -26,7 +26,7 @@ module M : | Some (Num (I32 n)) -> n | _ -> assert false in - (I32 n, Value.pair n (Expr.mk_symbol sym)) ) + (I32 n, Value.pair n (Expr.symbol sym)) ) let symbol_i8 () : Value.int32 Choice.t = Choice.with_new_symbol (Ty_bitv 32) (fun sym forced_value -> @@ -37,7 +37,7 @@ module M : | _ -> assert false in let sym_expr = - Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.mk_symbol sym)) + Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) in (I32 n, Value.pair n sym_expr) ) @@ -50,7 +50,7 @@ module M : | _ -> assert false in let sym_expr = - Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.mk_symbol sym)) + Expr.make (Cvtop (Ty_bitv 32, Zero_extend 24, Expr.symbol sym)) in (I32 n, Value.pair n sym_expr) ) @@ -62,7 +62,7 @@ module M : | Some (Num (I64 n)) -> n | _ -> assert false in - (I64 n, Value.pair n (Expr.mk_symbol sym)) ) + (I64 n, Value.pair n (Expr.symbol sym)) ) let symbol_f32 () : Value.float32 Choice.t = Choice.with_new_symbol (Ty_fp 32) (fun sym forced_value -> @@ -73,7 +73,7 @@ module M : | _ -> assert false in let n = Float32.of_bits n in - (F32 n, Value.pair n (Expr.mk_symbol sym)) ) + (F32 n, Value.pair n (Expr.symbol sym)) ) let symbol_f64 () : Value.float64 Choice.t = Choice.with_new_symbol (Ty_fp 64) (fun sym forced_value -> @@ -84,7 +84,7 @@ module M : | _ -> assert false in let n = Float64.of_bits n in - (F64 n, Value.pair n (Expr.mk_symbol sym)) ) + (F64 n, Value.pair n (Expr.symbol sym)) ) let assume_i32 (i : Value.int32) : unit Choice.t = let c = Value.I32.to_bool i in diff --git a/src/symbolic/symbolic_choice.ml b/src/symbolic/symbolic_choice.ml index 8c489dbba..55e81ccf6 100644 --- a/src/symbolic/symbolic_choice.ml +++ b/src/symbolic/symbolic_choice.ml @@ -420,7 +420,7 @@ module Make (Thread : Thread.S) = struct let sym_name = Fmt.str "choice_i32_%i" num_symbols in let sym_type = Smtml.Ty.Ty_bitv 32 in let sym = Smtml.Symbol.make sym_type sym_name in - let assign = Smtml.Expr.(relop Ty_bool Eq (mk_symbol sym) e) in + let assign = Smtml.Expr.(relop Ty_bool Eq (symbol sym) e) in (Some assign, sym) let select_i32 (i : Symbolic_value.int32) = @@ -440,7 +440,7 @@ module Make (Thread : Thread.S) = struct | Smtml.Value.Num (I32 i) -> i | _ -> Fmt.failwith "Unreachable: found symbol must be a value" in - let s = Smtml.Expr.mk_symbol symbol in + let s = Smtml.Expr.symbol symbol in let this_value_cond = let open Smtml.Expr in Bitv.I32.(s = v i) diff --git a/src/symbolic/symbolic_memory_concretizing.ml b/src/symbolic/symbolic_memory_concretizing.ml index 16fcd6724..47578ce59 100644 --- a/src/symbolic/symbolic_memory_concretizing.ml +++ b/src/symbolic/symbolic_memory_concretizing.ml @@ -1,6 +1,4 @@ module Backend = struct - open Smtml - type address = Int32.t type t = @@ -21,7 +19,7 @@ module Backend = struct let address a = let open Symbolic_choice_without_memory in - match Expr.view a with + match Smtml.Expr.view a with | Val (Num (I32 i)) -> return i | Ptr { base; offset } -> select_i32 Symbolic_value.(I32.add (const_i32 base) offset) @@ -33,21 +31,22 @@ module Backend = struct try Hashtbl.find data a with Not_found -> ( match parent with - | None -> Expr.value (Num (I8 0)) + | None -> Smtml.Expr.value (Num (I8 0)) | Some parent -> load_byte parent a ) (* TODO: don't rebuild so many values it generates unecessary hc lookups *) let merge_extracts (e1, h, m1) (e2, m2, l) = - let ty = Expr.ty e1 in - if m1 = m2 && Expr.equal e1 e2 then - if h - l = Ty.size ty then e1 else Expr.make (Extract (e1, h, l)) + let ty = Smtml.Expr.ty e1 in + if m1 = m2 && Smtml.Expr.equal e1 e2 then + if h - l = Smtml.Ty.size ty then e1 + else Smtml.Expr.make (Extract (e1, h, l)) else - Expr.( + Smtml.Expr.( make (Concat (make (Extract (e1, h, m1)), make (Extract (e2, m2, l)))) ) let concat ~msb ~lsb offset = assert (offset > 0 && offset <= 8); - match (Expr.view msb, Expr.view lsb) with + match (Smtml.Expr.view msb, Smtml.Expr.view lsb) with | Val (Num (I8 i1)), Val (Num (I8 i2)) -> Symbolic_value.const_i32 Int32.(logor (shl (of_int i1) 8l) (of_int i2)) | Val (Num (I8 i1)), Val (Num (I32 i2)) -> @@ -65,8 +64,8 @@ module Backend = struct | Extract (e1, h, m1), Extract (e2, m2, l) -> merge_extracts (e1, h, m1) (e2, m2, l) | Extract (e1, h, m1), Concat ({ node = Extract (e2, m2, l); _ }, e3) -> - Expr.(make (Concat (merge_extracts (e1, h, m1) (e2, m2, l), e3))) - | _ -> Expr.make (Concat (msb, lsb)) + Smtml.Expr.(make (Concat (merge_extracts (e1, h, m1) (e2, m2, l), e3))) + | _ -> Smtml.Expr.make (Concat (msb, lsb)) let loadn m a n = let rec loop addr size i acc = @@ -80,21 +79,21 @@ module Backend = struct loop a n 1 v0 let extract v pos = - match Expr.view v with + match Smtml.Expr.view v with | Val (Num (I8 _)) -> v | Val (Num (I32 i)) -> let i' = Int32.(to_int @@ logand 0xffl @@ shr_s i @@ of_int (pos * 8)) in - Expr.value (Num (I8 i')) + Smtml.Expr.value (Num (I8 i')) | Val (Num (I64 i)) -> let i' = Int64.(to_int @@ logand 0xffL @@ shr_s i @@ of_int (pos * 8)) in - Expr.value (Num (I8 i')) + Smtml.Expr.value (Num (I8 i')) | Cvtop (_, Zero_extend 24, ({ node = Symbol { ty = Ty_bitv 8; _ }; _ } as sym)) | Cvtop (_, Sign_extend 24, ({ node = Symbol { ty = Ty_bitv 8; _ }; _ } as sym)) -> sym - | _ -> Expr.make (Extract (v, pos + 1, pos)) + | _ -> Smtml.Expr.make (Extract (v, pos + 1, pos)) let storen m a v n = for i = 0 to n - 1 do @@ -127,16 +126,16 @@ module Backend = struct else Ok a ) | _ -> (* A symbolic expression is valid, but we print to check if Ptr's are passing through here *) - Log.debug2 "Saw a symbolic address: %a@." Expr.pp a; + Log.debug2 "Saw a symbolic address: %a@." Smtml.Expr.pp a; return (Ok a) let ptr v = let open Symbolic_choice_without_memory in - match Expr.view v with + match Smtml.Expr.view v with | Ptr { base; _ } -> return base | _ -> - Log.debug2 {|free: cannot fetch pointer base of "%a"|} Expr.pp v; - let* () = add_pc @@ Expr.value False in + Log.debug2 {|free: cannot fetch pointer base of "%a"|} Smtml.Expr.pp v; + let* () = add_pc @@ Smtml.Expr.value False in assert false let free m p = @@ -151,7 +150,7 @@ module Backend = struct let open Symbolic_choice_without_memory in let+ base = address ptr in Hashtbl.replace m.chunks base size; - Expr.ptr base (Symbolic_value.const_i32 0l) + Smtml.Expr.ptr base (Symbolic_value.const_i32 0l) end include Symbolic_memory_make.Make (Backend)