fixed select parser

Generative-Program-Analysis · Mar 30, 2024 · ed262fa · ed262fa
1 parent 0e25181
commit ed262fa
Show file tree

Hide file tree

Showing 36 changed files with 4,922 additions and 4,627 deletions.
diff --git a/benchmarks/.cache/clangd/index/maze_test.c.1B2CC30026BE0FDE.idx b/benchmarks/.cache/clangd/index/maze_test.c.1B2CC30026BE0FDE.idx
diff --git a/benchmarks/.cache/clangd/index/multipath_1024_sym.c.90139B4C320D93CE.idx b/benchmarks/.cache/clangd/index/multipath_1024_sym.c.90139B4C320D93CE.idx
diff --git a/benchmarks/.cache/clangd/index/multipath_1048576_sym.c.22F45474979E6CE9.idx b/benchmarks/.cache/clangd/index/multipath_1048576_sym.c.22F45474979E6CE9.idx
diff --git a/benchmarks/.cache/clangd/index/multipath_65536_sym.c.F4273C634D39D72B.idx b/benchmarks/.cache/clangd/index/multipath_65536_sym.c.F4273C634D39D72B.idx
diff --git a/benchmarks/.cache/clangd/index/regexp.c.C838878EC181859D.idx b/benchmarks/.cache/clangd/index/regexp.c.C838878EC181859D.idx
diff --git a/benchmarks/.cache/clangd/index/sort.c.EA45F9DFDC3C894E.idx b/benchmarks/.cache/clangd/index/sort.c.EA45F9DFDC3C894E.idx
diff --git a/benchmarks/demo-benchmarks/bst b/benchmarks/demo-benchmarks/bst
diff --git a/benchmarks/demo-benchmarks/klee-last b/benchmarks/demo-benchmarks/klee-last
@@ -0,0 +1 @@
+klee-out-44
diff --git a/benchmarks/demo-benchmarks/test-klee-uninit.c b/benchmarks/demo-benchmarks/test-klee-uninit.c
@@ -0,0 +1,19 @@
+#include <stdio.h>
+#include <stdlib.h>
+
+int main() {
+    int* x;
+    if (x[10] == -1414812757) {
+        printf("true: %d\n", x[10]);
+    } else {
+        printf("false: %d\n", x[10]);
+    }
+
+    /* int* buf = (int*) malloc(1000); */
+    /* return buf[10]; */
+    /* if (buf[5] == 0xAB) { */
+    /*     return buf[0]; */
+    /* } else { */
+    /*     return 10; */
+    /* } */
+}
diff --git a/benchmarks/external-lib/klee-last b/benchmarks/external-lib/klee-last
@@ -0,0 +1 @@
+/home/mk/projects/GenSym/benchmarks/external-lib/klee-out-4
diff --git a/benchmarks/llvm/klee-last b/benchmarks/llvm/klee-last
@@ -0,0 +1 @@
+/home/mk/projects/GenSym/benchmarks/llvm/klee-out-1
diff --git a/benchmarks/wasm/test.c b/benchmarks/wasm/test.c
@@ -1,4 +1,6 @@
-int sym_int(char* name) { return (int) name; }
+static int cnt = 0;
+
+int sym_int(char* name) { return cnt++; }
 void assert(int expr) {}
 
 int main() {

diff --git a/benchmarks/wasm/test.wat b/benchmarks/wasm/test.wat
@@ -6,7 +6,7 @@
   (type (;4;) (func (param i32 i32) (result i32)))
   (func $__wasm_call_ctors (type 0))
   (func $sym_int (type 1) (param i32) (result i32)
-    (local i32 i32 i32 i32)
+    (local i32 i32 i32 i32 i32 i32 i32 i32)
     global.get 0
     local.set 1
     i32.const 16
@@ -18,10 +18,23 @@
     local.get 3
     local.get 0
     i32.store offset=12
-    local.get 3
-    i32.load offset=12
+    i32.const 0
     local.set 4
     local.get 4
+    i32.load offset=1028
+    local.set 5
+    i32.const 1
+    local.set 6
+    local.get 5
+    local.get 6
+    i32.add
+    local.set 7
+    i32.const 0
+    local.set 8
+    local.get 8
+    local.get 7
+    i32.store offset=1028
+    local.get 5
     return)
   (func $assert (type 2) (param i32)
     (local i32 i32 i32)
@@ -131,7 +144,7 @@
   (memory (;0;) 2)
   (global (;0;) (mut i32) (i32.const 66576))
   (global (;1;) i32 (i32.const 1024))
-  (global (;2;) i32 (i32.const 1028))
+  (global (;2;) i32 (i32.const 1032))
   (global (;3;) i32 (i32.const 1024))
   (global (;4;) i32 (i32.const 66576))
   (global (;5;) i32 (i32.const 0))

diff --git a/grammar/WatLexer.g4 b/grammar/WatLexer.g4
@@ -65,7 +65,7 @@ RETURN: 'return' ;
 IF: 'if' ;
 THEN: 'then' ;
 ELSE: 'else' ;
-SELECT: 'select' ;
+SELECT: '.select' ;
 CALL: 'call' ;
 CALL_INDIRECT: 'call_indirect' ;
 

diff --git a/grammar/WatLexer.interp b/grammar/WatLexer.interp
diff --git a/grammar/WatLexer.java b/grammar/WatLexer.java
diff --git a/grammar/WatLexer.tokens b/grammar/WatLexer.tokens
@@ -166,7 +166,7 @@ COMMENT=147
 'if'=26
 'then'=27
 'else'=28
-'select'=29
+'.select'=29
 'call'=30
 'call_indirect'=31
 'local.get'=32

diff --git a/grammar/WatParser.g4 b/grammar/WatParser.g4
@@ -127,7 +127,7 @@ plainInstr
   : UNREACHABLE
   | NOP
   | DROP
-  | SELECT
+  | selectInstr
   | BR idx
   | BR_IF idx
   | BR_TABLE idx+
@@ -170,6 +170,10 @@ store
   : numType STORE (MEM_SIZE)?
 ;
 
+selectInstr
+  : numType SELECT
+;
+
 callIndirectInstr
   /* : CALL_INDIRECT typeUse? callInstrParams */
   : CALL_INDIRECT idx? typeUse

diff --git a/grammar/WatParser.interp b/grammar/WatParser.interp
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		/home/mk/projects/GenSym/benchmarks/external-lib/klee-out-4
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		/home/mk/projects/GenSym/benchmarks/llvm/klee-out-1