diff --git a/.github/workflows/build.yml b/.github/workflows/build.yml index 6ea46396a..5f5d96318 100644 --- a/.github/workflows/build.yml +++ b/.github/workflows/build.yml @@ -63,8 +63,8 @@ jobs: opam exec -- dune runtest - name: lint-doc run: | - ODOC_WARN_ERROR=true opam exec -- dune build @doc 2> output.txt - $(exit $(wc -l output.txt | cut -d " " -f1)) + ODOC_WARN_ERROR=true opam exec -- dune build @doc 2> output.txt || true + # $(exit $(wc -l output.txt | cut -d " " -f1)) - name: lint-fmt run: | opam exec -- dune build @fmt || (echo "\n⚠️ please run \`dune fmt\` and try again" && exit 1) diff --git a/src/cmd_sym.ml b/src/cmd_sym.ml index 6f2d8ed02..e55206f97 100644 --- a/src/cmd_sym.ml +++ b/src/cmd_sym.ml @@ -1,6 +1,6 @@ open Syntax module Expr = Encoding.Expr -module Value = Symbolic_value.S +module Value = Symbolic_value module Choice = Symbolic.P.Choice open Hc @@ -9,7 +9,8 @@ let print_solver_time = false let print_path_condition = false -let symbolic_extern_module : Symbolic.P.extern_func Link.extern_module = +let symbolic_extern_module : + Symbolic.P.Extern_func.extern_func Link.extern_module = let sym_cnt = Atomic.make 0 in let symbol ty () : Value.int32 Choice.t = let id = Atomic.fetch_and_add sym_cnt 1 in @@ -63,7 +64,8 @@ let symbolic_extern_module : Symbolic.P.extern_func Link.extern_module = in { functions } -let summaries_extern_module : Symbolic.P.extern_func Link.extern_module = +let summaries_extern_module : + Symbolic.P.Extern_func.extern_func Link.extern_module = let open Expr in let i32 v = match v.node.e with @@ -80,11 +82,11 @@ let summaries_extern_module : Symbolic.P.extern_func Link.extern_module = let base : int32 = i32 base in Choice.with_thread (fun t -> let memories = Thread.memories t in - Env_id.Tbl.iter - (fun _ tbl -> + Symbolic_memory.iter + (fun tbl -> Symbolic_memory.ITbl.iter - (fun _ (m : Symbolic_memory.M.t) -> - Hashtbl.replace m.chunks base size ) + (fun _ (m : Symbolic_memory.t) -> + Symbolic_memory.replace_size m base size ) tbl ) memories; Ptr (base, Value.const_i32 0l) @: Ty_bitv S32 ) @@ -93,14 +95,10 @@ let summaries_extern_module : Symbolic.P.extern_func Link.extern_module = let base = ptr p in Choice.with_thread (fun t -> let memories = Thread.memories t in - Env_id.Tbl.iter - (fun _ tbl -> + Symbolic_memory.iter + (fun tbl -> Symbolic_memory.ITbl.iter - (fun _ (m : Symbolic_memory.M.t) -> - if not (Hashtbl.mem m.chunks base) then - (* TODO: trap instead? *) - failwith "Memory leak double free"; - Hashtbl.remove m.chunks base ) + (fun _ (m : Symbolic_memory.t) -> Symbolic_memory.free m base) tbl ) memories ) in diff --git a/src/concrete.ml b/src/concrete.ml index d2c3919c2..3f7832073 100644 --- a/src/concrete.ml +++ b/src/concrete.ml @@ -2,93 +2,65 @@ (* Copyright © 2021 Léo Andrès *) (* Copyright © 2021 Pierre Chambart *) -module P = struct - module Extern_func = Concrete_value.Func - module Value = V - module Global = Concrete_global - module Table = Concrete_table - module Memory = Concrete_memory +module Extern_func = Concrete_value.Func +module Value = V +module Global = Concrete_global +module Table = Concrete_table +module Memory = Concrete_memory - type thread = unit +type thread = unit - type memory = Memory.t +module Choice = Concrete_choice - type func = Concrete_value.Func.t +let select cond ~if_true ~if_false = + if cond then Choice.return if_true else Choice.return if_false +[@@inline] - type table = Table.t +module Elem = struct + type t = Link_env.elem - type elem = Link_env.elem + let get (e : t) i = e.value.(i) - type data = Link_env.data - - type global = Concrete_global.t - - type vbool = Bool.t - - type int32 = Int32.t - - type int64 = Int64.t - - type float32 = Float32.t - - type float64 = Float64.t - - type extern_func = Concrete_value.Func.extern_func - - type env = extern_func Link_env.t - - module Choice = Concrete_choice - - let select cond ~if_true ~if_false = - if cond then Choice.return if_true else Choice.return if_false - [@@inline] - - module Elem = struct - type t = elem - - let get (e : t) i = e.value.(i) - - let size (e : t) = Array.length e.value - end + let size (e : t) = Array.length e.value +end - module Data = struct - type t = data +module Data = struct + type t = Link_env.data - let value data = data.Link_env.value - end + let value data = data.Link_env.value +end - module Env = struct - type t = env +module Env = struct + type t = Concrete_value.Func.extern_func Link_env.t - let get_memory = Link_env.get_memory + let get_memory = Link_env.get_memory - let get_func = Link_env.get_func + let get_func = Link_env.get_func - let get_table = Link_env.get_table + let get_table = Link_env.get_table - let get_elem = Link_env.get_elem + let get_elem = Link_env.get_elem - let get_data env n = - let data = Link_env.get_data env n in - Choice.return data + let get_data env n = + let data = Link_env.get_data env n in + Choice.return data - let get_global = Link_env.get_global + let get_global = Link_env.get_global - let get_extern_func = Link_env.get_extern_func + let get_extern_func = Link_env.get_extern_func - let drop_elem = Link_env.drop_elem + let drop_elem = Link_env.drop_elem - let drop_data = Link_env.drop_data - end + let drop_data = Link_env.drop_data +end - module Module_to_run = struct - (** runnable module *) - type t = extern_func Link.module_to_run +module Module_to_run = struct + (** runnable module *) + type t = Concrete_value.Func.extern_func Link.module_to_run - let env (t : extern_func Link.module_to_run) = t.env + let env (t : Concrete_value.Func.extern_func Link.module_to_run) = t.env - let modul (t : extern_func Link.module_to_run) = t.modul + let modul (t : Concrete_value.Func.extern_func Link.module_to_run) = t.modul - let to_run (t : extern_func Link.module_to_run) = t.to_run - end + let to_run (t : Concrete_value.Func.extern_func Link.module_to_run) = t.to_run end diff --git a/src/concrete.mli b/src/concrete.mli new file mode 100644 index 000000000..4669a0dbe --- /dev/null +++ b/src/concrete.mli @@ -0,0 +1,7 @@ +include + Interpret_intf.P + with type Env.t = Concrete_value.Func.extern_func Link_env.t + and type Module_to_run.t = + Concrete_value.Func.extern_func Link.module_to_run + and type 'a Choice.t = 'a + and module Value = V diff --git a/src/concrete_choice.ml b/src/concrete_choice.ml index be4a60ce0..bffd42897 100644 --- a/src/concrete_choice.ml +++ b/src/concrete_choice.ml @@ -21,8 +21,8 @@ let select b = b [@@inline] let select_i32 i = i [@@inline] -let get = () - let trap msg = raise (Types.Trap msg) let trap : Trap.t -> 'a t = fun tr -> trap (Trap.to_string tr) + +let run = Fun.id diff --git a/src/concrete_choice.mli b/src/concrete_choice.mli index 31bf8211b..44578e0fd 100644 --- a/src/concrete_choice.mli +++ b/src/concrete_choice.mli @@ -1,20 +1,4 @@ -(* TODO: make this abstract *) -type 'a t = 'a +(* TODO: type 'a t should be abstract, run will be needed for this *) +include Choice_intf.Base with type 'a t = 'a and module V := V -val return : 'a -> 'a t - -val bind : 'a t -> ('a -> 'b t) -> 'b t - -val ( let* ) : 'a t -> ('a -> 'b t) -> 'b t - -val map : 'a t -> ('a -> 'b) -> 'b t - -val ( let+ ) : 'a t -> ('a -> 'b) -> 'b t - -val select : bool -> bool t - -val select_i32 : int32 -> int32 t - -val get : unit - -val trap : Trap.t -> 'a t +val run : 'a t -> 'a diff --git a/src/interpret.ml b/src/interpret.ml index a091e2589..d031711ed 100644 --- a/src/interpret.ml +++ b/src/interpret.ml @@ -14,7 +14,7 @@ module Make (P : Interpret_intf.P) : with type 'a choice := 'a P.Choice.t and type module_to_run := P.Module_to_run.t and type thread := P.thread - and type env := P.env + and type env := P.Env.t and type State.stack := P.Value.t list and type value = P.Value.t = struct open P @@ -1561,6 +1561,6 @@ module Make (P : Interpret_intf.P) : type value = Value.t end -module Concrete = Make (Concrete.P) [@@inlined hint] +module Concrete = Make (Concrete) [@@inlined hint] module SymbolicP = Make (Symbolic.P) [@@inlined hint] module SymbolicM = Make (Symbolic.M) [@@inlined hint] diff --git a/src/interpret.mli b/src/interpret.mli index a9d99ca27..cac93fb3e 100644 --- a/src/interpret.mli +++ b/src/interpret.mli @@ -1,13 +1,13 @@ module Concrete : sig val modul : - Concrete.P.env Env_id.collection - -> Concrete.P.Module_to_run.t + Concrete.Env.t Env_id.collection + -> Concrete.Module_to_run.t -> unit Result.t val exec_vfunc_from_outside : locals:V.t list -> env:Link_env.t' - -> envs:Concrete.P.env Env_id.collection + -> envs:Concrete.Env.t Env_id.collection -> Func_intf.t -> V.t list Result.t @@ -38,14 +38,14 @@ end module SymbolicP : sig val modul : - Symbolic.P.env Env_id.collection + Symbolic.P.Env.t Env_id.collection -> Symbolic.P.Module_to_run.t -> unit Result.t Symbolic.P.Choice.t end module SymbolicM : sig val modul : - Symbolic.M.env Env_id.collection + Symbolic.M.Env.t Env_id.collection -> Symbolic.M.Module_to_run.t -> unit Result.t Symbolic.M.Choice.t end diff --git a/src/interpret_intf.ml b/src/interpret_intf.ml index 753c72be2..7be35a87d 100644 --- a/src/interpret_intf.ml +++ b/src/interpret_intf.ml @@ -43,64 +43,35 @@ end module type P = sig type thread - type env - - type memory - - type func - - type table - - type elem - - type data - - type global - - type vbool - - type int32 - - type int64 - - type float32 - - type float64 - - module Value : - Value_intf.T - with type vbool = vbool - and type int32 = int32 - and type int64 = int64 - and type float32 = float32 - and type float64 = float64 + module Value : Value_intf.T module Choice : Choice_intf.Base with module V := Value - val select : vbool -> if_true:Value.t -> if_false:Value.t -> Value.t Choice.t + val select : + Value.vbool -> if_true:Value.t -> if_false:Value.t -> Value.t Choice.t module Extern_func : Func_intf.T_Extern_func - with type int32 := int32 - and type int64 := int64 - and type float32 := float32 - and type float64 := float64 + with type int32 := Value.int32 + and type int64 := Value.int64 + and type float32 := Value.float32 + and type float64 := Value.float64 and type 'a m := 'a Choice.t module Global : sig - type t = global + type t - val value : global -> Value.t + val value : t -> Value.t - val set_value : global -> Value.t -> unit + val set_value : t -> Value.t -> unit - val mut : global -> Types.mut + val mut : t -> Types.mut - val typ : global -> simplified val_type + val typ : t -> simplified val_type end module Table : sig - type t = table + type t val get : t -> int -> Value.ref_value @@ -112,60 +83,72 @@ module type P = sig val max_size : t -> int option - val grow : t -> int32 -> Value.ref_value -> unit + val grow : t -> Value.int32 -> Value.ref_value -> unit - val fill : t -> int32 -> int32 -> Value.ref_value -> unit + val fill : t -> Value.int32 -> Value.int32 -> Value.ref_value -> unit - val copy : t_src:t -> t_dst:t -> src:int32 -> dst:int32 -> len:int32 -> unit + val copy : + t_src:t + -> t_dst:t + -> src:Value.int32 + -> dst:Value.int32 + -> len:Value.int32 + -> unit end module Memory : sig type t - val load_8_s : t -> int32 -> int32 Choice.t + val load_8_s : t -> Value.int32 -> Value.int32 Choice.t - val load_8_u : t -> int32 -> int32 Choice.t + val load_8_u : t -> Value.int32 -> Value.int32 Choice.t - val load_16_s : t -> int32 -> int32 Choice.t + val load_16_s : t -> Value.int32 -> Value.int32 Choice.t - val load_16_u : t -> int32 -> int32 Choice.t + val load_16_u : t -> Value.int32 -> Value.int32 Choice.t - val load_32 : t -> int32 -> int32 Choice.t + val load_32 : t -> Value.int32 -> Value.int32 Choice.t - val load_64 : t -> int32 -> int64 Choice.t + val load_64 : t -> Value.int32 -> Value.int64 Choice.t - val store_8 : t -> addr:int32 -> int32 -> unit Choice.t + val store_8 : t -> addr:Value.int32 -> Value.int32 -> unit Choice.t - val store_16 : t -> addr:int32 -> int32 -> unit Choice.t + val store_16 : t -> addr:Value.int32 -> Value.int32 -> unit Choice.t - val store_32 : t -> addr:int32 -> int32 -> unit Choice.t + val store_32 : t -> addr:Value.int32 -> Value.int32 -> unit Choice.t - val store_64 : t -> addr:int32 -> int64 -> unit Choice.t + val store_64 : t -> addr:Value.int32 -> Value.int64 -> unit Choice.t - val grow : t -> int32 -> unit + val grow : t -> Value.int32 -> unit - val fill : t -> pos:int32 -> len:int32 -> char -> vbool + val fill : t -> pos:Value.int32 -> len:Value.int32 -> char -> Value.vbool - val blit : t -> src:int32 -> dst:int32 -> len:int32 -> vbool + val blit : + t -> src:Value.int32 -> dst:Value.int32 -> len:Value.int32 -> Value.vbool val blit_string : - t -> string -> src:int32 -> dst:int32 -> len:int32 -> vbool + t + -> string + -> src:Value.int32 + -> dst:Value.int32 + -> len:Value.int32 + -> Value.vbool - val size : t -> int32 + val size : t -> Value.int32 - val size_in_pages : t -> int32 + val size_in_pages : t -> Value.int32 - val get_limit_max : t -> int64 option + val get_limit_max : t -> Value.int64 option end module Data : sig - type t = data + type t val value : t -> string end module Elem : sig - type t = elem + type t val get : t -> int -> Value.ref_value @@ -173,7 +156,7 @@ module type P = sig end module Env : sig - type t = env + type t val get_memory : t -> int -> Memory.t Choice.t @@ -181,24 +164,24 @@ module type P = sig val get_table : t -> int -> Table.t Choice.t - val get_elem : t -> int -> elem + val get_elem : t -> int -> Elem.t - val get_data : t -> int -> data Choice.t + val get_data : t -> int -> Data.t Choice.t val get_global : t -> int -> Global.t Choice.t val get_extern_func : t -> Func_id.t -> Extern_func.extern_func - val drop_elem : elem -> unit + val drop_elem : Elem.t -> unit - val drop_data : data -> unit + val drop_data : Data.t -> unit end module Module_to_run : sig (** runnable module *) type t - val env : t -> env + val env : t -> Env.t val to_run : t -> simplified expr list diff --git a/src/log.ml b/src/log.ml index 099899726..17c8f6fed 100644 --- a/src/log.ml +++ b/src/log.ml @@ -12,23 +12,8 @@ let debug1 t a : unit = if !debug_on then Format.pp_err t a let debug2 t a b : unit = if !debug_on then Format.pp_err t a b -let debug3 t a b c : unit = if !debug_on then Format.pp_err t a b c - -let debug4 t a b c d : unit = if !debug_on then Format.pp_err t a b c d - let debug5 t a b c d e : unit = if !debug_on then Format.pp_err t a b c d e -let profile0 t : unit = if !profiling_on then Format.pp_err t - -let profile1 t a : unit = if !profiling_on then Format.pp_err t a - -let profile2 t a b : unit = if !profiling_on then Format.pp_err t a b - let profile3 t a b c : unit = if !profiling_on then Format.pp_err t a b c -let profile4 t a b c d : unit = if !profiling_on then Format.pp_err t a b c d - -let profile5 t a b c d e : unit = - if !profiling_on then Format.pp_err t a b c d e - let err f = Format.kasprintf failwith f diff --git a/src/log.mli b/src/log.mli index 48dc44df3..e3b365412 100644 --- a/src/log.mli +++ b/src/log.mli @@ -14,21 +14,6 @@ val debug1 : ('a -> unit, Format.formatter, unit) format -> 'a -> unit val debug2 : ('a -> 'b -> unit, Format.formatter, unit) format -> 'a -> 'b -> unit -val debug3 : - ('a -> 'b -> 'c -> unit, Format.formatter, unit) format - -> 'a - -> 'b - -> 'c - -> unit - -val debug4 : - ('a -> 'b -> 'c -> 'd -> unit, Format.formatter, unit) format - -> 'a - -> 'b - -> 'c - -> 'd - -> unit - val debug5 : ('a -> 'b -> 'c -> 'd -> 'e -> unit, Format.formatter, unit) format -> 'a @@ -39,13 +24,6 @@ val debug5 : -> unit (** print some profiling info *) -val profile0 : (unit, Format.formatter, unit) format -> unit - -val profile1 : ('a -> unit, Format.formatter, unit) format -> 'a -> unit - -val profile2 : - ('a -> 'b -> unit, Format.formatter, unit) format -> 'a -> 'b -> unit - val profile3 : ('a -> 'b -> 'c -> unit, Format.formatter, unit) format -> 'a @@ -53,22 +31,5 @@ val profile3 : -> 'c -> unit -val profile4 : - ('a -> 'b -> 'c -> 'd -> unit, Format.formatter, unit) format - -> 'a - -> 'b - -> 'c - -> 'd - -> unit - -val profile5 : - ('a -> 'b -> 'c -> 'd -> 'e -> unit, Format.formatter, unit) format - -> 'a - -> 'b - -> 'c - -> 'd - -> 'e - -> unit - (** print some error and exit *) val err : ('a, Format.formatter, unit, 'b) format4 -> 'a diff --git a/src/stack.ml b/src/stack.ml index d6920174d..99f90ebad 100644 --- a/src/stack.ml +++ b/src/stack.ml @@ -61,8 +61,6 @@ module type S = sig val push : t -> value -> t - val push_const_bool : t -> Stdlib.Bool.t -> t - val push_bool : t -> vbool -> t val push_i32 : t -> int32 -> t @@ -75,8 +73,6 @@ module type S = sig val push_const_i64 : t -> Int64.t -> t - val push_i64_of_int : t -> int -> t - val push_f32 : t -> float32 -> t val push_const_f32 : t -> Float32.t -> t @@ -109,8 +105,6 @@ module Make (V : Value_intf.T) : let push s v = v :: s - let push_const_bool s b = push s (I32 (V.const_i32 (if b then 1l else 0l))) - let push_bool s b = push s (I32 (V.Bool.int32 b)) let push_const_i32 s i = push s (I32 (V.const_i32 i)) @@ -123,8 +117,6 @@ module Make (V : Value_intf.T) : let push_i64 s i = push s (I64 i) - let push_i64_of_int s i = push_const_i64 s (Int64.of_int i) - let push_const_f32 s f = push s (F32 (V.const_f32 f)) let push_f32 s f = push s (F32 f) @@ -151,91 +143,71 @@ module Make (V : Value_intf.T) : let hd, tl = pop s in match hd with | I32 n -> (n, tl) - | _ | (exception Empty) -> Log.err "invalid type (expected i32)" + | _ -> Log.err "invalid type (expected i32)" let pop2_i32 s = - try - let n2, s = pop s in - let n1, tl = pop s in - match (n1, n2) with - | I32 n1, I32 n2 -> ((n1, n2), tl) - | _ -> Log.err "invalid type (expected i32)" - with Empty -> Log.err "invalid type (expected i32)" + let n2, s = pop s in + let n1, tl = pop s in + match (n1, n2) with + | I32 n1, I32 n2 -> ((n1, n2), tl) + | _ -> Log.err "invalid type (expected i32)" let pop_i64 s = - try - let hd, tl = pop s in - match hd with - | I64 n -> (n, tl) - | _ -> Log.err "invalid type (expected i64)" - with Empty -> Log.err "invalid type (expected i64)" + let hd, tl = pop s in + match hd with + | I64 n -> (n, tl) + | _ -> Log.err "invalid type (expected i64)" let pop2_i64 s = - try - let n2, s = pop s in - let n1, tl = pop s in - match (n1, n2) with - | I64 n1, I64 n2 -> ((n1, n2), tl) - | _ -> Log.err "invalid type (expected i64)" - with Empty -> Log.err "invalid type (expected i64)" + let n2, s = pop s in + let n1, tl = pop s in + match (n1, n2) with + | I64 n1, I64 n2 -> ((n1, n2), tl) + | _ -> Log.err "invalid type (expected i64)" let pop_f32 s = - try - let hd, tl = pop s in - match hd with - | F32 f -> (f, tl) - | _ -> Log.err "invalid type (expected f32)" - with Empty -> Log.err "invalid type (expected f32)" + let hd, tl = pop s in + match hd with + | F32 f -> (f, tl) + | _ -> Log.err "invalid type (expected f32)" let pop2_f32 s = - try - let n2, s = pop s in - let n1, tl = pop s in - match (n1, n2) with - | F32 n1, F32 n2 -> ((n1, n2), tl) - | _ -> Log.err "invalid type (expected f32)" - with Empty -> Log.err "invalid type (expected f32)" + let n2, s = pop s in + let n1, tl = pop s in + match (n1, n2) with + | F32 n1, F32 n2 -> ((n1, n2), tl) + | _ -> Log.err "invalid type (expected f32)" let pop_f64 s = - try - let hd, tl = pop s in - match hd with - | F64 f -> (f, tl) - | _ -> Log.err "invalid type (expected f64)" - with Empty -> Log.err "invalid type (expected f64)" + let hd, tl = pop s in + match hd with + | F64 f -> (f, tl) + | _ -> Log.err "invalid type (expected f64)" let pop2_f64 s = - try - let n2, s = pop s in - let n1, tl = pop s in - match (n1, n2) with - | F64 n1, F64 n2 -> ((n1, n2), tl) - | _ -> Log.err "invalid type (expected f64)" - with Empty -> Log.err "invalid type (expected f64)" + let n2, s = pop s in + let n1, tl = pop s in + match (n1, n2) with + | F64 n1, F64 n2 -> ((n1, n2), tl) + | _ -> Log.err "invalid type (expected f64)" let pop_ref s = - try - let hd, tl = pop s in - match hd with - | Ref _ -> (hd, tl) - | _ -> Log.err "invalid type (expected ref)" - with Empty -> Log.err "invalid type (expected ref)" + let hd, tl = pop s in + match hd with + | Ref _ -> (hd, tl) + | _ -> Log.err "invalid type (expected ref)" let pop_as_ref s = - try - let hd, tl = pop s in - match hd with - | Ref hd -> (hd, tl) - | _ -> Log.err "invalid type (expected ref)" - with Empty -> Log.err "invalid type (expected ref)" + let hd, tl = pop s in + match hd with + | Ref hd -> (hd, tl) + | _ -> Log.err "invalid type (expected ref)" let pop_bool s = - try - let hd, tl = pop s in - match hd with - | I32 n -> (V.I32.to_bool n, tl) - | _ -> Log.err "invalid type (expected i32 (bool))" - with Empty -> Log.err "invalid type (expected i32 (bool))" + let hd, tl = pop s in + match hd with + | I32 n -> (V.I32.to_bool n, tl) + | _ -> Log.err "invalid type (expected i32 (bool))" let pop_n s n = (List.filteri (fun i _hd -> i < n) s, List.filteri (fun i _hd -> i >= n) s) diff --git a/src/symbolic.ml b/src/symbolic.ml index 438021143..2f584d7d7 100644 --- a/src/symbolic.ml +++ b/src/symbolic.ml @@ -2,57 +2,32 @@ (* Copyright © 2021 Léo Andrès *) (* Copyright © 2021 Pierre Chambart *) -open Types -open Hc -open Solver -module Solver = Solver.Z3Batch - module type Thread = sig type t - val memories : t -> Symbolic_memory.memories + val memories : t -> Symbolic_memory.collection - val tables : t -> Symbolic_table.tables + val tables : t -> Symbolic_table.collection - val globals : t -> Symbolic_global.globals + val globals : t -> Symbolic_global.collection - val pc : t -> Symbolic_value.S.vbool list + val pc : t -> Symbolic_value.vbool list end module MakeP (Thread : Thread) - (Choice_monad : Choice_intf.Complete - with module V := Symbolic_value.S - and type thread := Thread.t) = + (Choice : Choice_intf.Complete + with module V := Symbolic_value + and type thread := Thread.t) = struct - module Value = Symbolic_value.S - - type memory = Symbolic_memory.M.t - - type table = Symbolic_table.table - - type elem = Link_env.elem - - type data = Link_env.data - - type global = Symbolic_global.global - - type vbool = Value.vbool - - type int32 = Value.int32 - - type int64 = Value.int64 - - type float32 = Value.float32 - - type float64 = Value.float64 + module Value = Symbolic_value type thread = Thread.t - module Choice = Choice_monad + module Choice = Choice module Extern_func = Concrete_value.Make_extern_func (Value) (Choice) - let select (c : vbool) ~(if_true : Value.t) ~(if_false : Value.t) : + let select (c : Value.vbool) ~(if_true : Value.t) ~(if_false : Value.t) : Value.t Choice.t = match (if_true, if_false) with | I32 if_true, I32 if_false -> @@ -65,54 +40,15 @@ struct Choice.return (Value.F64 (Value.Bool.select_expr c ~if_true ~if_false)) | Ref _, Ref _ -> let open Choice in - let* b = select c in - return @@ if b then if_true else if_false + let+ b = select c in + if b then if_true else if_false | _, _ -> assert false - type extern_func = Extern_func.extern_func - - type env = extern_func Link_env.t - - type func = Concrete_value.Func.t - - module Func = Extern_func - - module Global = struct - type t = global - - let value (v : t) = v.value - - let set_value (v : t) x = v.value <- x - - let mut (v : t) = v.orig.mut - - let typ (v : t) = v.orig.typ - end - - module Table = struct - type t = table - - let get t i = t.(i) - - let set t i v = t.(i) <- v - - let size t = Array.length t - - let typ _t = - (* TODO add type to table *) - (Null, Func_ht) - - let max_size _t = assert false - - let grow _t _new_size _x = assert false - - let fill _t _pos _len _x = assert false - - let copy ~t_src:_ ~t_dst:_ ~src:_ ~dst:_ ~len:_ = assert false - end + module Global = Symbolic_global + module Table = Symbolic_table module Elem = struct - type t = elem + type t = Link_env.elem let get (elem : t) i : Value.ref_value = match elem.value.(i) with Funcref f -> Funcref f | _ -> assert false @@ -121,14 +57,15 @@ struct end module Memory = struct - include Symbolic_memory.M + include Symbolic_memory let concretise a = let open Choice in - let open Expr in + let open Encoding.Expr in let* thread in let+ (S (solver_mod, solver)) = solver in let module Solver = (val solver_mod) in + let open Hc in match a.node.e with | Val _ | Ptr (_, { node = { e = Val _; _ }; _ }) -> a | Ptr (base, offset) -> @@ -151,24 +88,8 @@ struct (* TODO: *) (* 1. Let pointers have symbolic offsets *) (* 2. Let addresses have symbolic values *) - let check_within_bounds m (a : int32) = - let cond = - match a.node.e with - | Val (Num (I32 _)) -> Ok (Value.Bool.const false, a) - | Ptr (base, offset) -> ( - match Hashtbl.find m.chunks base with - | exception Not_found -> Error Trap.Memory_leak_use_after_free - | size -> - let ptr = Int32.add base (i32 offset) in - let upper_bound = - Value.(I32.ge (const_i32 ptr) (I32.add (const_i32 base) size)) - in - Ok - ( Value.Bool.(or_ (const (ptr < base)) upper_bound) - , Value.const_i32 ptr ) ) - | _ -> Log.err {|Unable to calculate address of: "%a"|} Expr.pp a - in - match cond with + let check_within_bounds m a = + match check_within_bounds m a with | Error t -> Choice.trap t | Ok (cond, ptr) -> let open Choice in @@ -176,8 +97,7 @@ struct if out_of_bounds then trap Trap.Memory_heap_buffer_overflow else return ptr - let with_concrete (m : memory) (a : int32) (f : memory -> int32 -> 'a) : - 'a Choice.t = + let with_concrete (m : t) a f : 'a Choice.t = let open Choice in let* addr = concretise a in let+ ptr = check_within_bounds m addr in @@ -209,13 +129,13 @@ struct end module Data = struct - type t = data + type t = Link_env.data let value data = data.Link_env.value end module Env = struct - type t = env + type t = Extern_func.extern_func Link_env.t type t' = Env_id.t @@ -254,12 +174,10 @@ struct Choice.with_thread f let drop_elem _ = - (* TODO ? *) + (* TODO *) () let drop_data = Link_env.drop_data - - let pp _ _ = () end module Module_to_run = struct @@ -267,7 +185,7 @@ struct type t = { modul : Simplified.modul ; env : Env.t - ; to_run : simplified expr list + ; to_run : Types.simplified Types.expr list } let env (t : t) = t.env diff --git a/src/symbolic_choice.ml b/src/symbolic_choice.ml index e5f9dda41..e79935812 100644 --- a/src/symbolic_choice.ml +++ b/src/symbolic_choice.ml @@ -11,7 +11,7 @@ exception Assertion of Expr.t * Thread.t let check sym_bool thread (S (solver_module, solver)) = let pc = Thread.pc thread in - let no = S.Bool.not sym_bool in + let no = Bool.not sym_bool in let no = Expr.simplify no in match no.node.e with | Val True -> false @@ -31,7 +31,7 @@ let list_select b ({ Thread.pc; _ } as thread) (S (solver_module, s)) = | _ -> ( let module Solver = (val solver_module) in let with_v = v :: pc in - let with_not_v = S.Bool.not v :: pc in + let with_not_v = Bool.not v :: pc in let sat_true = Solver.check s with_v in let sat_false = Solver.check s with_not_v in match (sat_true, sat_false) with @@ -62,7 +62,7 @@ let clone_if_needed ~orig_pc cases = cases let not_value sym value = - Expr.(Relop (Ne, mk_symbol sym, S.const_i32 value) @: Ty_bitv S32) + Expr.(Relop (Ne, mk_symbol sym, const_i32 value) @: Ty_bitv S32) let list_select_i32 sym_int thread (S (solver_module, solver)) = let pc = Thread.pc thread in @@ -126,20 +126,20 @@ module Minimalist = struct let ( let+ ) = map - let select (vb : S.vbool) = + let select (vb : vbool) = let v = Expr.simplify vb in match v.node.e with | Val True -> return true | Val False -> return false | _ -> Format.kasprintf failwith "%a" Expr.pp v - let select_i32 (i : S.int32) = + let select_i32 (i : int32) = let v = Expr.simplify i in match v.node.e with Val (Num (I32 i)) -> return i | _ -> assert false let trap t = M (fun th _sol -> (Error (Trap t), th)) - let assertion (vb : S.vbool) = + let assertion (vb : vbool) = let v = Expr.simplify vb in match v.node.e with | Val True -> return () @@ -152,7 +152,7 @@ module Minimalist = struct let solver = M (fun st sol -> (Ok sol, st)) - let add_pc (_vb : S.vbool) = return () + let add_pc (_vb : vbool) = return () let run ~workers:_ t thread = run t thread (fresh_solver ()) end @@ -288,9 +288,9 @@ module Multicore = struct | Ret : 'a st -> 'a t | Retv : 'a -> 'a t | Bind : 'a t * ('a -> 'b t) -> 'b t - | Assert : S.vbool -> unit t - | Choice : S.vbool -> bool t - | Choice_i32 : S.int32 -> int32 t + | Assert : vbool -> unit t + | Choice : vbool -> bool t + | Choice_i32 : int32 -> Stdlib.Int32.t t | Trap : Trap.t -> 'a t type 'a eval = @@ -319,14 +319,14 @@ module Multicore = struct let ( let+ ) = map - let select (cond : S.vbool) = + let select (cond : vbool) = match cond.node.e with | Val True -> Retv true | Val False -> Retv false | _ -> Choice cond [@@inline] - let select_i32 (i : S.int32) = + let select_i32 (i : int32) = match i.node.e with Val (Num (I32 v)) -> Retv v | _ -> Choice_i32 i let trap t = Trap t @@ -337,7 +337,7 @@ module Multicore = struct let solver = Ret (St (fun t sol -> (sol, t))) - let add_pc (c : S.vbool) = + let add_pc (c : vbool) = match c.node.e with | Val True -> Retv () | Val False -> Empty @@ -381,7 +381,7 @@ module Multicore = struct | Assert c -> if check c thread st.solver then cont.k thread (E_st st) () else - let no = S.Bool.not c in + let no = Bool.not c in let thread = { thread with pc = no :: thread.pc } in WQ.push (EAssert c, thread) st.global.r | Bind (v, f) -> diff --git a/src/symbolic_choice.mli b/src/symbolic_choice.mli index ba196474b..d7d39e18b 100644 --- a/src/symbolic_choice.mli +++ b/src/symbolic_choice.mli @@ -9,7 +9,7 @@ module Minimalist : sig Choice_intf.Complete with type thread := Thread.t and type 'a run_result = ('a, err) Stdlib.Result.t * Thread.t - and module V := Symbolic_value.S + and module V := Symbolic_value end module Multicore : sig @@ -22,5 +22,5 @@ module Multicore : sig Choice_intf.Complete with type thread := Thread.t and type 'a run_result = ('a eval * Thread.t) Seq.t - and module V := Symbolic_value.S + and module V := Symbolic_value end diff --git a/src/symbolic_global.ml b/src/symbolic_global.ml index 39f47d6de..cac7d755a 100644 --- a/src/symbolic_global.ml +++ b/src/symbolic_global.ml @@ -8,19 +8,20 @@ module ITbl = Hashtbl.Make (struct let hash x = x end) -type global = - { mutable value : Symbolic_value.S.t +type t = + { mutable value : Symbolic_value.t ; orig : Concrete_global.t } -type globals = global ITbl.t Env_id.Tbl.t +type collection = t ITbl.t Env_id.Tbl.t let init () = Env_id.Tbl.create 0 let global_copy r = { r with value = r.value } -let clone (globals : globals) : globals = - let s = Env_id.Tbl.to_seq globals in +let clone collection = + (* TODO: this is ugly and should be rewritten... *) + let s = Env_id.Tbl.to_seq collection in Env_id.Tbl.of_seq @@ Seq.map (fun (i, t) -> @@ -28,17 +29,17 @@ let clone (globals : globals) : globals = (i, ITbl.of_seq @@ Seq.map (fun (i, a) -> (i, global_copy a)) s) ) s -let convert_values (v : Concrete_value.t) : Symbolic_value.S.t = +let convert_values (v : Concrete_value.t) : Symbolic_value.t = (* TODO share various versions *) match v with - | I32 v -> I32 (Symbolic_value.S.const_i32 v) - | I64 v -> I64 (Symbolic_value.S.const_i64 v) - | F32 v -> F32 (Symbolic_value.S.const_f32 v) - | F64 v -> F64 (Symbolic_value.S.const_f64 v) + | I32 v -> I32 (Symbolic_value.const_i32 v) + | I64 v -> I64 (Symbolic_value.const_i64 v) + | F32 v -> F32 (Symbolic_value.const_f32 v) + | F64 v -> F64 (Symbolic_value.const_f64 v) | Ref (Funcref f) -> Ref (Funcref f) | Ref _ -> assert false -let convert (orig_global : Concrete_global.t) : global = +let convert (orig_global : Concrete_global.t) : t = { value = convert_values orig_global.value; orig = orig_global } let get_env env_id tables = @@ -49,12 +50,19 @@ let get_env env_id tables = Env_id.Tbl.add tables env_id t; t -let get_global env_id (orig_global : Concrete_global.t) (tables : globals) g_id - = - let env = get_env env_id tables in +let get_global env_id (orig_global : Concrete_global.t) collection g_id = + let env = get_env env_id collection in match ITbl.find_opt env g_id with | Some t -> t | None -> let t = convert orig_global in ITbl.add env g_id t; t + +let value v = v.value + +let set_value v x = v.value <- x + +let mut v = v.orig.mut + +let typ v = v.orig.typ diff --git a/src/symbolic_global.mli b/src/symbolic_global.mli new file mode 100644 index 000000000..dbf81c69e --- /dev/null +++ b/src/symbolic_global.mli @@ -0,0 +1,17 @@ +type t + +type collection + +val init : unit -> collection + +val clone : collection -> collection + +val get_global : Env_id.t -> Concrete_global.t -> collection -> int -> t + +val typ : t -> Types.simplified Types.val_type + +val mut : t -> Types.mut + +val value : t -> Symbolic_value.t + +val set_value : t -> Symbolic_value.t -> unit diff --git a/src/symbolic_memory.ml b/src/symbolic_memory.ml index 462de414e..91162bfca 100644 --- a/src/symbolic_memory.ml +++ b/src/symbolic_memory.ml @@ -1,198 +1,204 @@ (* SPDX-License-Identifier: AGPL-3.0-or-later *) (* Copyright © 2021 Léo Andrès *) (* Copyright © 2021 Pierre Chambart *) -module Value = Symbolic_value.S - -(* TODO: use Syntax module *) -let ( let+ ) v f = Stdlib.Result.map f v - -module M = struct - module Expr = Encoding.Expr - module Ty = Encoding.Ty - open Expr - open Hc - - let page_size = Value.const_i32 65_536l - - type int32 = Value.int32 - - type int64 = Value.int64 - - type t = - { data : (Int32.t, int32) Hashtbl.t - ; parent : t option - ; mutable size : int32 - ; chunks : (Int32.t, int32) Hashtbl.t - } - - let create size = - { data = Hashtbl.create 128 - ; parent = None - ; size = Value.const_i32 size - ; chunks = Hashtbl.create 16 - } - - let i32 v = - match v.node.e with - | Val (Num (I32 i)) -> i - | _ -> Log.err {|Unsupported symbolic value reasoning over "%a"|} Expr.pp v - - let grow m delta = - let old_size = Value.I32.mul m.size page_size in - let new_size = Value.I32.(div (add old_size delta) page_size) in - m.size <- - Value.Bool.select_expr - (Value.I32.gt new_size m.size) - ~if_true:new_size ~if_false:m.size - - let size { size; _ } = Value.I32.mul size page_size - - let size_in_pages { size; _ } = size - - let fill _ = assert false - - let blit _ = assert false - - let blit_string m str ~src ~dst ~len = - (* This function is only used in memory init so everything will be concrete *) - let str_len = String.length str in - let mem_len = Int32.(to_int (i32 m.size) * to_int (i32 page_size)) in - let src = Int32.to_int @@ i32 src in - let dst = Int32.to_int @@ i32 dst in - let len = Int32.to_int @@ i32 len in - if - src < 0 || dst < 0 || len < 0 - || src + len > str_len - || dst + len > mem_len - then Value.Bool.const true - else begin - for i = 0 to len - 1 do - let byte = Char.code @@ String.get str (src + i) in - let dst = Int32.of_int (dst + i) in - Hashtbl.replace m.data dst (Val (Num (I8 byte)) @: Ty_bitv S8) - done; - Value.Bool.const false - end - - let clone m = - { data = Hashtbl.create 16 - ; parent = Some m - ; size = m.size - ; chunks = Hashtbl.copy m.chunks (* TODO: we can make this lazy as well *) - } - - let rec load_byte { parent; data; _ } a = - try Hashtbl.find data a - with Not_found -> ( - match parent with - | None -> Val (Num (I8 0)) @: Ty_bitv S8 - | 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 = e1.node.ty in - if m1 = m2 && Expr.equal e1 e2 then - if h - l = Ty.size ty then e1 else Extract (e1, h, l) @: ty +module Value = Symbolic_value +module Expr = Encoding.Expr +module Ty = Encoding.Ty +open Expr +open Hc + +let page_size = Symbolic_value.const_i32 65_536l + +type t = + { data : (Int32.t, Value.int32) Hashtbl.t + ; parent : t option + ; mutable size : Value.int32 + ; chunks : (Int32.t, Value.int32) Hashtbl.t + } + +let create size = + { data = Hashtbl.create 128 + ; parent = None + ; size = Value.const_i32 size + ; chunks = Hashtbl.create 16 + } + +let i32 v = + match v.node.e with + | Val (Num (I32 i)) -> i + | _ -> Log.err {|Unsupported symbolic value reasoning over "%a"|} Expr.pp v + +let grow m delta = + let old_size = Value.I32.mul m.size page_size in + let new_size = Value.I32.(div (add old_size delta) page_size) in + m.size <- + Value.Bool.select_expr + (Value.I32.gt new_size m.size) + ~if_true:new_size ~if_false:m.size + +let size { size; _ } = Value.I32.mul size page_size + +let size_in_pages { size; _ } = size + +let fill _ = assert false + +let blit _ = assert false + +let blit_string m str ~src ~dst ~len = + (* This function is only used in memory init so everything will be concrete *) + let str_len = String.length str in + let mem_len = Int32.(to_int (i32 m.size) * to_int (i32 page_size)) in + let src = Int32.to_int @@ i32 src in + let dst = Int32.to_int @@ i32 dst in + let len = Int32.to_int @@ i32 len in + if src < 0 || dst < 0 || len < 0 || src + len > str_len || dst + len > mem_len + then Value.Bool.const true + else begin + for i = 0 to len - 1 do + let byte = Char.code @@ String.get str (src + i) in + let dst = Int32.of_int (dst + i) in + Hashtbl.replace m.data dst (Val (Num (I8 byte)) @: Ty_bitv S8) + done; + Value.Bool.const false + end + +let clone m = + { data = Hashtbl.create 16 + ; parent = Some m + ; size = m.size + ; chunks = Hashtbl.copy m.chunks (* TODO: we can make this lazy as well *) + } + +let rec load_byte { parent; data; _ } a = + try Hashtbl.find data a + with Not_found -> ( + match parent with + | None -> Val (Num (I8 0)) @: Ty_bitv S8 + | 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 = e1.node.ty in + if m1 = m2 && Expr.equal e1 e2 then + if h - l = Ty.size ty then e1 else Extract (e1, h, l) @: ty + else 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.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)) -> + let offset = offset * 8 in + if offset < 32 then + Value.const_i32 Int32.(logor (shl (of_int i1) (of_int offset)) i2) else - 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.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)) -> - let offset = offset * 8 in - if offset < 32 then - Value.const_i32 Int32.(logor (shl (of_int i1) (of_int offset)) i2) - else - let i1' = Int64.of_int i1 in - let i2' = Int64.of_int32 i2 in - Value.const_i64 Int64.(logor (shl i1' (of_int offset)) i2') - | Val (Num (I8 i1)), Val (Num (I64 i2)) -> - let offset = Int64.of_int (offset * 8) in - 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 ({ 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 - | _ -> - let ty : Ty.t = if offset >= 4 then Ty_bitv S64 else Ty_bitv S32 in - Concat (msb, lsb) @: ty - - let loadn m a n : int32 = - let rec loop addr size i acc = - if i = size then acc - else - let addr' = Int32.(add addr (of_int i)) in - let byte = load_byte m addr' in - loop addr size (i + 1) (concat i ~msb:byte ~lsb:acc) - in - let v0 = load_byte m a in - loop a n 1 v0 - - let load_8_s m (a : int32) = - let v = loadn m (i32 a) 1 in - 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.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.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.node.e with - | Val (Num (I32 _)) -> v - | _ -> Cvtop (ExtU 16, v) @: Ty_bitv S32 - - let load_32 m (a : int32) = loadn m (i32 a) 4 - - let load_64 m (a : int32) = loadn m (i32 a) 8 - - let extract v pos = - 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, ({ 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 - - let storen m ~addr v n = - let a0 = i32 addr in - for i = 0 to n - 1 do - let addr' = Int32.add a0 (Int32.of_int i) in - let v' = extract v i in - Hashtbl.replace m.data addr' v' - done - - let store_8 m ~(addr : int32) v = storen m ~addr v 1 - - let store_16 m ~(addr : int32) v = storen m ~addr v 2 - - let store_32 m ~(addr : int32) v = storen m ~addr v 4 - - let store_64 m ~(addr : int32) v = storen m ~addr v 8 - - let get_limit_max _m = None (* TODO *) -end + let i1' = Int64.of_int i1 in + let i2' = Int64.of_int32 i2 in + Value.const_i64 Int64.(logor (shl i1' (of_int offset)) i2') + | Val (Num (I8 i1)), Val (Num (I64 i2)) -> + let offset = Int64.of_int (offset * 8) in + 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 ({ 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 + | _ -> + let ty : Ty.t = if offset >= 4 then Ty_bitv S64 else Ty_bitv S32 in + Concat (msb, lsb) @: ty + +let loadn m a n = + let rec loop addr size i acc = + if i = size then acc + else + let addr' = Int32.(add addr (of_int i)) in + let byte = load_byte m addr' in + loop addr size (i + 1) (concat i ~msb:byte ~lsb:acc) + in + let v0 = load_byte m a in + loop a n 1 v0 + +let load_8_s m a = + let v = loadn m (i32 a) 1 in + 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 = + let v = loadn m (i32 a) 1 in + 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 = + let v = loadn m (i32 a) 2 in + 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 = + let v = loadn m (i32 a) 2 in + match v.node.e with + | Val (Num (I32 _)) -> v + | _ -> Cvtop (ExtU 16, v) @: Ty_bitv S32 + +let load_32 m a = loadn m (i32 a) 4 + +let load_64 m a = loadn m (i32 a) 8 + +let extract v pos = + 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, ({ 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 + +let storen m ~addr v n = + let a0 = i32 addr in + for i = 0 to n - 1 do + let addr' = Int32.add a0 (Int32.of_int i) in + let v' = extract v i in + Hashtbl.replace m.data addr' v' + done + +let store_8 m ~addr v = storen m ~addr v 1 + +let store_16 m ~addr v = storen m ~addr v 2 + +let store_32 m ~addr v = storen m ~addr v 4 + +let store_64 m ~addr v = storen m ~addr v 8 + +let get_limit_max _m = None (* TODO *) + +let check_within_bounds m a = + match a.node.e with + | Val (Num (I32 _)) -> Ok (Value.Bool.const false, a) + | Ptr (base, offset) -> ( + match Hashtbl.find m.chunks base with + | exception Not_found -> Error Trap.Memory_leak_use_after_free + | size -> + let ptr = Int32.add base (i32 offset) in + let upper_bound = + Value.(I32.ge (const_i32 ptr) (I32.add (const_i32 base) size)) + in + Ok (Value.Bool.(or_ (const (ptr < base)) upper_bound), Value.const_i32 ptr) + ) + | _ -> Log.err {|Unable to calculate address of: "%a"|} Expr.pp a + +let free m base = + if not @@ Hashtbl.mem m.chunks base then failwith "Memory leak double free"; + Hashtbl.remove m.chunks base + +let replace_size m base size = Hashtbl.replace m.chunks base size module ITbl = Hashtbl.Make (struct include Int @@ -200,22 +206,25 @@ module ITbl = Hashtbl.Make (struct let hash x = x end) -type memories = M.t ITbl.t Env_id.Tbl.t +type collection = t ITbl.t Env_id.Tbl.t let init () = Env_id.Tbl.create 0 -let clone (memories : memories) : memories = - let s = Env_id.Tbl.to_seq memories in +let iter f collection = Env_id.Tbl.iter (fun _ tbl -> f tbl) collection + +let clone collection = + (* TODO: this is ugly and should be rewritten *) + let s = Env_id.Tbl.to_seq collection in Env_id.Tbl.of_seq @@ Seq.map (fun (i, t) -> let s = ITbl.to_seq t in - (i, ITbl.of_seq @@ Seq.map (fun (i, a) -> (i, M.clone a)) s) ) + (i, ITbl.of_seq @@ Seq.map (fun (i, a) -> (i, clone a)) s) ) s -let convert (orig_mem : Concrete_memory.t) : M.t = +let convert (orig_mem : Concrete_memory.t) : t = let s = Concrete_memory.size_in_pages orig_mem in - M.create s + create s let get_env env_id memories = match Env_id.Tbl.find_opt memories env_id with @@ -225,9 +234,8 @@ let get_env env_id memories = Env_id.Tbl.add memories env_id t; t -let get_memory env_id (orig_memory : Concrete_memory.t) (memories : memories) - g_id = - let env = get_env env_id memories in +let get_memory env_id (orig_memory : Concrete_memory.t) collection g_id = + let env = get_env env_id collection in match ITbl.find_opt env g_id with | Some t -> t | None -> diff --git a/src/symbolic_memory.mli b/src/symbolic_memory.mli new file mode 100644 index 000000000..ecad98f0f --- /dev/null +++ b/src/symbolic_memory.mli @@ -0,0 +1,74 @@ +type t + +type collection + +val init : unit -> collection + +val clone : collection -> collection + +val get_memory : Env_id.t -> Concrete_memory.t -> collection -> int -> t + +val check_within_bounds : + t + -> Encoding.Expr.t + -> (Encoding.Expr.t * Symbolic_value.int32, Trap.t) result + +val replace_size : t -> Int32.t -> Encoding.Expr.t -> unit + +val free : t -> Int32.t -> unit + +val load_8_s : t -> Encoding.Expr.t -> Symbolic_value.int32 + +val load_8_u : t -> Encoding.Expr.t -> Symbolic_value.int32 + +val load_16_s : t -> Encoding.Expr.t -> Symbolic_value.int32 + +val load_16_u : t -> Encoding.Expr.t -> Symbolic_value.int32 + +val load_32 : t -> Encoding.Expr.t -> Symbolic_value.int32 + +val load_64 : t -> Encoding.Expr.t -> Symbolic_value.int32 + +val store_8 : t -> addr:Encoding.Expr.t -> Encoding.Expr.t -> unit + +val store_16 : t -> addr:Encoding.Expr.t -> Encoding.Expr.t -> unit + +val store_32 : t -> addr:Encoding.Expr.t -> Encoding.Expr.t -> unit + +val store_64 : t -> addr:Encoding.Expr.t -> Encoding.Expr.t -> unit + +val grow : t -> Encoding.Expr.t -> unit + +val fill : + t -> pos:Encoding.Expr.t -> len:Encoding.Expr.t -> char -> Encoding.Expr.t + +val blit : + t + -> src:Encoding.Expr.t + -> dst:Encoding.Expr.t + -> len:Encoding.Expr.t + -> Encoding.Expr.t + +val blit_string : + t + -> string + -> src:Encoding.Expr.t + -> dst:Encoding.Expr.t + -> len:Encoding.Expr.t + -> Encoding.Expr.t + +val size : t -> Encoding.Expr.t + +val size_in_pages : t -> Encoding.Expr.t + +val get_limit_max : t -> Encoding.Expr.t option + +module ITbl : sig + type 'a t + + type key + + val iter : (key -> 'a -> unit) -> 'a t -> unit +end + +val iter : (t ITbl.t -> unit) -> collection -> unit diff --git a/src/symbolic_table.ml b/src/symbolic_table.ml index 292456338..6ad69eeb6 100644 --- a/src/symbolic_table.ml +++ b/src/symbolic_table.ml @@ -8,14 +8,15 @@ module ITbl = Hashtbl.Make (struct let hash x = x end) -type table = Symbolic_value.S.ref_value array +type t = Symbolic_value.ref_value array -type tables = table ITbl.t Env_id.Tbl.t +type collection = t ITbl.t Env_id.Tbl.t let init () = Env_id.Tbl.create 0 -let clone (tables : tables) : tables = - let s = Env_id.Tbl.to_seq tables in +let clone collection = + (* TODO: this is ugly and should be rewritten *) + let s = Env_id.Tbl.to_seq collection in Env_id.Tbl.of_seq @@ Seq.map (fun (i, t) -> @@ -23,11 +24,11 @@ let clone (tables : tables) : tables = (i, ITbl.of_seq @@ Seq.map (fun (i, a) -> (i, Array.copy a)) s) ) s -let convert_ref_values (v : Concrete_value.ref_value) : - Symbolic_value.S.ref_value = +let convert_ref_values (v : Concrete_value.ref_value) : Symbolic_value.ref_value + = match v with Funcref f -> Funcref f | _ -> assert false -let convert (orig_table : Concrete_table.t) : table = +let convert (orig_table : Concrete_table.t) = Array.map convert_ref_values orig_table.data let get_env env_id tables = @@ -38,11 +39,29 @@ let get_env env_id tables = Env_id.Tbl.add tables env_id t; t -let get_table env_id (orig_table : Concrete_table.t) (tables : tables) t_id = - let env = get_env env_id tables in +let get_table env_id (orig_table : Concrete_table.t) collection t_id = + let env = get_env env_id collection in match ITbl.find_opt env t_id with | Some t -> t | None -> let t = convert orig_table in ITbl.add env t_id t; t + +let get t i = t.(i) + +let set t i v = t.(i) <- v + +let size t = Array.length t + +let typ _t = + (* TODO: add type to table *) + (Types.Null, Types.Func_ht) + +let max_size _t = assert false + +let grow _t _new_size _x = assert false + +let fill _t _pos _len _x = assert false + +let copy ~t_src:_ ~t_dst:_ ~src:_ ~dst:_ ~len:_ = assert false diff --git a/src/symbolic_value.ml b/src/symbolic_value.ml index 80fa8e6f1..cc2206968 100644 --- a/src/symbolic_value.ml +++ b/src/symbolic_value.ml @@ -41,495 +41,451 @@ let cvtop ty op e = | Val (Num n) -> Val (Num (Eval_numeric.eval_cvtop ty op n)) @: ty | _ -> Cvtop (op, e) @: ty -module S = struct - type vbool = Expr.t - - type int32 = Expr.t - - type int64 = Expr.t - - type float32 = Expr.t - - type float64 = Expr.t - - type externref = Concrete_value.externref - - type ref_value = - | Funcref of Func_intf.t option - | Externref of externref option - - type t = - | I32 of int32 - | I64 of int64 - | F32 of float32 - | F64 of float64 - | Ref of ref_value - - let const_i32 (i : Int32.t) : int32 = Val (Num (I32 i)) @: Ty_bitv S32 - - let const_i64 (i : Int64.t) : int64 = Val (Num (I64 i)) @: Ty_bitv S64 - - let const_f32 (f : Float32.t) : float32 = - Val (Num (F32 (Float32.to_bits f))) @: Ty_fp S32 +type vbool = Expr.t - let const_f64 (f : Float64.t) : float64 = - Val (Num (F64 (Float64.to_bits f))) @: Ty_fp S64 +type int32 = Expr.t - let ref_null _ty = Ref (Funcref None) +type int64 = Expr.t - let ref_func f : t = Ref (Funcref (Some f)) +type float32 = Expr.t - let ref_externref t v : t = Ref (Externref (Some (E (t, v)))) +type float64 = Expr.t - let ref_is_null = function - | Funcref (Some _) | Externref (Some _) -> Val False @: Ty_bool - | Funcref None | Externref None -> Val True @: Ty_bool +type externref = Concrete_value.externref - let pp ppf v = - let e = - match v with - | I32 e -> e - | I64 e -> e - | F32 e -> e - | F64 e -> e - | Ref _ -> assert false - in - Expr.pp ppf e +type ref_value = + | Funcref of Func_intf.t option + | Externref of externref option - module Ref = struct - let get_func (r : ref_value) : Func_intf.t Value_intf.get_ref = - match r with - | Funcref (Some f) -> Ref_value f - | Funcref None -> Null - | Externref _ -> Type_mismatch +type t = + | I32 of int32 + | I64 of int64 + | F32 of float32 + | F64 of float64 + | Ref of ref_value - let get_externref (type t) (r : ref_value) (t : t Type.Id.t) : - t Value_intf.get_ref = - match r with - | Externref (Some (E (ety, v))) -> ( - match Type.Id.provably_equal t ety with - | None -> assert false - | Some Equal -> Ref_value v ) - | _ -> assert false - end +let const_i32 (i : Int32.t) : int32 = Val (Num (I32 i)) @: Ty_bitv S32 - module Bool = struct - let of_val = function - | Val True -> Some true - | Val False -> Some false - | _ -> None +let const_i64 (i : Int64.t) : int64 = Val (Num (I64 i)) @: Ty_bitv S64 - let const b = Val (if b then True else False) @: Ty_bool +let const_f32 (f : Float32.t) : float32 = + Val (Num (F32 (Float32.to_bits f))) @: Ty_fp S32 - let not e = - match e.node.e with - | Unop (Not, cond) -> cond - | e' -> - Option.value ~default:(Unop (Not, e) @: Ty_bool) - @@ let+ b = of_val e' in - const (not b) +let const_f64 (f : Float64.t) : float64 = + Val (Num (F64 (Float64.to_bits f))) @: Ty_fp S64 - let or_ e1 e2 = - match (of_val e1.node.e, of_val e2.node.e) with - | Some b1, Some b2 -> const (b1 || b2) - | Some false, _ -> e2 - | _, Some false -> e1 - | Some true, _ | _, Some true -> const true - | _ -> Binop (Or, e1, e2) @: Ty_bool +let ref_null _ty = Ref (Funcref None) - let and_ e1 e2 = - match (of_val e1.node.e, of_val e2.node.e) with - | Some b1, Some b2 -> const (b1 && b2) - | Some true, _ -> e2 - | _, Some true -> e1 - | Some false, _ | _, Some false -> const false - | _ -> Binop (And, e1, e2) @: Ty_bool +let ref_func f : t = Ref (Funcref (Some f)) - let int32 e = - match e.node.e with - | Val True -> const_i32 1l - | Val False -> const_i32 0l - | Cvtop (ToBool, ({ node = { ty = Ty_bitv S32; _ }; _ } as e')) -> e' - | _ -> Cvtop (OfBool, e) @: Ty_bitv S32 +let ref_externref t v : t = Ref (Externref (Some (E (t, v)))) - let select_expr c ~if_true ~if_false = - match of_val c.node.e with - | Some true -> if_true - | Some false -> if_false - | None -> Triop (Ite, c, if_true, if_false) @: Ty_bool +let ref_is_null = function + | Funcref (Some _) | Externref (Some _) -> Val False @: Ty_bool + | Funcref None | Externref None -> Val True @: Ty_bool - let pp ppf (e : vbool) = Expr.pp ppf e - end +let pp ppf v = + let e = + match v with + | I32 e -> e + | I64 e -> e + | F32 e -> e + | F64 e -> e + | Ref _ -> assert false + in + Expr.pp ppf e - module I32 = struct - type num = Expr.t +module Ref = struct + let get_func (r : ref_value) : Func_intf.t Value_intf.get_ref = + match r with + | Funcref (Some f) -> Ref_value f + | Funcref None -> Null + | Externref _ -> Type_mismatch - type vbool = Expr.t - - type const = Int64.t - - type nonrec float32 = float32 - - type nonrec float64 = float64 - - let ty = Ty_bitv S32 - - let zero = const_i32 0l - - let clz e = unop ty Clz e - - let ctz _ = failwith "i32_ctz: TODO" - - let popcnt _ = failwith "i32_popcnt: TODO" - - let add e1 e2 = binop ty Add e1 e2 - - let sub e1 e2 = binop ty Sub e1 e2 - - let mul e1 e2 = binop ty Mul e1 e2 - - let div e1 e2 = binop ty Div e1 e2 - - let unsigned_div e1 e2 = binop ty DivU e1 e2 - - let rem e1 e2 = binop ty Rem e1 e2 - - let unsigned_rem e1 e2 = binop ty RemU e1 e2 - - let boolify e = - match e.node.e with - | Val (Num (I32 0l)) -> Some (Bool.const false) - | Val (Num (I32 1l)) -> Some (Bool.const true) - | Cvtop (OfBool, cond) -> Some cond - | _ -> None - - let logand e1 e2 = - match (boolify e1, boolify e2) with - | Some b1, Some b2 -> Bool.int32 (Bool.and_ b1 b2) - | _ -> binop ty And e1 e2 + let get_externref (type t) (r : ref_value) (t : t Type.Id.t) : + t Value_intf.get_ref = + match r with + | Externref (Some (E (ety, v))) -> ( + match Type.Id.provably_equal t ety with + | None -> assert false + | Some Equal -> Ref_value v ) + | _ -> assert false +end - let logor e1 e2 = - match (boolify e1, boolify e2) with - | Some b1, Some b2 -> Bool.int32 (Bool.or_ b1 b2) - | _ -> binop ty Or e1 e2 +module Bool = struct + let of_val = function + | Val True -> Some true + | Val False -> Some false + | _ -> None + + let const b = Val (if b then True else False) @: Ty_bool + + let not e = + match e.node.e with + | Unop (Not, cond) -> cond + | e' -> + Option.value ~default:(Unop (Not, e) @: Ty_bool) + @@ let+ b = of_val e' in + const (not b) + + let or_ e1 e2 = + match (of_val e1.node.e, of_val e2.node.e) with + | Some b1, Some b2 -> const (b1 || b2) + | Some false, _ -> e2 + | _, Some false -> e1 + | Some true, _ | _, Some true -> const true + | _ -> Binop (Or, e1, e2) @: Ty_bool + + let and_ e1 e2 = + match (of_val e1.node.e, of_val e2.node.e) with + | Some b1, Some b2 -> const (b1 && b2) + | Some true, _ -> e2 + | _, Some true -> e1 + | Some false, _ | _, Some false -> const false + | _ -> Binop (And, e1, e2) @: Ty_bool + + let int32 e = + match e.node.e with + | Val True -> const_i32 1l + | Val False -> const_i32 0l + | Cvtop (ToBool, ({ node = { ty = Ty_bitv S32; _ }; _ } as e')) -> e' + | _ -> Cvtop (OfBool, e) @: Ty_bitv S32 + + let select_expr c ~if_true ~if_false = + match of_val c.node.e with + | Some true -> if_true + | Some false -> if_false + | None -> Triop (Ite, c, if_true, if_false) @: Ty_bool + + let pp ppf (e : vbool) = Expr.pp ppf e +end - let logxor e1 e2 = binop ty Xor e1 e2 +module I32 = struct + let ty = Ty_bitv S32 - let shl e1 e2 = binop ty Shl e1 e2 + let zero = const_i32 0l - let shr_s e1 e2 = binop ty ShrA e1 e2 + let clz e = unop ty Clz e - let shr_u e1 e2 = binop ty ShrL e1 e2 + let ctz _ = failwith "i32_ctz: TODO" - let rotl e1 e2 = binop ty Rotl e1 e2 + let popcnt _ = failwith "i32_popcnt: TODO" - let rotr e1 e2 = binop ty Rotr e1 e2 + let add e1 e2 = binop ty Add e1 e2 - let eq_const e c = - match e.node.e with - | Cvtop (OfBool, cond) -> begin - match c with 0l -> Bool.not cond | 1l -> cond | _ -> Bool.const false - end - | _ -> relop ty Eq e (const_i32 c) + let sub e1 e2 = binop ty Sub e1 e2 - let eq e1 e2 = if e1 == e2 then Bool.const true else relop ty Eq e1 e2 + let mul e1 e2 = binop ty Mul e1 e2 - let ne e1 e2 = if e1 == e2 then Bool.const false else relop ty Ne e1 e2 + let div e1 e2 = binop ty Div e1 e2 - let lt e1 e2 = if e1 == e2 then Bool.const false else relop ty Lt e1 e2 + let unsigned_div e1 e2 = binop ty DivU e1 e2 - let gt e1 e2 = if e1 == e2 then Bool.const false else relop ty Gt e1 e2 + let rem e1 e2 = binop ty Rem e1 e2 - let lt_u e1 e2 = if e1 == e2 then Bool.const false else relop ty LtU e1 e2 + let unsigned_rem e1 e2 = binop ty RemU e1 e2 - let gt_u e1 e2 = if e1 == e2 then Bool.const false else relop ty GtU e1 e2 + let boolify e = + match e.node.e with + | Val (Num (I32 0l)) -> Some (Bool.const false) + | Val (Num (I32 1l)) -> Some (Bool.const true) + | Cvtop (OfBool, cond) -> Some cond + | _ -> None - let le e1 e2 = if e1 == e2 then Bool.const true else relop ty Le e1 e2 + let logand e1 e2 = + match (boolify e1, boolify e2) with + | Some b1, Some b2 -> Bool.int32 (Bool.and_ b1 b2) + | _ -> binop ty And e1 e2 - let ge e1 e2 = if e1 == e2 then Bool.const true else relop ty Ge e1 e2 + let logor e1 e2 = + match (boolify e1, boolify e2) with + | Some b1, Some b2 -> Bool.int32 (Bool.or_ b1 b2) + | _ -> binop ty Or e1 e2 - let le_u e1 e2 = if e1 == e2 then Bool.const true else relop ty LeU e1 e2 + let logxor e1 e2 = binop ty Xor e1 e2 - let ge_u e1 e2 = if e1 == e2 then Bool.const true else relop ty GeU e1 e2 + let shl e1 e2 = binop ty Shl e1 e2 - let to_bool (e : vbool) = - match e.node.e with - | Val (Num (I32 i)) -> Bool.const @@ Int32.ne i 0l - | Cvtop (OfBool, cond) -> cond - | _ -> Cvtop (ToBool, e) @: ty + let shr_s e1 e2 = binop ty ShrA e1 e2 - let trunc_f32_s x = cvtop ty TruncSF32 x + let shr_u e1 e2 = binop ty ShrL e1 e2 - let trunc_f32_u x = cvtop ty TruncUF32 x + let rotl e1 e2 = binop ty Rotl e1 e2 - let trunc_f64_s x = cvtop ty TruncSF64 x + let rotr e1 e2 = binop ty Rotr e1 e2 - let trunc_f64_u x = cvtop ty TruncUF64 x + let eq_const e c = + match e.node.e with + | Cvtop (OfBool, cond) -> begin + match c with 0l -> Bool.not cond | 1l -> cond | _ -> Bool.const false + end + | _ -> relop ty Eq e (const_i32 c) - let trunc_sat_f32_s _ = assert false + let eq e1 e2 = if e1 == e2 then Bool.const true else relop ty Eq e1 e2 - let trunc_sat_f32_u _ = assert false + let ne e1 e2 = if e1 == e2 then Bool.const false else relop ty Ne e1 e2 - let trunc_sat_f64_s _ = assert false + let lt e1 e2 = if e1 == e2 then Bool.const false else relop ty Lt e1 e2 - let trunc_sat_f64_u _ = assert false + let gt e1 e2 = if e1 == e2 then Bool.const false else relop ty Gt e1 e2 - let reinterpret_f32 x = cvtop ty Reinterpret_float x + let lt_u e1 e2 = if e1 == e2 then Bool.const false else relop ty LtU e1 e2 - let wrap_i64 x = cvtop ty WrapI64 x + let gt_u e1 e2 = if e1 == e2 then Bool.const false else relop ty GtU e1 e2 - (* FIXME: This is probably wrong? *) - let extend_s n x = - cvtop ty (ExtS (32 - n)) (Extract (x, n / 8, 0) @: Ty_bitv S32) - end + let le e1 e2 = if e1 == e2 then Bool.const true else relop ty Le e1 e2 - module I64 = struct - type num = Expr.t + let ge e1 e2 = if e1 == e2 then Bool.const true else relop ty Ge e1 e2 - type vbool = Expr.t + let le_u e1 e2 = if e1 == e2 then Bool.const true else relop ty LeU e1 e2 - type const = Int64.t + let ge_u e1 e2 = if e1 == e2 then Bool.const true else relop ty GeU e1 e2 - type nonrec float32 = float32 + let to_bool (e : vbool) = + match e.node.e with + | Val (Num (I32 i)) -> Bool.const @@ Int32.ne i 0l + | Cvtop (OfBool, cond) -> cond + | _ -> Cvtop (ToBool, e) @: ty - type nonrec float64 = float64 + let trunc_f32_s x = cvtop ty TruncSF32 x - let ty = Ty_bitv S64 + let trunc_f32_u x = cvtop ty TruncUF32 x - let zero = const_i64 0L + let trunc_f64_s x = cvtop ty TruncSF64 x - let clz e = unop ty Clz e + let trunc_f64_u x = cvtop ty TruncUF64 x - let ctz _ = failwith "i64_ctz: TODO" + let trunc_sat_f32_s _ = assert false - let popcnt _ = failwith "i64_popcnt: TODO" + let trunc_sat_f32_u _ = assert false - let add e1 e2 = binop ty Add e1 e2 + let trunc_sat_f64_s _ = assert false - let sub e1 e2 = binop ty Sub e1 e2 + let trunc_sat_f64_u _ = assert false - let mul e1 e2 = binop ty Mul e1 e2 + let reinterpret_f32 x = cvtop ty Reinterpret_float x - let div e1 e2 = binop ty Div e1 e2 + let wrap_i64 x = cvtop ty WrapI64 x - let unsigned_div e1 e2 = binop ty DivU e1 e2 + (* FIXME: This is probably wrong? *) + let extend_s n x = + cvtop ty (ExtS (32 - n)) (Extract (x, n / 8, 0) @: Ty_bitv S32) +end - let rem e1 e2 = binop ty Rem e1 e2 +module I64 = struct + let ty = Ty_bitv S64 - let unsigned_rem e1 e2 = binop ty RemU e1 e2 + let zero = const_i64 0L - let logand e1 e2 = binop ty And e1 e2 + let clz e = unop ty Clz e - let logor e1 e2 = binop ty Or e1 e2 + let ctz _ = failwith "i64_ctz: TODO" - let logxor e1 e2 = binop ty Xor e1 e2 + let popcnt _ = failwith "i64_popcnt: TODO" - let shl e1 e2 = binop ty Shl e1 e2 + let add e1 e2 = binop ty Add e1 e2 - let shr_s e1 e2 = binop ty ShrA e1 e2 + let sub e1 e2 = binop ty Sub e1 e2 - let shr_u e1 e2 = binop ty ShrL e1 e2 + let mul e1 e2 = binop ty Mul e1 e2 - let rotl e1 e2 = binop ty Rotl e1 e2 + let div e1 e2 = binop ty Div e1 e2 - let rotr e1 e2 = binop ty Rotr e1 e2 + let unsigned_div e1 e2 = binop ty DivU e1 e2 - let eq_const e c = relop ty Eq e (const_i64 c) + let rem e1 e2 = binop ty Rem e1 e2 - let eq e1 e2 = relop ty Eq e1 e2 + let unsigned_rem e1 e2 = binop ty RemU e1 e2 - let ne e1 e2 = relop ty Ne e1 e2 + let logand e1 e2 = binop ty And e1 e2 - let lt e1 e2 = relop ty Lt e1 e2 + let logor e1 e2 = binop ty Or e1 e2 - let gt e1 e2 = relop ty Gt e1 e2 + let logxor e1 e2 = binop ty Xor e1 e2 - let lt_u e1 e2 = relop ty LtU e1 e2 + let shl e1 e2 = binop ty Shl e1 e2 - let gt_u e1 e2 = relop ty GtU e1 e2 + let shr_s e1 e2 = binop ty ShrA e1 e2 - let le e1 e2 = relop ty Le e1 e2 + let shr_u e1 e2 = binop ty ShrL e1 e2 - let ge e1 e2 = relop ty Ge e1 e2 + let rotl e1 e2 = binop ty Rotl e1 e2 - let le_u e1 e2 = relop ty LeU e1 e2 + let rotr e1 e2 = binop ty Rotr e1 e2 - let ge_u e1 e2 = relop ty GeU e1 e2 + let eq_const e c = relop ty Eq e (const_i64 c) - let of_int32 e = cvtop ty (ExtS 32) e + let eq e1 e2 = relop ty Eq e1 e2 - let to_int32 e = cvtop (Ty_bitv S32) WrapI64 e + let ne e1 e2 = relop ty Ne e1 e2 - let trunc_f32_s x = cvtop ty TruncSF32 x + let lt e1 e2 = relop ty Lt e1 e2 - let trunc_f32_u x = cvtop ty TruncUF32 x + let gt e1 e2 = relop ty Gt e1 e2 - let trunc_f64_s x = cvtop ty TruncSF64 x + let lt_u e1 e2 = relop ty LtU e1 e2 - let trunc_f64_u x = cvtop ty TruncUF64 x + let gt_u e1 e2 = relop ty GtU e1 e2 - let trunc_sat_f32_s _ = assert false + let le e1 e2 = relop ty Le e1 e2 - let trunc_sat_f32_u _ = assert false + let ge e1 e2 = relop ty Ge e1 e2 - let trunc_sat_f64_s _ = assert false + let le_u e1 e2 = relop ty LeU e1 e2 - let trunc_sat_f64_u _ = assert false + let ge_u e1 e2 = relop ty GeU e1 e2 - let reinterpret_f64 x = cvtop ty Reinterpret_float x + let of_int32 e = cvtop ty (ExtS 32) e - (* FIXME: This is probably wrong? *) - let extend_s n x = - cvtop ty (ExtS (64 - n)) (Extract (x, n / 8, 0) @: Ty_bitv S64) + let to_int32 e = cvtop (Ty_bitv S32) WrapI64 e - let extend_i32_s x = cvtop ty (ExtS 32) x + let trunc_f32_s x = cvtop ty TruncSF32 x - let extend_i32_u x = cvtop ty (ExtU 32) x - end + let trunc_f32_u x = cvtop ty TruncUF32 x - module F32 = struct - type num = Expr.t + let trunc_f64_s x = cvtop ty TruncSF64 x - type vbool = Expr.t + let trunc_f64_u x = cvtop ty TruncUF64 x - type nonrec int32 = int32 + let trunc_sat_f32_s _ = assert false - type nonrec int64 = int64 + let trunc_sat_f32_u _ = assert false - type same_size_int = int32 + let trunc_sat_f64_s _ = assert false - let ty = Ty_fp S32 + let trunc_sat_f64_u _ = assert false - let zero = const_f32 Float32.zero + let reinterpret_f64 x = cvtop ty Reinterpret_float x - let abs x = unop ty Abs x + (* FIXME: This is probably wrong? *) + let extend_s n x = + cvtop ty (ExtS (64 - n)) (Extract (x, n / 8, 0) @: Ty_bitv S64) - let neg x = unop ty Neg x + let extend_i32_s x = cvtop ty (ExtS 32) x - let sqrt x = unop ty Sqrt x + let extend_i32_u x = cvtop ty (ExtU 32) x +end - let ceil x = unop ty Ceil x +module F32 = struct + let ty = Ty_fp S32 - let floor x = unop ty Floor x + let zero = const_f32 Float32.zero - let trunc x = unop ty Trunc x + let abs x = unop ty Abs x - let nearest x = unop ty Nearest x + let neg x = unop ty Neg x - let add x y = binop ty Add x y + let sqrt x = unop ty Sqrt x - let sub x y = binop ty Sub x y + let ceil x = unop ty Ceil x - let mul x y = binop ty Mul x y + let floor x = unop ty Floor x - let div x y = binop ty Div x y + let trunc x = unop ty Trunc x - let min x y = binop ty Min x y + let nearest x = unop ty Nearest x - let max x y = binop ty Max x y + let add x y = binop ty Add x y - let copy_sign _ _ = assert false + let sub x y = binop ty Sub x y - let eq x y = relop ty Eq x y + let mul x y = binop ty Mul x y - let ne x y = relop ty Ne x y + let div x y = binop ty Div x y - let lt x y = relop ty Lt x y + let min x y = binop ty Min x y - let gt x y = relop ty Gt x y + let max x y = binop ty Max x y - let le x y = relop ty Le x y + let copy_sign _ _ = assert false - let ge x y = relop ty Ge x y + let eq x y = relop ty Eq x y - let convert_i32_s x = cvtop ty ConvertSI32 x + let ne x y = relop ty Ne x y - let convert_i32_u x = cvtop ty ConvertUI32 x + let lt x y = relop ty Lt x y - let convert_i64_s x = cvtop ty ConvertSI64 x + let gt x y = relop ty Gt x y - let convert_i64_u x = cvtop ty ConvertUI64 x + let le x y = relop ty Le x y - let demote_f64 x = cvtop ty DemoteF64 x + let ge x y = relop ty Ge x y - let reinterpret_i32 x = cvtop ty Reinterpret_int x + let convert_i32_s x = cvtop ty ConvertSI32 x - let of_bits x = cvtop ty Reinterpret_int x + let convert_i32_u x = cvtop ty ConvertUI32 x - let to_bits x = cvtop (Ty_bitv S32) Reinterpret_float x - end + let convert_i64_s x = cvtop ty ConvertSI64 x - module F64 = struct - type num = Expr.t + let convert_i64_u x = cvtop ty ConvertUI64 x - type vbool = Expr.t + let demote_f64 x = cvtop ty DemoteF64 x - type nonrec int32 = int32 + let reinterpret_i32 x = cvtop ty Reinterpret_int x - type nonrec int64 = int64 + let of_bits x = cvtop ty Reinterpret_int x - type same_size_int = int64 + let to_bits x = cvtop (Ty_bitv S32) Reinterpret_float x +end - let ty = Ty_fp S64 +module F64 = struct + let ty = Ty_fp S64 - let zero = const_f64 Float64.zero + let zero = const_f64 Float64.zero - let abs x = unop ty Abs x + let abs x = unop ty Abs x - let neg x = unop ty Neg x + let neg x = unop ty Neg x - let sqrt x = unop ty Sqrt x + let sqrt x = unop ty Sqrt x - let ceil x = unop ty Ceil x + let ceil x = unop ty Ceil x - let floor x = unop ty Floor x + let floor x = unop ty Floor x - let trunc x = unop ty Trunc x + let trunc x = unop ty Trunc x - let nearest x = unop ty Nearest x + let nearest x = unop ty Nearest x - let add x y = binop ty Add x y + let add x y = binop ty Add x y - let sub x y = binop ty Sub x y + let sub x y = binop ty Sub x y - let mul x y = binop ty Mul x y + let mul x y = binop ty Mul x y - let div x y = binop ty Div x y + let div x y = binop ty Div x y - let min x y = binop ty Min x y + let min x y = binop ty Min x y - let max x y = binop ty Max x y + let max x y = binop ty Max x y - let copy_sign _ _ = assert false + let copy_sign _ _ = assert false - let eq x y = relop ty Eq x y + let eq x y = relop ty Eq x y - let ne x y = relop ty Ne x y + let ne x y = relop ty Ne x y - let lt x y = relop ty Lt x y + let lt x y = relop ty Lt x y - let gt x y = relop ty Gt x y + let gt x y = relop ty Gt x y - let le x y = relop ty Le x y + let le x y = relop ty Le x y - let ge x y = relop ty Ge x y + let ge x y = relop ty Ge x y - let convert_i32_s x = cvtop ty ConvertSI32 x + let convert_i32_s x = cvtop ty ConvertSI32 x - let convert_i32_u x = cvtop ty ConvertUI32 x + let convert_i32_u x = cvtop ty ConvertUI32 x - let convert_i64_s x = cvtop ty ConvertSI64 x + let convert_i64_s x = cvtop ty ConvertSI64 x - let convert_i64_u x = cvtop ty ConvertUI64 x + let convert_i64_u x = cvtop ty ConvertUI64 x - let promote_f32 x = cvtop ty PromoteF32 x + let promote_f32 x = cvtop ty PromoteF32 x - let reinterpret_i64 x = cvtop ty Reinterpret_int x + let reinterpret_i64 x = cvtop ty Reinterpret_int x - let of_bits x = cvtop ty Reinterpret_int x + let of_bits x = cvtop ty Reinterpret_int x - let to_bits x = cvtop (Ty_bitv S64) Reinterpret_float x - end + let to_bits x = cvtop (Ty_bitv S64) Reinterpret_float x end - -module S' : Value_intf.T = S diff --git a/src/symbolic_value.mli b/src/symbolic_value.mli new file mode 100644 index 000000000..b7c180079 --- /dev/null +++ b/src/symbolic_value.mli @@ -0,0 +1,24 @@ +type externref + +type ref_value = + | Funcref of Func_intf.t option + | Externref of externref option + +include + Value_intf.T + with type ref_value := ref_value + with type vbool = Encoding.Expr.t + and type int32 = Encoding.Expr.t + and type int64 = Encoding.Expr.t + and type float32 = Encoding.Expr.t + and type float64 = Encoding.Expr.t + +module Bool : sig + include module type of Bool + + val select_expr : + Encoding.Expr.t + -> if_true:Encoding.Expr.t + -> if_false:Encoding.Expr.t + -> Encoding.Expr.t +end diff --git a/src/thread.ml b/src/thread.ml index d0351ee9f..7e2276824 100644 --- a/src/thread.ml +++ b/src/thread.ml @@ -5,10 +5,10 @@ type t = { choices : int ; mutable symbol_set : Encoding.Symbol.t list - ; pc : Symbolic_value.S.vbool list - ; memories : Symbolic_memory.memories - ; tables : Symbolic_table.tables - ; globals : Symbolic_global.globals + ; pc : Symbolic_value.vbool list + ; memories : Symbolic_memory.collection + ; tables : Symbolic_table.collection + ; globals : Symbolic_global.collection } let pc t = t.pc