Skip to content

V128: proper symbolic and concolic handling #698

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 4 commits into from
Jun 5, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
13 changes: 13 additions & 0 deletions src/cmd/cmd_replay.ml
Original file line number Diff line number Diff line change
Expand Up @@ -122,6 +122,16 @@ let run_file ~unsafe ~optimize ~entry_point ~invoke_with_symbols filename model
Logs.err (fun m -> m "Got value %a but expected a f64 value." V.pp v);
assert false

let symbol_v128 () =
let i = next () in
match model.(i) with
| V.V128 n ->
add_sym i;
Ok n
| v ->
Logs.err (fun m -> m "Got value %a but expected a v128 value." V.pp v);
assert false

let symbol_range _ _ =
let i = next () in
match model.(i) with
Expand Down Expand Up @@ -191,6 +201,9 @@ let run_file ~unsafe ~optimize ~entry_point ~invoke_with_symbols filename model
; ( "f64_symbol"
, Concrete_extern_func.Extern_func (Func (UArg Res, R1 F64), symbol_f64)
)
; ( "v128_symbol"
, Concrete_extern_func.Extern_func
(Func (UArg Res, R1 V128), symbol_v128) )
; ( "bool_symbol"
, Concrete_extern_func.Extern_func (Func (UArg Res, R1 I32), symbol_bool)
)
Expand Down
7 changes: 6 additions & 1 deletion src/cmd/cmd_utils.ml
Original file line number Diff line number Diff line change
Expand Up @@ -73,13 +73,18 @@ let default_symbol_of_t m =
let desc = Types.Bt_raw (None, ([], [ Types.Num_type Types.F64 ])) in
Binary.Module.add_import_if_not_present ~modul_name ~func_name ~desc m
in
let v128_symbol, m =
let func_name = "v128_symbol" in
let desc = Types.Bt_raw (None, ([], [ Types.Num_type Types.V128 ])) in
Binary.Module.add_import_if_not_present ~modul_name ~func_name ~desc m
in
( m
, function
| Types.Num_type I32 -> Ok (Types.Call i32_symbol)
| Num_type I64 -> Ok (Types.Call i64_symbol)
| Num_type F32 -> Ok (Types.Call f32_symbol)
| Num_type F64 -> Ok (Types.Call f64_symbol)
| Num_type V128 -> Fmt.error_msg "TODO default_symbol_of_t V128"
| Num_type V128 -> Ok (Types.Call v128_symbol)
| Ref_type t ->
Fmt.error_msg "can not create default symbol of type %a" Types.pp_ref_type
t )
Expand Down
1 change: 1 addition & 0 deletions src/concolic/concolic_value.mli
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ include
and type int64 = Concrete.Value.int64 * Symbolic_value.int64
and type float32 = Concrete.Value.float32 * Symbolic_value.float32
and type float64 = Concrete.Value.float64 * Symbolic_value.float64
and type v128 = Concrete.Value.v128 * Symbolic_value.v128
and type ref_value = Concrete.Value.ref_value * Symbolic_value.ref_value

module Bool : sig
Expand Down
20 changes: 20 additions & 0 deletions src/concolic/concolic_wasm_ffi.ml
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,23 @@ module M :
let n = Float64.of_bits n in
(F64 n, (n, Expr.symbol sym)) )

let symbol_v128 () : Value.v128 Concolic_choice.t =
Concolic_choice.with_new_symbol (Ty_bitv 128) (fun sym forced_value ->
let a, b =
match forced_value with
| None ->
let a = Random.bits64 () in
let b = Random.bits64 () in
(a, b)
| Some (Bitv n) ->
let a = Smtml.Bitvector.extract n ~low:8 ~high:16 in
let b = Smtml.Bitvector.extract n ~low:0 ~high:8 in
(Smtml.Bitvector.to_int64 a, Smtml.Bitvector.to_int64 b)
| _ -> assert false
in
let n = V128.of_i64x2 a b in
(V128 n, (n, Expr.symbol sym)) )

let symbol_invisible_bool () : Value.int32 Concolic_choice.t =
Concolic_choice.with_new_invisible_symbol Ty_bool
(fun sym (forced_value : Smtml.Value.t option) ->
Expand Down Expand Up @@ -193,6 +210,9 @@ let symbolic_extern_module =
; ( "f64_symbol"
, Concolic.Extern_func.Extern_func (Func (UArg Res, R1 F64), symbol_f64)
)
; ( "v128_symbol"
, Concolic.Extern_func.Extern_func (Func (UArg Res, R1 V128), symbol_v128)
)
; ( "bool_symbol"
, Concolic.Extern_func.Extern_func (Func (UArg Res, R1 I32), symbol_bool)
)
Expand Down
2 changes: 2 additions & 0 deletions src/concrete/concrete_extern_func.ml
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,8 @@ include

type float64 = Float64.t

type v128 = V128.t

type bool = Bool.t
end)
(struct
Expand Down
2 changes: 2 additions & 0 deletions src/interpret/interpret.ml
Original file line number Diff line number Diff line change
Expand Up @@ -536,6 +536,7 @@ module Make (P : Interpret_intf.P) :
| I64 -> Choice.return @@ Stack.pop_i64 stack
| F32 -> Choice.return @@ Stack.pop_f32 stack
| F64 -> Choice.return @@ Stack.pop_f64 stack
| V128 -> Choice.return @@ Stack.pop_v128 stack
| Externref ety -> (
let v, stack = Stack.pop_as_ref stack in
match Ref.get_externref v ety with
Expand Down Expand Up @@ -583,6 +584,7 @@ module Make (P : Interpret_intf.P) :
| I64 -> Stack.push_i64 stack v
| F32 -> Stack.push_f32 stack v
| F64 -> Stack.push_f64 stack v
| V128 -> Stack.push_v128 stack v
| Externref ty -> Stack.push_as_externref stack ty v
in
let+ r in
Expand Down
8 changes: 8 additions & 0 deletions src/intf/func_intf.ml
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,8 @@ module type Value_types = sig

type float64

type v128

type bool
end

Expand All @@ -33,6 +35,8 @@ module type T_Extern_func = sig

type float64

type v128

type 'a m

type memory
Expand All @@ -42,6 +46,7 @@ module type T_Extern_func = sig
| I64 : int64 telt
| F32 : float32 telt
| F64 : float64 telt
| V128 : v128 telt
| Externref : 'a Type.Id.t -> 'a telt

type _ rtype =
Expand Down Expand Up @@ -96,6 +101,7 @@ module Make_extern_func
and type int64 := V.int64
and type float32 := V.float32
and type float64 := V.float64
and type v128 := V.v128
and type 'a m := 'a M.t
and type memory := Memory.t
end = struct
Expand All @@ -108,6 +114,7 @@ end = struct
| I64 : V.int64 telt
| F32 : V.float32 telt
| F64 : V.float64 telt
| V128 : V.v128 telt
| Externref : 'a Type.Id.t -> 'a telt

type _ rtype =
Expand All @@ -134,6 +141,7 @@ end = struct
| I64 -> Num_type I64
| F32 -> Num_type F32
| F64 -> Num_type F64
| V128 -> Num_type V128
| Externref _ -> Ref_type (Null, Extern_ht)

let res_type (type t) (r : t rtype) : binary result_type =
Expand Down
1 change: 1 addition & 0 deletions src/intf/interpret_intf.ml
Original file line number Diff line number Diff line change
Expand Up @@ -97,6 +97,7 @@ module type P = sig
and type int64 := Value.int64
and type float32 := Value.float32
and type float64 := Value.float64
and type v128 := Value.v128
and type 'a m := 'a Choice.t
and type memory := Memory.t

Expand Down
4 changes: 4 additions & 0 deletions src/intf/wasm_ffi_intf.ml
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,8 @@ module type S0 = sig
type float32

type float64

type v128
end

val symbol_i8 : unit -> Value.int32 t
Expand All @@ -29,6 +31,8 @@ module type S0 = sig

val symbol_f64 : unit -> Value.float64 t

val symbol_v128 : unit -> Value.v128 t

val symbol_invisible_bool : unit -> Value.int32 t

val symbol_bool : unit -> Value.int32 t
Expand Down
23 changes: 16 additions & 7 deletions src/symbolic/symbolic_value.ml
Original file line number Diff line number Diff line change
Expand Up @@ -24,9 +24,9 @@ type float64 = Expr.t

let pp_float64 = Expr.pp

type v128 = int64 * int64
type v128 = Expr.t

let pp_v128 fmt (a, b) = Fmt.pf fmt "(%a,%a)" pp_int64 a pp_int64 b
let pp_v128 = Expr.pp

type externref = V.externref

Expand Down Expand Up @@ -56,7 +56,7 @@ let const_f64 (f : Float64.t) : float64 = value (Num (F64 (Float64.to_bits f)))

let const_v128 (v : V128.t) : v128 =
let a, b = V128.to_i64x2 v in
(const_i64 a, const_i64 b)
Smtml.Expr.concat (const_i64 a) (const_i64 b)

let ref_null _ty = Ref (Funcref None)

Expand Down Expand Up @@ -482,11 +482,20 @@ end
module V128 = struct
let zero : v128 = const_v128 V128.zero

let of_i32x4 _ = assert false (* TODO *)
let of_i32x4 a b c d =
Smtml.Expr.concat (Smtml.Expr.concat a b) (Smtml.Expr.concat c d)

let to_i32x4 _ = assert false (* TODO *)
let to_i32x4 v =
let a = Smtml.Expr.extract v ~low:12 ~high:16 in
let b = Smtml.Expr.extract v ~low:8 ~high:12 in
let c = Smtml.Expr.extract v ~low:4 ~high:8 in
let d = Smtml.Expr.extract v ~low:0 ~high:4 in
(a, b, c, d)

let of_i64x2 _ = assert false (* TODO *)
let of_i64x2 a b = Smtml.Expr.concat a b

let to_i64x2 _ = assert false (* TODO *)
let to_i64x2 v =
let a = Smtml.Expr.extract v ~low:8 ~high:16 in
let b = Smtml.Expr.extract v ~low:0 ~high:8 in
(a, b)
end
2 changes: 1 addition & 1 deletion src/symbolic/symbolic_value.mli
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ include
and type int64 = Smtml.Expr.t
and type float32 = Smtml.Expr.t
and type float64 = Smtml.Expr.t
and type v128 = Smtml.Expr.t * Smtml.Expr.t
and type v128 = Smtml.Expr.t

module Bool : sig
include module type of Bool
Expand Down
5 changes: 5 additions & 0 deletions src/symbolic/symbolic_wasm_ffi.ml
Original file line number Diff line number Diff line change
Expand Up @@ -63,6 +63,8 @@ end = struct

let symbol_f64 () = Choice.with_new_symbol (Ty_fp 64) Expr.symbol

let symbol_v128 () = Choice.with_new_symbol (Ty_bitv 128) Expr.symbol

let symbol_range (lo : Value.int32) (hi : Value.int32) =
let open Choice in
let* x = symbol_i32 () in
Expand Down Expand Up @@ -168,6 +170,9 @@ let symbolic_extern_module =
; ( "f64_symbol"
, Symbolic.Extern_func.Extern_func (Func (UArg Res, R1 F64), symbol_f64)
)
; ( "v128_symbol"
, Symbolic.Extern_func.Extern_func (Func (UArg Res, R1 V128), symbol_v128)
)
; ( "bool_symbol"
, Symbolic.Extern_func.Extern_func (Func (UArg Res, R1 I32), symbol_bool)
)
Expand Down
2 changes: 1 addition & 1 deletion test/replay/alloc.t
Original file line number Diff line number Diff line change
Expand Up @@ -22,7 +22,7 @@
owi: [INFO] stack : [ ]
owi: [INFO] running instr : data.drop 0
owi: [INFO] stack : [ ]
owi: [INFO] running instr : call 12
owi: [INFO] running instr : call 13
owi: [INFO] calling func : func anonymous
owi: [INFO] stack : [ ]
owi: [INFO] running instr : i32.const 0
Expand Down
2 changes: 1 addition & 1 deletion test/sym/print_pc.t
Original file line number Diff line number Diff line change
Expand Up @@ -86,7 +86,7 @@
owi: [INFO] linking ...
owi: [INFO] interpreting ...
owi: [INFO] stack : [ ]
owi: [INFO] running instr : call 5
owi: [INFO] running instr : call 6
owi: [DEBUG] path condition: [ ]
owi: [INFO] calling func : func anonymous
owi: [INFO] stack : [ ]
Expand Down
Loading