[asl] Change type of index in for loop

herd · Aug 5, 2024 · 1dd0a7f · 1dd0a7f
1 parent 946b3a8
commit 1dd0a7f
Show file tree

Hide file tree

Showing 4 changed files with 31 additions and 79 deletions.
diff --git a/asllib/Typing.ml b/asllib/Typing.ml
@@ -35,7 +35,6 @@ let unsupported_expr e = Error.fatal_from e Error.(UnsupportedExpr (Static, e))
 let conflict pos expected provided =
   fatal_from pos (Error.ConflictingTypes (expected, provided))
 
-let expr_of_z z = literal (L_Int z)
 let plus = binop PLUS
 let t_bits_bitwidth e = T_Bits (e, [])
 
@@ -133,50 +132,6 @@ let annotate_literal = function
   | L_BitVector bv -> Bitvector.length bv |> expr_of_int |> t_bits_bitwidth
 (* End *)
 
-exception ConstraintMinMaxTop
-
-let min_constraint env = function
-  | Constraint_Exact e | Constraint_Range (e, _) -> (
-      let e = StaticModel.try_normalize env e in
-      match e.desc with
-      | E_Literal (L_Int i) -> i
-      | _ ->
-          let () =
-            if false then
-              Format.eprintf "Min constraint found strange value %a@."
-                PP.pp_expr e
-          in
-          raise ConstraintMinMaxTop)
-
-let max_constraint env = function
-  | Constraint_Exact e | Constraint_Range (_, e) -> (
-      let e = StaticModel.try_normalize env e in
-      match e.desc with
-      | E_Literal (L_Int i) -> i
-      | _ ->
-          let () =
-            if false then
-              Format.eprintf "Max constraint found strange value %a@."
-                PP.pp_expr e
-          in
-          raise ConstraintMinMaxTop)
-
-let min_max_constraints m_constraint m =
-  let rec do_rec env = function
-    | [] ->
-        failwith
-          "A well-constrained integer cannot have an empty list of constraints."
-    | [ c ] -> m_constraint env c
-    | c :: cs ->
-        let i = m_constraint env c and j = do_rec env cs in
-        m i j
-  in
-  do_rec
-
-(* NB: functions raise [ConstraintMinMaxTop] if no approximation can be found *)
-let min_constraints = min_max_constraints min_constraint min
-and max_constraints = min_max_constraints max_constraint max
-
 let get_first_duplicate extractor li =
   let exception Duplicate of identifier in
   let folder acc elt =
@@ -2238,33 +2193,19 @@ module Annotate (C : ANNOTATE_CONFIG) = struct
     (* Begin SFor *)
     | S_For (id, e1, dir, e2, s') ->
         let t1, e1' = annotate_expr env e1 and t2, e2' = annotate_expr env e2 in
-        let struct1 = Types.get_well_constrained_structure env t1
-        and struct2 = Types.get_well_constrained_structure env t2 in
+        let struct1 = Types.make_anonymous env t1
+        and struct2 = Types.make_anonymous env t2 in
         let cs =
           match (struct1.desc, struct2.desc) with
           | T_Int UnConstrained, T_Int _ | T_Int _, T_Int UnConstrained ->
               UnConstrained
-          | T_Int (WellConstrained cs1), T_Int (WellConstrained cs2) -> (
-              let bot_cs, top_cs =
-                match dir with Up -> (cs1, cs2) | Down -> (cs2, cs1)
+          | T_Int _, T_Int _ ->
+              let e1n = StaticModel.try_normalize env e1'
+              and e2n = StaticModel.try_normalize env e2' in
+              let e_bot, e_top =
+                match dir with Up -> (e1n, e2n) | Down -> (e2n, e1n)
               in
-              try
-                let bot = min_constraints env bot_cs
-                and top = max_constraints env top_cs in
-                if bot <= top then
-                  WellConstrained
-                    [ Constraint_Range (expr_of_z bot, expr_of_z top) ]
-                else WellConstrained cs1
-              with ConstraintMinMaxTop -> (
-                match (bot_cs, top_cs) with
-                | [ Constraint_Exact e_bot ], [ Constraint_Exact e_top ] ->
-                    WellConstrained [ Constraint_Range (e_bot, e_top) ]
-                | _ ->
-                    (* TODO: this case is not specified by the LRM. *)
-                    UnConstrained))
-          | T_Int (UnderConstrained _), T_Int _
-          | T_Int _, T_Int (UnderConstrained _) ->
-              assert false
+              WellConstrained [ Constraint_Range (e_bot, e_top) ]
           | T_Int _, _ -> conflict s [ integer' ] t2
           | _, _ -> conflict s [ integer' ] t1
           (* only happens in relaxed type-checking mode because of check_structure_integer earlier. *)

diff --git a/asllib/tests/typing.t/TPositive8-1.asl b/asllib/tests/typing.t/TPositive8-1.asl
@@ -0,0 +1,8 @@
+func tpositive8b ()
+begin
+    // NOTE: this test is not supported by ASLRef.
+    for i = 100 as integer {8,16} to 110 as integer {0,31} do
+        let testK : integer {8..31} = i;
+    end
+end
+
diff --git a/asllib/tests/typing.t/TPositive8.asl b/asllib/tests/typing.t/TPositive8.asl
@@ -3,21 +3,20 @@
 ////////////////////////////////////////////////////////////////////////////////
 func positive8(N : integer {0..15}, M : integer {7,15})
 begin
-    // Loop iterators are constrained integers with the constranints based on the constraints (not the values) of the range
     for i = 0 to 7 do
-        // i has type integer {0..7} because the type of the start index is integer {0} and the end is integer {7}
+        // i has type integer {0..7}
         let testA : integer {0..7} = i;
     end
     for i = 7 downto 0 do
-        // i has type integer {0..7} because the type of the start index is integer {7} and the end is integer {0}
+        // i has type integer {0..7}
         let testB : integer {0..7} = i;
     end
     for i = 0 to N do
-        // i has type integer {0..15} because the type of the start index is integer {0} and the max value in the domain of N is 15
+        // i has type integer {0..N}
         let testC : integer {0..15} = i;
     end
     for i = 0 to M do
-        // i has type integer {0..15} because the type of the start index is integer {0} and the max value in the domain of M is 15
+        // i has type integer {0..M}
         let testD : integer {0..15} = i;
     end
     for i = N downto 0 do
@@ -27,21 +26,16 @@ begin
         let testF : integer {0..15} = i;
     end
     for i = N to 31 do
-        let testG : integer {0..31} = i; // i has type integer {0..31} as the min value in the domain of N is 0
+        let testG : integer {0..31} = i; // i has type integer {N..31}
     end
     for i = M to 31 do
-        let testH : integer {7..31} = i; // i has type integer {7..31} as the min value in the domain of M is 7
+        let testH : integer {7..31} = i; // i has type integer {M..31}
     end
     for i = 31 downto N do
         let testI : integer {0..31} = i;
     end
     for i = 31 downto M do
         let testJ : integer {7..31} = i;
     end
-    // NOTE: testK is required to be legal staticaly, but the ATC's will fail at runtime if this code is reached
-    for i = 100 as integer {8,16} to 110 as integer {0,31} do
-        let testK : integer {8..31} = i; // i has type integer {8..31} as the min value of the domain of the start
-                                         // expression is 8, and the max value of the domain of the end expression is 31.
-    end
 end
 
diff --git a/asllib/tests/typing.t/run.t b/asllib/tests/typing.t/run.t
@@ -111,6 +111,15 @@ Named types
 
 Loops
   $ aslref --no-exec TPositive8.asl
+  File TPositive8.asl, line 16, characters 8 to 40:
+  ASL Typing error: a subtype of integer {0..15} was expected,
+    provided integer {0..N}.
+  [1]
+  $ aslref --no-exec TPositive8-1.asl
+  File TPositive8-1.asl, line 5, characters 8 to 40:
+  ASL Typing error: a subtype of integer {8..31} was expected,
+    provided integer {100..110}.
+  [1]
   $ aslref --no-exec TNegative8-0.asl
   File TNegative8-0.asl, line 5, characters 8 to 40:
   ASL Typing error: a subtype of integer {0..7} was expected, provided integer.