Test relop simplification

formalsec · Jul 12, 2024 · 9070d32 · 9070d32
1 parent 6957035
commit 9070d32
Showing 1 changed file with 88 additions and 63 deletions.
diff --git a/test/unit/test_relop.ml b/test/unit/test_relop.ml
@@ -3,105 +3,130 @@ open Ty
 open Expr
 open Value
 
+let ( = ) = Expr.equal
+
+let true_ = value True
+
+let false_ = value False
+
 let int i = value (Int i)
 
 let real f = value (Real f)
 
 let str s = value (Str s)
 
-let i32 i = value (Num (I32 i))
+let int32 i = value (Num (I32 i))
 
-let i64 i = value (Num (I64 i))
+let int64 i = value (Num (I64 i))
 
-let f32 f = value (Num (F32 (Int32.bits_of_float f)))
+let float32 f = value (Num (F32 (Int32.bits_of_float f)))
 
-let f64 f = value (Num (F64 (Int64.bits_of_float f)))
+let float64 f = value (Num (F64 (Int64.bits_of_float f)))
 
-let app f args = value (App (f, args))
+let app f = value (App (f, []))
 
 (* bool *)
 let () =
-  assert (relop Ty_bool Eq (int 0) (int 0) = value True);
-  assert (relop Ty_bool Ne (int 0) (int 0) = value False);
-  assert (relop Ty_bool Eq (real 0.0) (real 0.0) = value True);
-  assert (relop Ty_bool Ne (real 0.0) (real 0.0) = value False);
-  assert (relop Ty_bool Eq (i32 0l) (i32 0l) = value True);
-  assert (relop Ty_bool Ne (i32 0l) (i32 0l) = value False);
-  assert (relop Ty_bool Eq (i64 0L) (i64 0L) = value True);
-  assert (relop Ty_bool Ne (i64 0L) (i64 0L) = value False);
-  assert (relop Ty_bool Eq (f32 0.0) (f32 0.0) = value True);
-  assert (relop Ty_bool Ne (f32 0.0) (f32 0.0) = value False);
-  assert (relop Ty_bool Eq (f64 0.0) (f64 0.0) = value True);
-  assert (relop Ty_bool Ne (f64 0.0) (f64 0.0) = value False)
+  assert (relop Ty_bool Eq (int 0) (int 0) = true_);
+  assert (relop Ty_bool Ne (int 0) (int 0) = false_);
+  assert (relop Ty_bool Eq (real 0.0) (real 0.0) = true_);
+  assert (relop Ty_bool Ne (real 0.0) (real 0.0) = false_);
+  assert (relop Ty_bool Eq (int32 0l) (int32 0l) = true_);
+  assert (relop Ty_bool Ne (int32 0l) (int32 0l) = false_);
+  assert (relop Ty_bool Eq (int64 0L) (int64 0L) = true_);
+  assert (relop Ty_bool Ne (int64 0L) (int64 0L) = false_);
+  assert (relop Ty_bool Eq (float32 0.0) (float32 0.0) = true_);
+  assert (relop Ty_bool Ne (float32 0.0) (float32 0.0) = false_);
+  assert (relop Ty_bool Eq (float64 0.0) (float64 0.0) = true_);
+  assert (relop Ty_bool Ne (float64 0.0) (float64 0.0) = false_)
 
 (* int *)
 let () =
-  assert (relop Ty_int Lt (int 0) (int 1) = value True);
-  assert (relop Ty_int Le (int 0) (int 1) = value True);
-  assert (relop Ty_int Gt (int 0) (int 1) = value False);
-  assert (relop Ty_int Ge (int 0) (int 1) = value False)
+  assert (relop Ty_int Lt (int 0) (int 1) = true_);
+  assert (relop Ty_int Le (int 0) (int 1) = true_);
+  assert (relop Ty_int Gt (int 0) (int 1) = false_);
+  assert (relop Ty_int Ge (int 0) (int 1) = false_)
 
 (* real *)
 let () =
-  assert (relop Ty_real Lt (real 0.0) (real 1.0) = value True);
-  assert (relop Ty_real Le (real 0.0) (real 1.0) = value True);
-  assert (relop Ty_real Gt (real 0.0) (real 1.0) = value False);
-  assert (relop Ty_real Ge (real 0.0) (real 1.0) = value False)
+  let x = symbol @@ Symbol.make Ty_real "x" in
+  assert (relop Ty_bool Ne (real Float.nan) x = true_);
+  assert (relop Ty_bool Eq x (real Float.nan) = false_);
+  assert (relop Ty_real Lt (real 0.0) (real 1.0) = true_);
+  assert (relop Ty_real Le (real 0.0) (real 1.0) = true_);
+  assert (relop Ty_real Gt (real 0.0) (real 1.0) = false_);
+  assert (relop Ty_real Ge (real 0.0) (real 1.0) = false_)
 
 (* str *)
 let () =
-  assert (relop Ty_str Lt (str "a") (str "b") = value True);
-  assert (relop Ty_str Le (str "a") (str "b") = value True);
-  assert (relop Ty_str Gt (str "a") (str "b") = value False);
-  assert (relop Ty_str Ge (str "a") (str "b") = value False);
-  assert (relop Ty_str Eq (str "a") (str "a") = value True);
-  assert (relop Ty_str Ne (str "a") (str "a") = value False);
-  assert (relop Ty_str Eq (str "a") (str "b") = value False);
-  assert (relop Ty_str Ne (str "a") (str "b") = value True)
+  assert (relop Ty_str Lt (str "a") (str "b") = true_);
+  assert (relop Ty_str Le (str "a") (str "b") = true_);
+  assert (relop Ty_str Gt (str "a") (str "b") = false_);
+  assert (relop Ty_str Ge (str "a") (str "b") = false_);
+  assert (relop Ty_str Eq (str "a") (str "a") = true_);
+  assert (relop Ty_str Ne (str "a") (str "a") = false_);
+  assert (relop Ty_str Eq (str "a") (str "b") = false_);
+  assert (relop Ty_str Ne (str "a") (str "b") = true_)
 
 (* i32 *)
 let () =
-  assert (relop (Ty_bitv 32) Lt (i32 0l) (i32 1l) = value True);
-  assert (relop (Ty_bitv 32) LtU (i32 (-1l)) (i32 0l) = value False);
-  assert (relop (Ty_bitv 32) Le (i32 0l) (i32 1l) = value True);
-  assert (relop (Ty_bitv 32) LeU (i32 (-1l)) (i32 0l) = value False);
-  assert (relop (Ty_bitv 32) Gt (i32 1l) (i32 0l) = value True);
-  assert (relop (Ty_bitv 32) GtU (i32 0l) (i32 (-1l)) = value False);
-  assert (relop (Ty_bitv 32) Ge (i32 1l) (i32 0l) = value True);
-  assert (relop (Ty_bitv 32) GeU (i32 0l) (i32 (-1l)) = value False)
+  assert (relop (Ty_bitv 32) Lt (int32 0l) (int32 1l) = true_);
+  assert (relop (Ty_bitv 32) LtU (int32 (-1l)) (int32 0l) = false_);
+  assert (relop (Ty_bitv 32) Le (int32 0l) (int32 1l) = true_);
+  assert (relop (Ty_bitv 32) LeU (int32 (-1l)) (int32 0l) = false_);
+  assert (relop (Ty_bitv 32) Gt (int32 1l) (int32 0l) = true_);
+  assert (relop (Ty_bitv 32) GtU (int32 0l) (int32 (-1l)) = false_);
+  assert (relop (Ty_bitv 32) Ge (int32 1l) (int32 0l) = true_);
+  assert (relop (Ty_bitv 32) GeU (int32 0l) (int32 (-1l)) = false_)
 
 (* i64 *)
 let () =
-  assert (relop (Ty_bitv 64) Lt (i64 0L) (i64 1L) = value True);
-  assert (relop (Ty_bitv 64) LtU (i64 (-1L)) (i64 0L) = value False);
-  assert (relop (Ty_bitv 64) Le (i64 0L) (i64 1L) = value True);
-  assert (relop (Ty_bitv 64) LeU (i64 (-1L)) (i64 0L) = value False);
-  assert (relop (Ty_bitv 64) Gt (i64 1L) (i64 0L) = value True);
-  assert (relop (Ty_bitv 64) GtU (i64 0L) (i64 (-1L)) = value False);
-  assert (relop (Ty_bitv 64) Ge (i64 1L) (i64 0L) = value True);
-  assert (relop (Ty_bitv 64) GeU (i64 0L) (i64 (-1L)) = value False)
+  assert (relop (Ty_bitv 64) Lt (int64 0L) (int64 1L) = true_);
+  assert (relop (Ty_bitv 64) LtU (int64 (-1L)) (int64 0L) = false_);
+  assert (relop (Ty_bitv 64) Le (int64 0L) (int64 1L) = true_);
+  assert (relop (Ty_bitv 64) LeU (int64 (-1L)) (int64 0L) = false_);
+  assert (relop (Ty_bitv 64) Gt (int64 1L) (int64 0L) = true_);
+  assert (relop (Ty_bitv 64) GtU (int64 0L) (int64 (-1L)) = false_);
+  assert (relop (Ty_bitv 64) Ge (int64 1L) (int64 0L) = true_);
+  assert (relop (Ty_bitv 64) GeU (int64 0L) (int64 (-1L)) = false_)
 
 (* f32 *)
 let () =
-  assert (relop (Ty_fp 32) Lt (f32 0.0) (f32 1.0) = value True);
-  assert (relop (Ty_fp 32) Le (f32 0.0) (f32 1.0) = value True);
-  assert (relop (Ty_fp 32) Gt (f32 0.0) (f32 1.0) = value False);
-  assert (relop (Ty_fp 32) Ge (f32 0.0) (f32 1.0) = value False)
+  assert (relop (Ty_fp 32) Lt (float32 0.0) (float32 1.0) = true_);
+  assert (relop (Ty_fp 32) Le (float32 0.0) (float32 1.0) = true_);
+  assert (relop (Ty_fp 32) Gt (float32 0.0) (float32 1.0) = false_);
+  assert (relop (Ty_fp 32) Ge (float32 0.0) (float32 1.0) = false_)
 
 (* f64 *)
 let () =
-  assert (relop (Ty_fp 64) Lt (f64 0.0) (f64 1.0) = value True);
-  assert (relop (Ty_fp 64) Le (f64 0.0) (f64 1.0) = value True);
-  assert (relop (Ty_fp 64) Gt (f64 0.0) (f64 1.0) = value False);
-  assert (relop (Ty_fp 64) Ge (f64 0.0) (f64 1.0) = value False)
+  assert (relop (Ty_fp 64) Lt (float64 0.0) (float64 1.0) = true_);
+  assert (relop (Ty_fp 64) Le (float64 0.0) (float64 1.0) = true_);
+  assert (relop (Ty_fp 64) Gt (float64 0.0) (float64 1.0) = false_);
+  assert (relop (Ty_fp 64) Ge (float64 0.0) (float64 1.0) = false_)
 
 (* app *)
 let () =
   assert (
-    relop Ty_app Eq (app (`Op "undefined") []) (app (`Op "undefined") [])
-    = value True );
+    relop Ty_app Eq (app (`Op "undefined")) (app (`Op "undefined")) = true_ );
   assert (
-    relop Ty_app Ne (app (`Op "undefined") []) (app (`Op "undefined") [])
-    = value False );
-  assert (relop Ty_app Eq (app (`Op "undefined") []) (int 1) = value False);
-  assert (relop Ty_app Eq (int 1) (app (`Op "undefined") []) = value False)
+    relop Ty_app Ne (app (`Op "undefined")) (app (`Op "undefined")) = false_ );
+  assert (relop Ty_app Eq (app (`Op "undefined")) (int 1) = false_);
+  assert (relop Ty_app Ne (int 1) (app (`Op "undefined")) = true_)
+
+(* ptr *)
+let () =
+  let ty = Ty_bitv 32 in
+  let p0 = ptr 0l (int32 0l) in
+  let p1 = ptr 4l (int32 0l) in
+  assert (relop Ty_bool Eq p0 p0 = true_);
+  assert (relop Ty_bool Eq p0 p1 = false_);
+  assert (relop Ty_bool Ne p0 p0 = false_);
+  assert (relop Ty_bool Ne p0 p1 = true_);
+  assert (relop ty LtU p0 p0 = false_);
+  assert (relop ty LeU p0 p1 = true_);
+  assert (relop ty GeU p0 p0 = true_);
+  assert (relop ty GtU p0 p1 = false_);
+  assert (relop ty Le p0 (int32 4l) = true_);
+  assert (relop ty Lt (int32 4l) p0 = false_);
+  assert (relop ty Gt p1 (int32 4l) = false_);
+  assert (relop ty Ge (int32 4l) p1 = true_)