Canonize relops in parser

formalsec · Feb 19, 2024 · 69f84aa · 69f84aa
1 parent 990e03b
commit 69f84aa
Showing 1 changed file with 23 additions and 4 deletions.
diff --git a/lib/parser.mly b/lib/parser.mly
@@ -3,6 +3,8 @@ open Value
 open Ty
 open Expr
 
+let canonize = false
+
 let varmap = Hashtbl.create 512
 
 let add_bind x t = Hashtbl.replace varmap x t
@@ -25,13 +27,13 @@ let get_bind x = Hashtbl.find varmap x
 %token <bool> BOOL
 %token <string> STR
 %token <string> SYMBOL
+%token <Ty.t> TYPE
+%token <Ty.logic> LOGIC
 %token <Ty.t * Ty.unop> UNARY
 %token <Ty.t * Ty.binop> BINARY
 %token <Ty.t * Ty.triop> TERNARY
 %token <Ty.t * Ty.relop> RELOP
 %token <Ty.t * Ty.cvtop> CVTOP
-%token <Ty.t> TYPE
-%token <Ty.logic> LOGIC
 
 %start <Ast.t list> script
 %%
@@ -54,7 +56,7 @@ let stmt :=
 let s_expr :=
   | x = SYMBOL; { mk_symbol @@ Symbol.mk_symbol (get_bind x) x }
   | c = spec_constant; { Val c @: Value.type_of c }
-  | LPAREN; op = paren_op; RPAREN; { op }
+  | LPAREN; op = paren_op; RPAREN; <>
 
 let paren_op :=
   | PTR; LPAREN; ty = TYPE; x = NUM; RPAREN; e = s_expr;
@@ -68,7 +70,24 @@ let paren_op :=
   | (ty, op) = CVTOP; e = s_expr;
     { Cvtop (op, e) @: ty }
   | (ty, op) = RELOP; e1 = s_expr; e2 = s_expr;
-    { Relop (op, e1, e2) @: ty }
+    {
+      let open Bitv in
+      if not canonize then Relop (op, e1, e2) @: ty
+      else match (ty, op) with
+      | Ty_bitv S32, Eq -> I32.(e1 = e2)
+      | Ty_bitv S32, Ne -> I32.(e1 != e2)
+      | Ty_bitv S32, Gt -> I32.(e1 > e2)
+      | Ty_bitv S32, Ge -> I32.(e1 >= e2)
+      | Ty_bitv S32, Lt -> I32.(e1 < e2)
+      | Ty_bitv S32, Le -> I32.(e1 < e2)
+      | Ty_bitv S64, Eq -> I64.(e1 = e2)
+      | Ty_bitv S64, Ne -> I64.(e1 != e2)
+      | Ty_bitv S64, Gt -> I64.(e1 > e2)
+      | Ty_bitv S64, Ge -> I64.(e1 >= e2)
+      | Ty_bitv S64, Lt -> I64.(e1 < e2)
+      | Ty_bitv S64, Le -> I64.(e1 < e2)
+      | _ -> Relop (op, e1, e2) @: ty
+    }
   | EXTRACT; ~ = s_expr; l = NUM; h = NUM;
     { Extract (s_expr, h, l) @: Ty_bitv S32 }
   | CONCAT; e1 = s_expr; e2 = s_expr;