[asl] Use qcheck to check constraint_binops

asllib/StaticOperations.ml

@@ -112,15 +112,15 @@ let constraint_pow c1 c2 =
       (* {a..b} POW c is {0.. (b POW c), (- ((-a) POW c)) ..
          ((-a) POW c)} *)
       let mac = pow (neg a) c in
-      [ range zero_expr (pow b c); range (neg mac) mac ]
+      [ range zero_expr (pow b c); range (neg mac) mac; exact one_expr ]
   | Constraint_Exact a, Constraint_Range (c, d) ->
       (* a POW {c..d} is {(a POW c) .. (a POW d), (-((-a) POW d)) .. ((-a) POW d)} *)
       let mad = pow (neg a) d in
-      [ range (pow a c) (pow a d); range (neg mad) mad ]
+      [ range (pow a c) (pow a d); range (neg mad) mad; exact one_expr ]
   | Constraint_Range (a, b), Constraint_Range (_c, d) ->
       (* {a..b} POW {c..d} is {0.. (b POW d), (- ((-a) POW d)) .. ((-a) POW d)} *)
       let mad = pow (neg a) d in
-      [ range zero_expr (pow b d); range (neg mad) mad ]
+      [ range zero_expr (pow b d); range (neg mad) mad; exact one_expr ]
 
 (* Begin ConstraintBinop *)
 let constraint_binop op cs1 cs2 =
@@ -138,6 +138,50 @@ let constraint_binop op cs1 cs2 =
       assert false
 (* End *)
 
+(* Begin FilterReduceConstraintDiv *)
+let filter_reduce_constraint_div =
+  let get_literal_div_opt e =
+    match e.desc with
+    | E_Binop (DIV, a, b) -> (
+        match (a.desc, b.desc) with
+        | E_Literal (L_Int z1), E_Literal (L_Int z2) -> Some (z1, z2)
+        | _ -> None)
+    | _ -> None
+  in
+  function
+  | Constraint_Exact e as c -> (
+      match get_literal_div_opt e with
+      | Some (z1, z2) when Z.sign z2 != 0 ->
+          if Z.divisible z1 z2 then Some c else None
+      | _ -> Some c)
+  | Constraint_Range (e1, e2) as c -> (
+      let z1_opt =
+        match get_literal_div_opt e1 with
+        | Some (z1, z2) when Z.sign z2 != 0 ->
+            let zdiv, zmod = Z.ediv_rem z1 z2 in
+            let zres = if Z.sign zmod = 0 then zdiv else Z.succ zdiv in
+            Some zres
+        | _ -> None
+      and z2_opt =
+        match get_literal_div_opt e2 with
+        | Some (z1, z2) when Z.sign z2 != 0 -> Some (Z.ediv z1 z2)
+        | _ -> None
+      in
+      match (z1_opt, z2_opt) with
+      | Some z1, Some z2 ->
+          let () =
+            if false then
+              Format.eprintf "Reducing %a DIV %a@ got z1=%a and z2=%a@."
+                PP.pp_expr e1 PP.pp_expr e2 Z.pp_print z1 Z.pp_print z2
+          in
+          if Z.equal z1 z2 then Some (exact (expr_of_z z1))
+          else if Z.leq z1 z2 then Some (range (expr_of_z z1) (expr_of_z z2))
+          else None
+      | Some z1, None -> Some (range (expr_of_z z1) e2)
+      | None, Some z2 -> Some (range e1 (expr_of_z z2))
+      | None, None -> Some c)
+(* End *)
+
 type strictness = [ `Silence | `Warn | `TypeCheck ]
 
 module type CONFIG = sig
@@ -245,51 +289,6 @@ module Make (C : CONFIG) = struct
         assert false
   (* End *)
 
-  (* Begin FilterReduceConstraintDiv *)
-  let filter_reduce_constraint_div =
-    let get_literal_div_opt e =
-      match e.desc with
-      | E_Binop (DIV, a, b) -> (
-          match (a.desc, b.desc) with
-          | E_Literal (L_Int z1), E_Literal (L_Int z2) -> Some (z1, z2)
-          | _ -> None)
-      | _ -> None
-    in
-    function
-    | Constraint_Exact e as c -> (
-        match get_literal_div_opt e with
-        | Some (z1, z2) when Z.sign z2 != 0 ->
-            if Z.divisible z1 z2 then Some c else None
-        | _ -> Some c)
-    | Constraint_Range (e1, e2) as c -> (
-        let z1_opt =
-          match get_literal_div_opt e1 with
-          | Some (z1, z2) when Z.sign z2 != 0 ->
-              let zdiv, zmod = Z.ediv_rem z1 z2 in
-              let zres = if Z.sign zmod = 0 then zdiv else Z.succ zdiv in
-              Some zres
-          | _ -> None
-        and z2_opt =
-          match get_literal_div_opt e2 with
-          | Some (z1, z2) when Z.sign z2 != 0 -> Some (Z.ediv z1 z2)
-          | _ -> None
-        in
-        match (z1_opt, z2_opt) with
-        | Some z1, Some z2 ->
-            let () =
-              if false then
-                Format.eprintf "Reducing %a DIV %a@ got z1=%a and z2=%a@."
-                  PP.pp_expr e1 PP.pp_expr e2 Z.pp_print z1 Z.pp_print z2
-            in
-            if Z.equal z1 z2 then Some (exact (expr_of_z z1))
-            else if Z.leq z1 z2 then Some (range (expr_of_z z1) (expr_of_z z2))
-            else None
-        | Some z1, None -> Some (range (expr_of_z z1) e2)
-        | None, Some z2 -> Some (range e1 (expr_of_z z2))
-        | None, None -> Some c)
-
-  (* End *)
-
   let refine_constraint_for_div ~loc op cs =
     match op with
     | DIV -> (

asllib/StaticOperations.mli

@@ -22,3 +22,7 @@ module Make : functor (C : CONFIG) -> sig
     int_constraint list ->
     int_constraint list
 end
+
+(* Used by asllib/tests/ConstraintBinops.ml *)
+
+val filter_reduce_constraint_div : int_constraint -> int_constraint option

asllib/tests/ConstraintBinops.ml

@@ -0,0 +1,161 @@
+open Asllib
+open AST
+
+let eval_binop x op y =
+  let pos = ASTUtils.dummy_annotated and t = Error.Static in
+  match Operations.binop_values pos t op (L_Int x) (L_Int y) with
+  | L_Int z -> z
+  | _ -> assert false
+
+let eval_expr e =
+  match StaticInterpreter.static_eval StaticEnv.empty e with
+  | L_Int z -> z
+  | _ -> assert false
+
+let z_in_constraint z c =
+  match StaticOperations.filter_reduce_constraint_div c with
+  | None -> false
+  | Some (Constraint_Exact e) -> (
+      try Z.equal z (eval_expr e) with _ -> false)
+  | Some (Constraint_Range (e1, e2)) -> (
+      try
+        let z1 = eval_expr e1 and z2 = eval_expr e2 in
+        Z.leq z1 z && Z.leq z z2
+      with _ -> false)
+
+let z_in_constraints z cs = List.exists (z_in_constraint z) cs
+
+let property op (x, y, cs1, cs2) =
+  QCheck.assume (z_in_constraints x cs1);
+  QCheck.assume (z_in_constraints y cs2);
+  (match op with
+  | SHR | SHL | POW -> QCheck.assume (Z.sign y >= 0)
+  | DIV | DIVRM | MOD -> QCheck.assume (Z.sign y > 0)
+  | _ -> ());
+  z_in_constraints (eval_binop x op y)
+    (StaticOperations.constraint_binop op cs1 cs2)
+
+let gen_xy _strict op =
+  let open QCheck2.Gen in
+  let base_nat = small_nat in
+  let non_null_nat =
+    oneof [ base_nat >|= ( + ) 1; (base_nat >|= fun n -> -(n + 1)) ]
+  in
+  let signed_nat = oneof [ base_nat; base_nat >|= ( ~- ) ] in
+  match op with
+  | SHR | SHL | POW -> pair signed_nat base_nat
+  | DIV ->
+      let* y = base_nat in
+      let+ x = signed_nat >|= ( * ) y in
+      (x, y)
+  | DIVRM | MOD -> pair signed_nat non_null_nat
+  | _ -> pair signed_nat signed_nat
+
+let gen_ab _strict _op x _y =
+  let open QCheck2.Gen in
+  let+ a = nat >|= ( - ) x >|= ASTUtils.expr_of_int
+  and+ b = nat >|= ( + ) x >|= ASTUtils.expr_of_int in
+  (a, b)
+
+let gen_cd strict op _x y =
+  let open QCheck2.Gen in
+  let+ c =
+    (if strict then
+       match op with
+       | SHR | SHL | POW -> 0 -- (y + 1)
+       | DIV | DIVRM | MOD ->
+           if y > 0 then oneof [ 1 -- (y + 1); nat >|= ( - ) ~-1 ]
+           else nat >|= ( - ) y
+       | _ -> nat >|= ( - ) y
+     else nat >|= ( - ) y)
+    >|= ASTUtils.expr_of_int
+  and+ d = nat >|= ( + ) y >|= ASTUtils.expr_of_int in
+  (c, d)
+
+let gen_test_abcd strict op =
+  let open QCheck2.Gen in
+  let* x, y = gen_xy strict op in
+  let+ a, b = gen_ab strict op x y and+ c, d = gen_cd strict op x y in
+  ( Z.of_int x,
+    Z.of_int y,
+    [ Constraint_Range (a, b) ],
+    [ Constraint_Range (c, d) ] )
+
+let gen_test_abc strict op =
+  let open QCheck2.Gen in
+  let* x, y = gen_xy strict op in
+  let+ a, b = gen_ab strict op x y in
+  let c = ASTUtils.expr_of_int y in
+  (Z.of_int x, Z.of_int y, [ Constraint_Range (a, b) ], [ Constraint_Exact c ])
+
+let gen_test_acd strict op =
+  let open QCheck2.Gen in
+  let* x, y = gen_xy strict op in
+  let+ c, d = gen_cd strict op x y in
+  let a = ASTUtils.expr_of_int x in
+  (Z.of_int x, Z.of_int y, [ Constraint_Exact a ], [ Constraint_Range (c, d) ])
+
+let print_test op (x, y, cs1, cs2) =
+  try
+    let res = eval_binop x op y in
+    let cs = StaticOperations.constraint_binop op cs1 cs2 in
+    Format.asprintf "@[@[%a %s %a = %a@]@ is@ not@ in@ @[[%a] %s [%a] = [%a]@]"
+      Z.pp_print x (PP.binop_to_string op) Z.pp_print y Z.pp_print res
+      PP.pp_int_constraints cs1 (PP.binop_to_string op) PP.pp_int_constraints
+      cs2 PP.pp_int_constraints cs
+  with _ ->
+    Format.asprintf
+      "(x=%a, y=%a, cs1=%a, cs2=%a) with op %s resulted in an error" Z.pp_print
+      x Z.pp_print y PP.pp_int_constraints cs1 PP.pp_int_constraints cs2
+      (PP.binop_to_string op)
+
+let long_factor = 1000
+let strict = true
+let base_count = 10000
+
+let test_abcd op =
+  let count = base_count * 10 in
+  QCheck2.Test.make ~count ~long_factor ~print:(print_test op)
+    ~name:"constraint_binop is sound" (gen_test_abcd strict op) (property op)
+
+let test_abc op =
+  let count = base_count in
+  QCheck2.Test.make ~count ~long_factor ~print:(print_test op)
+    ~name:"constraint_binop is sound" (gen_test_abc strict op) (property op)
+
+let test_acd op =
+  let count = base_count in
+  QCheck2.Test.make ~count ~long_factor ~print:(print_test op)
+    ~name:"constraint_binop is sound" (gen_test_acd strict op) (property op)
+
+let () =
+  QCheck_runner.run_tests_main
+    [
+      test_abcd PLUS;
+      test_acd PLUS;
+      test_abc PLUS;
+      test_abcd MINUS;
+      test_acd MINUS;
+      test_abc MINUS;
+      test_abcd MUL;
+      test_acd MUL;
+      test_abc MUL;
+      test_abcd DIV;
+      test_acd DIV;
+      test_abc DIV;
+      test_abcd DIVRM;
+      test_acd DIVRM;
+      test_abc DIVRM;
+      test_abcd MOD;
+      test_acd MOD;
+      test_abc MOD;
+      test_abcd SHR;
+      test_acd SHR;
+      test_abc SHR;
+      test_abcd SHL;
+      test_acd SHL;
+      test_abc SHL;
+      test_abcd POW;
+      test_acd POW;
+      test_abc POW;
+    ]

asllib/tests/dune

@@ -1,9 +1,9 @@
-(test
- (name toposort)
+(tests
+ (names toposort ConstraintBinops)
  (modes native)
  (enabled_if %{lib-available:qcheck})
  (libraries asllib qcheck)
- (modules toposort))
+ (modules toposort ConstraintBinops))
 
 (tests
  (names static bitvector types)

asllib/tests/toposort.ml

@@ -98,7 +98,4 @@ let testsuite =
   ]
 
 let () =
-  let errcode =
-    QCheck_base_runner.run_tests (* ~long:true ~verbose:true *) testsuite
-  in
-  exit errcode
+  QCheck_runner.run_tests_main (* ~long:true ~verbose:true *) testsuite