[asl] limit constraint size after explosion

asllib/StaticOperations.ml

@@ -310,32 +310,45 @@ module Make (C : CONFIG) = struct
     in
     function [] -> [] | x :: li -> aux x [ x ] li
 
+  let dz_unions =
+    let module DZ = Diet.Z in
+    let rec main = function
+      | [] -> DZ.empty
+      | [ x ] -> x
+      | li -> aux [] li |> main
+    and aux acc = function
+      | [] -> acc
+      | [ x ] -> x :: acc
+      | x :: y :: li -> aux (DZ.union x y :: acc) li
+    in
+    main
+
   let simplify_static_constraints =
     let module DZ = Diet.Z in
-    let acc_diet (diet, non_static) = function
+    let to_diets (diets, non_static) = function
       | Constraint_Exact e as c -> (
           match e.desc with
-          | E_Literal (L_Int z) ->
-              (DZ.(add Interval.(make z z) diet), non_static)
-          | _ -> (diet, c :: non_static))
+          | E_Literal (L_Int z) -> (DZ.singleton z :: diets, non_static)
+          | _ -> (diets, c :: non_static))
       | Constraint_Range (e1, e2) as c -> (
           match (e1.desc, e2.desc) with
           | E_Literal (L_Int z1), E_Literal (L_Int z2) when Z.leq z1 z2 ->
-              DZ.(add Interval.(make z1 z2) diet, non_static)
-          | _ -> (diet, c :: non_static))
+              DZ.(add Interval.(make z1 z2) empty :: diets, non_static)
+          | _ -> (diets, c :: non_static))
     in
     let constraint_of_interval interval =
       let x = DZ.Interval.x interval and y = DZ.Interval.y interval in
       if Z.equal x y then Constraint_Exact (expr_of_z x)
       else Constraint_Range (expr_of_z x, expr_of_z y)
     in
     fun constraints ->
-      let diet, non_static =
-        List.fold_left acc_diet (DZ.empty, []) constraints
-      in
-      DZ.fold
-        (fun interval acc -> constraint_of_interval interval :: acc)
-        diet non_static
+      if List.length constraints > 1000 then constraints
+      else
+        let diets, non_static = List.fold_left to_diets ([], []) constraints in
+        let diet = dz_unions diets in
+        DZ.fold
+          (fun interval acc -> constraint_of_interval interval :: acc)
+          diet non_static
 
   (* Begin ReduceConstraints *)
   let reduce_constraints env constraints =
@@ -353,6 +366,9 @@ module Make (C : CONFIG) = struct
     | OR | RDIV | BV_CONCAT ->
         assert false
 
+  let max_constraint_size = Z.shift_left Z.one 14
+  let max_exploded_interval_size = max_constraint_size
+
   (* Begin ExplodeIntervals *)
   let explode_intervals =
     let rec make_interval ~loc acc a b =
@@ -362,10 +378,9 @@ module Make (C : CONFIG) = struct
         make_interval ~loc acc' a (Z.pred b)
       else acc
     in
-    let[@warning "-44"] interval_too_large z1 z2 =
-      let open Z in
-      let max_interval_size = ~$1 lsl 14 in
-      Compare.(abs (z1 - z2) > max_interval_size)
+    let interval_too_large z1 z2 =
+      let expected_size = Z.sub z2 z1 in
+      Z.lt max_exploded_interval_size expected_size
     in
     let explode_constraint ~loc env = function
       | Constraint_Exact _ as c -> [ c ]
@@ -400,7 +415,22 @@ module Make (C : CONFIG) = struct
         in
         let cs1_arg, cs2_arg =
           if binop_is_exploding op then
-            (explode_intervals ~loc env cs1, explode_intervals ~loc env cs2_f)
+            let ex_cs1 = explode_intervals ~loc env cs1
+            and ex_cs2 = explode_intervals ~loc env cs2_f in
+            let l1 = List.length ex_cs1 and l2 = List.length ex_cs2 in
+            let expected_constraint_length =
+              Z.(if op = MOD then ~$l2 else mul ~$l1 ~$l2)
+            in
+            if Z.leq expected_constraint_length max_constraint_size then
+              (ex_cs1, ex_cs2)
+            else
+              let () =
+                C.warn_from ~loc
+                  Error.(
+                    ConstraintSetPairToBigToBeExploded
+                      { op; left = cs1; right = cs2_f })
+              in
+              (cs1, cs2_f)
           else (cs1, cs2_f)
         in
         let annotated_cs =

asllib/error.ml

@@ -120,6 +120,11 @@ type warning_desc =
   | NoRecursionLimit of identifier list
   | NoLoopLimit
   | IntervalTooBigToBeExploded of Z.t * Z.t
+  | ConstraintSetPairToBigToBeExploded of {
+      op : binop;
+      left : int_constraint list;
+      right : int_constraint list;
+    }
   | RemovingValuesFromConstraints of {
       op : binop;
       prev : int_constraint list;
@@ -196,6 +201,7 @@ let error_label = function
 let warning_label = function
   | NoLoopLimit -> "NoLoopLimit"
   | IntervalTooBigToBeExploded _ -> "IntervalTooBigToBeExploded"
+  | ConstraintSetPairToBigToBeExploded _ -> "ConstraintSetPairToBigToBeExploded"
   | RemovingValuesFromConstraints _ -> "RemovingValuesFromConstraints"
   | NoRecursionLimit _ -> "NoRecursionLimit"
   | PragmaUse _ -> "PragmaUse"
@@ -486,6 +492,13 @@ module PPrint = struct
     | NoLoopLimit ->
         fprintf f "@[%a@]" pp_print_text
           "ASL Warning: Loop does not have a limit."
+    | ConstraintSetPairToBigToBeExploded { op; left; right } ->
+        fprintf f
+          "@[Exploding@ sets@ in@ for@ the@ binary@ operation %s@ would@ \
+           result@ in@ too@ big@ a@ constraint@ set@ with@ constraints@ %a@ \
+           and@ %a. Continuing with those.@]"
+          (binop_to_string op) PP.pp_int_constraints left PP.pp_int_constraints
+          right
     | IntervalTooBigToBeExploded (za, zb) ->
         fprintf f
           "@[Interval too large: @[<h>[ %a .. %a ]@].@ Keeping it as an \

asllib/tests/ASLDefinition.t/run.t

@@ -2,6 +2,9 @@ Examples used in ASL High-level Definition:
   $ aslref --no-exec spec1.asl
   $ aslref --no-exec spec2.asl
   $ aslref spec3.asl
+  File spec3.asl, line 5, characters 16 to 45:
+  Exploding sets in for the binary operation * would result in too big a
+  constraint set with constraints 0..255 and 0..255. Continuing with those.
 
   $ aslref --no-exec Bitfields.asl
   $ aslref Bitfields_nested.asl

asllib/tests/performance.t/constraint-mul-00.asl

@@ -0,0 +1,20 @@
+constant A = 1 << 2;
+constant B = 1 << 2;
+
+func myfunction(a : integer{0..A}, b : integer{0..B})
+begin
+    let n = a DIVRM b;     // 10 DIVRM 3 == 3
+    var b1 = n * b;
+    b1 = 4;
+    b1 = A * B;
+end;
+
+func main() => integer
+begin
+    myfunction(0, 1);
+    myfunction(A, 1);
+    myfunction(A DIVRM 2, B DIVRM 4);
+    return 0;
+end;
+
+

asllib/tests/performance.t/constraint-mul-01.asl

@@ -0,0 +1,20 @@
+constant A = 1 << 4;
+constant B = 1 << 4;
+
+func myfunction(a : integer{0..A}, b : integer{0..B})
+begin
+    let n = a DIVRM b;     // 10 DIVRM 3 == 3
+    var b1 = n * b;
+    b1 = 4;
+    b1 = A * B;
+end;
+
+func main() => integer
+begin
+    myfunction(0, 1);
+    myfunction(A, 1);
+    myfunction(A DIVRM 2, B DIVRM 4);
+    return 0;
+end;
+
+

asllib/tests/performance.t/constraint-mul-02.asl

@@ -0,0 +1,20 @@
+constant A = 1 << 5;
+constant B = 1 << 5;
+
+func myfunction(a : integer{0..A}, b : integer{0..B})
+begin
+    let n = a DIVRM b;     // 10 DIVRM 3 == 3
+    var b1 = n * b;
+    b1 = 4;
+    b1 = A * B;
+end;
+
+func main() => integer
+begin
+    myfunction(0, 1);
+    myfunction(A, 1);
+    myfunction(A DIVRM 2, B DIVRM 4);
+    return 0;
+end;
+
+

asllib/tests/performance.t/constraint-mul-03.asl

@@ -0,0 +1,20 @@
+constant A = 1 << 6;
+constant B = 1 << 6;
+
+func myfunction(a : integer{0..A}, b : integer{0..B})
+begin
+    let n = a DIVRM b;     // 10 DIVRM 3 == 3
+    var b1 = n * b;
+    b1 = 4;
+    b1 = A * B;
+end;
+
+func main() => integer
+begin
+    myfunction(0, 1);
+    myfunction(A, 1);
+    myfunction(A DIVRM 2, B DIVRM 4);
+    return 0;
+end;
+
+

asllib/tests/performance.t/constraint-mul-04.asl

@@ -0,0 +1,20 @@
+constant A = 1 << 7;
+constant B = 1 << 7;
+
+func myfunction(a : integer{0..A}, b : integer{0..B})
+begin
+    let n = a DIVRM b;     // 10 DIVRM 3 == 3
+    var b1 = n * b;
+    b1 = 4;
+    b1 = A * B;
+end;
+
+func main() => integer
+begin
+    myfunction(0, 1);
+    myfunction(A, 1);
+    myfunction(A DIVRM 2, B DIVRM 4);
+    return 0;
+end;
+
+

asllib/tests/performance.t/constraint-mul-05.asl

@@ -0,0 +1,20 @@
+constant A = 1 << 8;
+constant B = 1 << 8;
+
+func myfunction(a : integer{0..A}, b : integer{0..B})
+begin
+    let n = a DIVRM b;     // 10 DIVRM 3 == 3
+    var b1 = n * b;
+    b1 = 4;
+    b1 = A * B;
+end;
+
+func main() => integer
+begin
+    myfunction(0, 1);
+    myfunction(A, 1);
+    myfunction(A DIVRM 2, B DIVRM 4);
+    return 0;
+end;
+
+

asllib/tests/performance.t/constraint-mul-06.asl

@@ -0,0 +1,20 @@
+constant A = 1 << 9;
+constant B = 1 << 9;
+
+func myfunction(a : integer{0..A}, b : integer{0..B})
+begin
+    let n = a DIVRM b;     // 10 DIVRM 3 == 3
+    var b1 = n * b;
+    b1 = 4;
+    b1 = A * B;
+end;
+
+func main() => integer
+begin
+    myfunction(0, 1);
+    myfunction(A, 1);
+    myfunction(A DIVRM 2, B DIVRM 4);
+    return 0;
+end;
+
+

asllib/tests/performance.t/constraint-mul-07.asl

@@ -0,0 +1,20 @@
+constant A = 1 << 10;
+constant B = 1 << 10;
+
+func myfunction(a : integer{0..A}, b : integer{0..B})
+begin
+    let n = a DIVRM b;     // 10 DIVRM 3 == 3
+    var b1 = n * b;
+    b1 = 4;
+    b1 = A * B;
+end;
+
+func main() => integer
+begin
+    myfunction(0, 1);
+    myfunction(A, 1);
+    myfunction(A DIVRM 2, B DIVRM 4);
+    return 0;
+end;
+
+

asllib/tests/performance.t/constraint-mul-08.asl

@@ -0,0 +1,20 @@
+constant A = 1 << 11;
+constant B = 1 << 11;
+
+func myfunction(a : integer{0..A}, b : integer{0..B})
+begin
+    let n = a DIVRM b;     // 10 DIVRM 3 == 3
+    var b1 = n * b;
+    b1 = 4;
+    b1 = A * B;
+end;
+
+func main() => integer
+begin
+    myfunction(0, 1);
+    myfunction(A, 1);
+    myfunction(A DIVRM 2, B DIVRM 4);
+    return 0;
+end;
+
+

asllib/tests/performance.t/constraint-mul-09.asl

@@ -0,0 +1,20 @@
+constant A = 1 << 12;
+constant B = 1 << 12;
+
+func myfunction(a : integer{0..A}, b : integer{0..B})
+begin
+    let n = a DIVRM b;     // 10 DIVRM 3 == 3
+    var b1 = n * b;
+    b1 = 4;
+    b1 = A * B;
+end;
+
+func main() => integer
+begin
+    myfunction(0, 1);
+    myfunction(A, 1);
+    myfunction(A DIVRM 2, B DIVRM 4);
+    return 0;
+end;
+
+

asllib/tests/performance.t/constraint-mul-10.asl

@@ -0,0 +1,20 @@
+constant A = 1 << 13;
+constant B = 1 << 13;
+
+func myfunction(a : integer{0..A}, b : integer{0..B})
+begin
+    let n = a DIVRM b;     // 10 DIVRM 3 == 3
+    var b1 = n * b;
+    b1 = 4;
+    b1 = A * B;
+end;
+
+func main() => integer
+begin
+    myfunction(0, 1);
+    myfunction(A, 1);
+    myfunction(A DIVRM 2, B DIVRM 4);
+    return 0;
+end;
+
+