Skip to content
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.

Sign up for GitHub

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

Test coverage improvement #96

Closed
wants to merge 24 commits into from
Closed

Test coverage improvement #96

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
24 commits
Select commit Hold shift + click to select a range
28587a2
cmd_sym refacto (duplicate symbolic_i32 function)
epatrizio Jan 5, 2024
f4128ac
add not exists file call
epatrizio Jan 5, 2024
1db0002
reviews not exists file call
epatrizio Jan 8, 2024
36d2d98
reviews not exists file call
epatrizio Jan 8, 2024
f8ddf49
clean cmd_sym assume / print
epatrizio Jan 8, 2024
0fcd59b
init symbolic binop test
epatrizio Jan 8, 2024
b979d28
reviews (assume_extern_module and binop sym tests)
epatrizio Jan 9, 2024
842bffa
reviews (debug mess)
epatrizio Jan 9, 2024
ac117e4
add symbolic binop tests
epatrizio Jan 9, 2024
e3624bd
init symbolic unop tests
epatrizio Jan 9, 2024
4bdff80
add symbolic binop tests
epatrizio Jan 10, 2024
19040e1
add symbolic unop tests
epatrizio Jan 10, 2024
f24fdf1
some reviews
epatrizio Jan 11, 2024
3f8e387
use Domain.recommended_domain_count instead of hardcoded default number
zapashcanon Jan 8, 2024
fbebe51
Bump encoding version
filipeom Jan 11, 2024
d877c38
assume sym test review
epatrizio Jan 12, 2024
3ef2d69
add more symbolic unop tests
epatrizio Jan 12, 2024
d62cfec
assume sym test review 2
epatrizio Jan 15, 2024
24740ac
add global and memory sym test
epatrizio Jan 16, 2024
488f0a0
improve memory sym test
epatrizio Jan 16, 2024
6de1469
add table sym test
epatrizio Jan 16, 2024
afe315e
reviews (memory, table sym tests)
epatrizio Jan 17, 2024
bb7beee
reviews (memory, table sym tests)
epatrizio Jan 18, 2024
54fe69f
add more binop sym test
epatrizio Jan 19, 2024
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
25 changes: 7 additions & 18 deletions src/cmd_sym.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -9,20 +9,6 @@ let print_solver_time = false

let print_path_condition = false

let assume_extern_module : Symbolic.P.extern_func Link.extern_module =
let assume_positive_i32 (i : Value.int32) : unit Choice.t =
let c = Value.I32.ge i Value.I32.zero in
Choice.add_pc c
in
(* we need to describe their types *)
let functions =
[ ( "assume_positive_i32"
, Symbolic.P.Extern_func.Extern_func
(Func (Arg (I32, Res), R0), assume_positive_i32) )
]
in
{ functions }

let symbolic_extern_module : Symbolic.P.extern_func Link.extern_module =
let sym_cnt = Atomic.make 0 in
let mk_symbol = Encoding.Symbol.mk_symbol in
Expand All @@ -37,6 +23,10 @@ let symbolic_extern_module : Symbolic.P.extern_func Link.extern_module =
let c = Value.I32.to_bool i in
Choice.add_pc c
in
let assume_positive_i32 (i : Value.int32) : unit Choice.t =
let c = Value.I32.ge i Value.I32.zero in
Choice.add_pc c
in
let assert_i32 (i : Value.int32) : unit Choice.t =
let c = Value.I32.to_bool i in
Choice.assertion c
Expand All @@ -61,6 +51,9 @@ let symbolic_extern_module : Symbolic.P.extern_func Link.extern_module =
; ( "assume"
, Symbolic.P.Extern_func.Extern_func
(Func (Arg (I32, Res), R0), assume_i32) )
; ( "assume_positive"
, Symbolic.P.Extern_func.Extern_func
(Func (Arg (I32, Res), R0), assume_positive_i32) )
; ( "assert"
, Symbolic.P.Extern_func.Extern_func
(Func (Arg (I32, Res), R0), assert_i32) )
Expand Down Expand Up @@ -127,10 +120,6 @@ let ( let*/ ) (t : 'a Result.t) (f : 'a -> 'b Result.t Choice.t) :
let simplify_then_link_then_run ~unsafe ~optimize (pc : unit Result.t Choice.t)
file =
let link_state = Link.empty_state in
let link_state =
Link.extern_module' link_state ~name:"assume"
~func_typ:Symbolic.P.Extern_func.extern_type assume_extern_module
in
let link_state =
Link.extern_module' link_state ~name:"symbolic"
~func_typ:Symbolic.P.Extern_func.extern_type symbolic_extern_module
Expand Down
7 changes: 6 additions & 1 deletion test/sym/assume.t
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,8 @@
assume extern module:
symbolic extern module (assume and assert test):
$ dune exec owi -- sym assume.wast
CHECK:
(i32.not (i32.to_bool symbol_0))
(i32.ge symbol_0 (i32 0))
(i32.to_bool symbol_0)
/CHECK OK
All OK
6 changes: 5 additions & 1 deletion test/sym/assume.wast
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,11 +1,15 @@
(module
(import "symbolic" "i32_symbol" (func $i32_symbol (result i32)))
(import "assume" "assume_positive_i32" (func $positive_i32 (param i32)))
(import "symbolic" "assume" (func $assume_i32 (param i32)))
(import "symbolic" "assume_positive" (func $positive_i32 (param i32)))
(import "symbolic" "assert" (func $assert_i32 (param i32)))

(func $start
(local $x i32)
(local.set $x (call $i32_symbol))
(call $assume_i32 (local.get $x))
(call $positive_i32 (local.get $x))
(call $assert_i32 (local.get $x))
(if (i32.gt_s (i32.const 0) (local.get $x))
(then unreachable)))

Expand Down
21 changes: 8 additions & 13 deletions test/sym/binop_f32.wast
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,25 +3,20 @@

(func $start
(local $x f32)
(local $res f32)

(local.set $x (call $f32_symbol))

(local.set $res (f32.add (local.get $x) (f32.const 42)))
(if (f32.eq (local.get $res) (f32.const 0))
(then unreachable))
(f32.eq (f32.add (local.get $x) (f32.const 42)) (f32.const 0))
(if (then unreachable))

(local.set $res (f32.sub (local.get $x) (f32.const 42)))
(if (f32.eq (local.get $res) (f32.const 0))
(then unreachable))
(f32.eq (f32.sub (local.get $x) (f32.const 42)) (f32.const 0))
(if (then unreachable))

(local.set $res (f32.mul (local.get $x) (f32.const 42)))
(if (f32.eq (local.get $res) (f32.const 0))
(then unreachable))
(f32.eq (f32.mul (local.get $x) (f32.const 42)) (f32.const 0))
(if (then unreachable))

(local.set $res (f32.div (local.get $x) (f32.const 42)))
(if (f32.eq (local.get $res) (f32.const 0))
(then unreachable)))
(f32.eq (f32.div (local.get $x) (f32.const 42)) (f32.const 0))
(if (then unreachable)))

(start $start)
)
21 changes: 8 additions & 13 deletions test/sym/binop_f64.wast
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,25 +3,20 @@

(func $start
(local $x f64)
(local $res f64)

(local.set $x (call $f64_symbol))

(local.set $res (f64.add (local.get $x) (f64.const 42)))
(if (f64.eq (local.get $res) (f64.const 0))
(then unreachable))
(f64.eq (f64.add (local.get $x) (f64.const 42)) (f64.const 0))
(if (then unreachable))

(local.set $res (f64.sub (local.get $x) (f64.const 42)))
(if (f64.eq (local.get $res) (f64.const 0))
(then unreachable))
(f64.eq (f64.sub (local.get $x) (f64.const 42)) (f64.const 0))
(if (then unreachable))

(local.set $res (f64.mul (local.get $x) (f64.const 42)))
(if (f64.eq (local.get $res) (f64.const 0))
(then unreachable))
(f64.eq (f64.mul (local.get $x) (f64.const 42)) (f64.const 0))
(if (then unreachable))

(local.set $res (f64.div (local.get $x) (f64.const 42)))
(if (f64.eq (local.get $res) (f64.const 0))
(then unreachable)))
(f64.eq (f64.div (local.get $x) (f64.const 42)) (f64.const 0))
(if (then unreachable)))

(start $start)
)
33 changes: 16 additions & 17 deletions test/sym/binop_i32.wast
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,29 +3,28 @@

(func $start
(local $x i32)
(local $res i32)


(local.set $x (call $i32_symbol))

(local.set $res (i32.add (local.get $x) (i32.const 42)))
(if (i32.eqz (local.get $res))
(then unreachable))
(i32.add (local.get $x) (i32.const 42))
i32.eqz
(if (then unreachable))

(local.set $res (i32.sub (local.get $x) (i32.const 42)))
(if (i32.eqz (local.get $res))
(then unreachable))
(i32.sub (local.get $x) (i32.const 42))
i32.eqz
(if (then unreachable))

(local.set $res (i32.mul (local.get $x) (i32.const 42)))
(if (i32.eqz (local.get $res))
(then unreachable))
(i32.mul (local.get $x) (i32.const 42))
i32.eqz
(if (then unreachable))

(local.set $res (i32.div_u (local.get $x) (i32.const 42)))
(if (i32.eqz (local.get $res))
(then unreachable))
(i32.div_u (local.get $x) (i32.const 42))
i32.eqz
(if (then unreachable))

(local.set $res (i32.div_s (local.get $x) (i32.const 42)))
(if (i32.eqz (local.get $res))
(then unreachable)))
(i32.div_s (local.get $x) (i32.const 42))
i32.eqz
(if (then unreachable)))

(start $start)
)
31 changes: 15 additions & 16 deletions test/sym/binop_i64.wast
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -3,29 +3,28 @@

(func $start
(local $x i64)
(local $res i64)

(local.set $x (call $i64_symbol))

(local.set $res (i64.add (local.get $x) (i64.const 42)))
(if (i64.eqz (local.get $res))
(then unreachable))
(i64.add (local.get $x) (i64.const 42))
i64.eqz
(if (then unreachable))

(local.set $res (i64.sub (local.get $x) (i64.const 42)))
(if (i64.eqz (local.get $res))
(then unreachable))
(i64.sub (local.get $x) (i64.const 42))
i64.eqz
(if (then unreachable))

(local.set $res (i64.mul (local.get $x) (i64.const 42)))
(if (i64.eqz (local.get $res))
(then unreachable))
(i64.mul (local.get $x) (i64.const 42))
i64.eqz
(if (then unreachable))

(local.set $res (i64.div_u (local.get $x) (i64.const 42)))
(if (i64.eqz (local.get $res))
(then unreachable))
(i64.div_u (local.get $x) (i64.const 42))
i64.eqz
(if (then unreachable))

(local.set $res (i64.div_s (local.get $x) (i64.const 42)))
(if (i64.eqz (local.get $res))
(then unreachable)))
(i64.div_s (local.get $x) (i64.const 42))
i64.eqz
(if (then unreachable)))

(start $start)
)
Loading