remove unused owi functions

OCamlPro · Aug 27, 2024 · 1f0da35 · 1f0da35
1 parent 2fa36b7
commit 1f0da35
Show file tree

Hide file tree

Showing 4 changed files with 26 additions and 57 deletions.
diff --git a/src/ast/code_generator.ml b/src/ast/code_generator.ml
@@ -680,14 +680,7 @@ let add_owi_funcs (owi_funcs : (string * binary func_type) array) (m : modul) :
 
 let generate (symbolic : bool) (m : modul) : modul Result.t =
   let owi_funcs =
-    if symbolic then
-      [| ("i32_symbol", ([], [ Num_type I32 ]))
-       ; ("i64_symbol", ([], [ Num_type I64 ]))
-       ; ("f32_symbol", ([], [ Num_type F32 ]))
-       ; ("f64_symbol", ([], [ Num_type F64 ]))
-       ; ("assume", ([ (None, Num_type I32) ], []))
-       ; ("assert", ([ (None, Num_type I32) ], []))
-      |]
+    if symbolic then [| ("assert", ([ (None, Num_type I32) ], [])) |]
     else [| ("assert", ([ (None, Num_type I32) ], [])) |]
   in
   let m, owi_funcs = add_owi_funcs owi_funcs m in

diff --git a/test/weasel/forall.t b/test/weasel/forall.t
@@ -40,18 +40,10 @@
   $ owi instrument forall.wat --symbolic
   $ cat forall.instrumented.wat
   (module
-    (import "symbolic" "i32_symbol" (func $i32_symbol  (result i32)))
-    (import "symbolic" "i64_symbol" (func $i64_symbol  (result i64)))
-    (import "symbolic" "f32_symbol" (func $f32_symbol  (result f32)))
-    (import "symbolic" "f64_symbol" (func $f64_symbol  (result f64)))
-    (import "symbolic" "assume" (func $assume  (param i32)))
     (import "symbolic" "assert" (func $assert  (param i32)))
     (type (sub final  (func)))
-    (type (sub final  (func (result i32))))
-    (type (sub final  (func (result i64))))
-    (type (sub final  (func (result f32))))
-    (type (sub final  (func (result f64))))
     (type (sub final  (func (param i32))))
+    (type (sub final  (func (result i32))))
     (type (sub final  (func (param i32) (result i32))))
     (func $start
 
@@ -79,10 +71,10 @@
           i32.const 10
           i32.le_s
           br_if 0))
-      call 5
-      call 6
+      call 0
+      call 1
     )
-    (start 7)
+    (start 2)
   )
   $ owi sym forall.wat --rac --debug
   parsing      ...
@@ -519,7 +511,7 @@
   linking      ...
   interpreting ...
   stack        : [  ]
-  running instr: call 7
+  running instr: call 2
   calling func : func __weasel_start
   stack        : [  ]
   running instr: (block $__weasel_forall (result i32)
@@ -912,9 +904,9 @@
   stack        : [ (i32 1) ]
   stack        : [ (i32 1) ]
   stack        : [ (i32 1) ]
-  running instr: call 5
+  running instr: call 0
   stack        : [  ]
-  running instr: call 6
+  running instr: call 1
   calling func : func start
   stack        : [  ]
   stack        : [  ]

diff --git a/test/weasel/plus.t b/test/weasel/plus.t
@@ -33,42 +33,34 @@
   $ owi instrument plus.wat --symbolic
   $ cat plus.instrumented.wat
   (module
-    (import "symbolic" "i32_symbol" (func $i32_symbol  (result i32)))
-    (import "symbolic" "i64_symbol" (func $i64_symbol  (result i64)))
-    (import "symbolic" "f32_symbol" (func $f32_symbol  (result f32)))
-    (import "symbolic" "f64_symbol" (func $f64_symbol  (result f64)))
-    (import "symbolic" "assume" (func $assume  (param i32)))
     (import "symbolic" "assert" (func $assert  (param i32)))
     (type (sub final  (func (param $x i32) (result i32))))
     (type (sub final  (func)))
-    (type (sub final  (func (result i32))))
-    (type (sub final  (func (result i64))))
-    (type (sub final  (func (result f32))))
-    (type (sub final  (func (result f64))))
     (type (sub final  (func (param i32))))
+    (type (sub final  (func (result i32))))
     (func $plus_three (param $x i32) (result i32)
       i32.const 3
       local.get 0
       i32.add
     )
     (func $start
       i32.const 42
-      call 8
+      call 3
       drop
     )
     (func $__weasel_plus_three (param $x i32) (result i32) (local $__weasel_temp i32) (local $__weasel_res_0 i32)
       local.get 0
-      call 6
+      call 1
       local.set 2
       local.get 2
       local.get 0
       i32.const 3
       i32.add
       i32.eq
-      call 5
+      call 0
       local.get 2
     )
-    (start 7)
+    (start 2)
   )
   $ owi sym plus.wat --rac --debug
   parsing      ...
@@ -143,17 +135,17 @@
   linking      ...
   interpreting ...
   stack        : [  ]
-  running instr: call 7
+  running instr: call 2
   calling func : func start
   stack        : [  ]
   running instr: i32.const 42
   stack        : [ (i32 42) ]
-  running instr: call 8
+  running instr: call 3
   calling func : func __weasel_plus_three
   stack        : [  ]
   running instr: local.get 0
   stack        : [ (i32 42) ]
-  running instr: call 6
+  running instr: call 1
   calling func : func plus_three
   stack        : [  ]
   running instr: i32.const 3
@@ -175,7 +167,7 @@
   stack        : [ (i32 45) ; (i32 45) ]
   running instr: i32.eq
   stack        : [ (i32 1) ]
-  running instr: call 5
+  running instr: call 0
   stack        : [  ]
   running instr: local.get 2
   stack        : [ (i32 45) ]

diff --git a/test/weasel/sum.t b/test/weasel/sum.t
@@ -48,19 +48,11 @@
   $ owi instrument sum.wat --symbolic
   $ cat sum.instrumented.wat
   (module
-    (import "symbolic" "i32_symbol" (func $i32_symbol  (result i32)))
-    (import "symbolic" "i64_symbol" (func $i64_symbol  (result i64)))
-    (import "symbolic" "f32_symbol" (func $f32_symbol  (result f32)))
-    (import "symbolic" "f64_symbol" (func $f64_symbol  (result f64)))
-    (import "symbolic" "assume" (func $assume  (param i32)))
     (import "symbolic" "assert" (func $assert  (param i32)))
     (type (sub final  (func (param $p1 i32) (param $p2 i32) (param $p3 i32) (param $p4 i32) (result i32))))
     (type (sub final  (func)))
-    (type (sub final  (func (result i32))))
-    (type (sub final  (func (result i64))))
-    (type (sub final  (func (result f32))))
-    (type (sub final  (func (result f64))))
     (type (sub final  (func (param i32))))
+    (type (sub final  (func (result i32))))
     (type (sub final  (func (param i32) (result i32))))
     (func $sum (param $p1 i32) (param $p2 i32) (param $p3 i32) (param $p4 i32) (result i32)
       local.get 0
@@ -76,15 +68,15 @@
       i32.const 42
       i32.const 42
       i32.const 42
-      call 8
+      call 3
       drop
     )
     (func $__weasel_sum (param $p1 i32) (param $p2 i32) (param $p3 i32) (param $p4 i32) (result i32) (local $__weasel_temp i32) (local $__weasel_res_0 i32)
       local.get 0
       local.get 1
       local.get 2
       local.get 3
-      call 6
+      call 1
       local.set 5
       local.get 5
       local.get 0
@@ -95,10 +87,10 @@
       i32.add
       i32.add
       i32.eq
-      call 5
+      call 0
       local.get 5
     )
-    (start 7)
+    (start 2)
   )
   $ owi sym sum.wat --rac --debug
   parsing      ...
@@ -201,7 +193,7 @@
   linking      ...
   interpreting ...
   stack        : [  ]
-  running instr: call 7
+  running instr: call 2
   calling func : func start
   stack        : [  ]
   running instr: i32.const 42
@@ -212,7 +204,7 @@
   stack        : [ (i32 42) ; (i32 42) ; (i32 42) ]
   running instr: i32.const 42
   stack        : [ (i32 42) ; (i32 42) ; (i32 42) ; (i32 42) ]
-  running instr: call 8
+  running instr: call 3
   calling func : func __weasel_sum
   stack        : [  ]
   running instr: local.get 0
@@ -223,7 +215,7 @@
   stack        : [ (i32 42) ; (i32 42) ; (i32 42) ]
   running instr: local.get 3
   stack        : [ (i32 42) ; (i32 42) ; (i32 42) ; (i32 42) ]
-  running instr: call 6
+  running instr: call 1
   calling func : func sum
   stack        : [  ]
   running instr: local.get 0
@@ -261,7 +253,7 @@
   stack        : [ (i32 168) ; (i32 168) ]
   running instr: i32.eq
   stack        : [ (i32 1) ]
-  running instr: call 5
+  running instr: call 0
   stack        : [  ]
   running instr: local.get 5
   stack        : [ (i32 168) ]