Modular subtype

experiments/golden-results/StratoX-summary.txt

@@ -3,12 +3,12 @@ Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Postcondition
 Nkind: N_Pragma
 --
-Occurs: 168 times
+Occurs: 134 times
 Calling function: Process_Declaration
 Error message: Unknown declaration kind
 Nkind: N_Freeze_Generic_Entity
 --
-Occurs: 147 times
+Occurs: 102 times
 Calling function: Do_Function_Call
 Error message: func name not in symbol table
 Nkind: N_Function_Call
@@ -19,26 +19,26 @@ Error message: Generic declaration
 Nkind: N_Generic_Subprogram_Declaration
 --
 Occurs: 50 times
-Calling function: Do_Expression
-Error message: Unknown attribute
-Nkind: N_Attribute_Reference
---
-Occurs: 50 times
 Calling function: Do_Type_Definition
 Error message: Access type unsupported
 Nkind: N_Access_To_Object_Definition
 --
+Occurs: 42 times
+Calling function: Do_Expression
+Error message: Unknown attribute
+Nkind: N_Attribute_Reference
+--
 Occurs: 35 times
 Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: No strict aliasing
 Nkind: N_Pragma
 --
-Occurs: 32 times
+Occurs: 31 times
 Calling function: Process_Declaration
 Error message: Package declaration
 Nkind: N_Package_Declaration
 --
-Occurs: 24 times
+Occurs: 23 times
 Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Check
 Nkind: N_Pragma
@@ -78,11 +78,6 @@ Calling function: Process_Declaration
 Error message: Generic instantiation declaration
 Nkind: N_Function_Instantiation
 --
-Occurs: 12 times
-Calling function: Do_Constant
-Error message: Constant Type not in symbol table
-Nkind: N_Integer_Literal
---
 Occurs: 11 times
 Calling function: Do_Expression
 Error message: In
@@ -139,6 +134,11 @@ Error message: Unsupported pragma: Suppress initialization
 Nkind: N_Pragma
 --
 Occurs: 6 times
+Calling function: Do_Constant
+Error message: Constant Type not in symbol table
+Nkind: N_Integer_Literal
+--
+Occurs: 6 times
 Calling function: Process_Declaration
 Error message: Generic instantiation declaration
 Nkind: N_Procedure_Instantiation

experiments/golden-results/UKNI-Information-Barrier-summary.txt

@@ -19,11 +19,6 @@ Error message: Unknown expression kind
 Nkind: N_Expanded_Name
 --
 Occurs: 5 times
-Calling function: Do_Itype_Definition
-Error message: Unknown Ekind
-Nkind: N_Defining_Identifier
---
-Occurs: 5 times
 Calling function: Do_Procedure_Call_Statement
 Error message: sym id not in symbol table
 Nkind: N_Procedure_Call_Statement
@@ -34,6 +29,16 @@ Error message: Wrong Nkind spec
 Nkind: N_Loop_Statement
 --
 Occurs: 1 times
+Calling function: Do_Base_Range_Constraint
+Error message: unsupported lower range kind
+Nkind: N_Attribute_Reference
+--
+Occurs: 1 times
+Calling function: Do_Base_Range_Constraint
+Error message: unsupported upper range kind
+Nkind: N_Attribute_Reference
+--
+Occurs: 1 times
 Calling function: Do_Operator_General
 Error message: Mod of unsupported type
 Nkind: N_Op_Not

experiments/golden-results/muen-summary.txt

@@ -53,11 +53,6 @@ Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Initializes
 Nkind: N_Pragma
 --
-Occurs: 10 times
-Calling function: Do_Constant
-Error message: Constant Type not in symbol table
-Nkind: N_Integer_Literal
---
 Occurs: 8 times
 Calling function: Process_Declaration
 Error message: Use type clause declaration
@@ -79,6 +74,11 @@ Error message: Unsupported pragma: Precondition
 Nkind: N_Pragma
 --
 Occurs: 7 times
+Calling function: Do_Constant
+Error message: Constant Type not in symbol table
+Nkind: N_Integer_Literal
+--
+Occurs: 7 times
 Calling function: Do_Function_Call
 Error message: func name not in symbol table
 Nkind: N_Function_Call

gnat2goto/driver/gnat2goto_itypes.adb

@@ -6,6 +6,7 @@ with GOTO_Utils;            use GOTO_Utils;
 with Range_Check;           use Range_Check;
 with Symbol_Table_Info;     use Symbol_Table_Info;
 with Tree_Walk;             use Tree_Walk;
+with Follow;                use Follow;
 
 package body Gnat2goto_Itypes is
 
@@ -89,7 +90,8 @@ package body Gnat2goto_Itypes is
          when E_Signed_Integer_Type => Do_Itype_Integer_Type (N),
          when E_Floating_Point_Type => Create_Dummy_Irep,
          when E_Anonymous_Access_Type => Make_Pointer_Type
-        (Base => Do_Type_Reference (Designated_Type (Etype (N)))),
+                (Base => Do_Type_Reference (Designated_Type (Etype (N)))),
+         when E_Modular_Integer_Subtype => Do_Modular_Integer_Subtype (N),
          when others => Report_Unhandled_Node_Irep (N, "Do_Itype_Definition",
                                                     "Unknown Ekind"));
    end Do_Itype_Definition;
@@ -171,4 +173,58 @@ package body Gnat2goto_Itypes is
       return Do_Type_Reference (Etype (N));
    end Do_Itype_Record_Subtype;
 
+   function Do_Modular_Integer_Subtype (N : Entity_Id) return Irep is
+      Modular_Type : constant Irep := Do_Type_Reference (Etype (N));
+      Followed_Mod_Type : constant Irep :=
+        Follow_Symbol_Type (Modular_Type, Global_Symbol_Table);
+
+      S_Range : constant Node_Id := Scalar_Range (N);
+      Lower_Bound : constant Node_Id := Low_Bound (S_Range);
+      Upper_Bound : constant Node_Id := High_Bound (S_Range);
+
+      Lower_Bound_Value : Integer;
+      Upper_Bound_Value : Integer;
+   begin
+      pragma Assert (Kind (Followed_Mod_Type) in I_Unsignedbv_Type
+                       | I_Ada_Mod_Type);
+
+      case Nkind (Lower_Bound) is
+         when N_Integer_Literal => Lower_Bound_Value :=
+              Store_Nat_Bound (Bound_Type_Nat (Intval (Lower_Bound)));
+         when N_Identifier => Lower_Bound_Value :=
+              Store_Symbol_Bound (Bound_Type_Symbol (Lower_Bound));
+         when others =>
+            Report_Unhandled_Node_Empty (Lower_Bound,
+                                         "Do_Base_Range_Constraint",
+                                         "unsupported lower range kind");
+      end case;
+
+      case Nkind (Upper_Bound) is
+         when N_Integer_Literal => Upper_Bound_Value :=
+              Store_Nat_Bound (Bound_Type_Nat (Intval (Upper_Bound)));
+         when N_Identifier => Upper_Bound_Value :=
+              Store_Symbol_Bound (Bound_Type_Symbol (Upper_Bound));
+         when others =>
+            Report_Unhandled_Node_Empty (Upper_Bound,
+                                         "Do_Base_Range_Constraint",
+                                         "unsupported upper range kind");
+      end case;
+
+      if Kind (Followed_Mod_Type) = I_Ada_Mod_Type then
+         return Make_Bounded_Mod_Type (I_Subtype   => Make_Nil_Type,
+                                       Width       =>
+                                         Get_Width (Followed_Mod_Type),
+                                       Lower_Bound => Lower_Bound_Value,
+                                       Ada_Mod_Max =>
+                                         Get_Ada_Mod_Max (Followed_Mod_Type),
+                                       Upper_Bound => Upper_Bound_Value);
+      else
+         return Make_Bounded_Unsignedbv_Type (I_Subtype   => Make_Nil_Type,
+                                              Width       =>
+                                                Get_Width (Followed_Mod_Type),
+                                              Lower_Bound => Lower_Bound_Value,
+                                             Upper_Bound => Upper_Bound_Value);
+      end if;
+   end Do_Modular_Integer_Subtype;
+
 end Gnat2goto_Itypes;

gnat2goto/driver/gnat2goto_itypes.ads

@@ -30,4 +30,7 @@ private
    function Do_Itype_Record_Subtype (N : Entity_Id) return Irep
      with Pre => Is_Itype (N) and then Ekind (N) = E_Record_Subtype;
 
+   function Do_Modular_Integer_Subtype (N : Entity_Id) return Irep
+     with Pre => Is_Itype (N) and then Ekind (N) = E_Modular_Integer_Subtype;
+
 end Gnat2goto_Itypes;

gnat2goto/driver/range_check.adb

@@ -228,7 +228,9 @@ package body Range_Check is
         (Value_Expr);
    begin
       pragma Assert (Kind (Bound_Type) in
-                       I_Bounded_Signedbv_Type | I_Bounded_Floatbv_Type);
+                       I_Bounded_Unsignedbv_Type
+                       | I_Bounded_Signedbv_Type
+                       | I_Bounded_Floatbv_Type);
       --  The compared expressions (value and bound) have to be of the
       --  same type
       if Get_Width (Bound_Type) > Get_Width (Value_Expr_Type)

gnat2goto/driver/range_check.ads

@@ -21,7 +21,8 @@ package Range_Check is
 
    function Get_Bound (Bound_Type : Irep; Pos : Bound_Low_Or_High) return Irep
      with Pre => Kind (Bound_Type) in
-     I_Bounded_Signedbv_Type | I_Bounded_Floatbv_Type,
+     I_Bounded_Unsignedbv_Type | I_Bounded_Signedbv_Type
+     | I_Bounded_Floatbv_Type,
      Post => Kind (Get_Bound'Result) in Class_Expr;
 
    function Make_Range_Assert_Expr (N : Node_Id; Value : Irep;

gnat2goto/driver/tree_walk.adb

@@ -754,7 +754,10 @@ package body Tree_Walk is
       Lower_Bound_Value : Integer;
       Upper_Bound_Value : Integer;
 
-      Result_Type : constant Irep := New_Irep (I_Bounded_Signedbv_Type);
+      Result_Type : constant Irep :=
+        New_Irep (if Kind (Resolved_Underlying) = I_Ada_Mod_Type
+                    then I_Bounded_Unsignedbv_Type
+                    else I_Bounded_Signedbv_Type);
    begin
       if not (Kind (Resolved_Underlying) in Class_Bitvector_Type or
               Kind (Resolved_Underlying) = I_C_Enum_Type)
@@ -771,7 +774,8 @@ package body Tree_Walk is
               Store_Symbol_Bound (Get_Array_Attr_Bound_Symbol (Lower_Bound));
          when N_Identifier =>
             Lower_Bound_Value :=
-               Store_Symbol_Bound (Bound_Type_Symbol (Lower_Bound));
+              Store_Symbol_Bound (Bound_Type_Symbol (
+                                   Do_Identifier (Lower_Bound)));
          when others =>
             Report_Unhandled_Node_Empty (Lower_Bound,
                                          "Do_Base_Range_Constraint",
@@ -785,7 +789,8 @@ package body Tree_Walk is
               Store_Symbol_Bound (Get_Array_Attr_Bound_Symbol (Upper_Bound));
          when N_Identifier =>
             Upper_Bound_Value :=
-               Store_Symbol_Bound (Bound_Type_Symbol (Upper_Bound));
+              Store_Symbol_Bound (Bound_Type_Symbol (
+                                   Do_Identifier (Upper_Bound)));
          when others =>
             Report_Unhandled_Node_Empty (Upper_Bound,
                                          "Do_Base_Range_Constraint",
@@ -2961,7 +2966,8 @@ package body Tree_Walk is
 
       if Init_Expr /= Ireps.Empty then
          Append_Op (Block, Make_Code_Assign (Lhs => Id,
-                                             Rhs => Init_Expr,
+                Rhs => Typecast_If_Necessary (Init_Expr, Get_Type (Id),
+                                              Global_Symbol_Table),
                                              Source_Location => Sloc (N)));
       end if;
 

gnat2goto/ireps/irep_specs/bounded_mod_type.json

@@ -0,0 +1,9 @@
+{
+   "parent": "bitvector_type",
+   "id": "bounded_mod_type",
+   "namedSub": {
+      "lower_bound": {"type": "integer"},
+      "upper_bound": {"type": "integer"},
+      "ada_mod_max": {"type": "string"}
+   }
+}

gnat2goto/ireps/irep_specs/bounded_unsignedbv_type.json

@@ -0,0 +1,7 @@
+{
+  "parent": "bitvector_type",
+  "namedSub": {
+    "lower_bound": {"type": "integer"},
+    "upper_bound": {"type": "integer"}
+  }
+}

gnat2goto/ireps/ireps_generator.py

@@ -2055,6 +2055,16 @@ def generate_code(self, optimize, schema_file_names):
         with indent(b):
             write(b, "return Make_Floatbv_Type (Get_Subtype (I), Get_Width (I), Get_F (I));")
         write(b, "end if;")
+        write(b, "")
+        write(b, "if Kind (I) = I_Bounded_Unsignedbv_Type then")
+        with indent(b):
+            write(b, "return Make_Unsignedbv_Type (Get_Subtype (I), Get_Width (I));")
+        write(b, "end if;")
+        write(b, "")
+        write(b, "if Kind (I) = I_Bounded_Mod_Type then")
+        with indent(b):
+            write(b, "return Make_Unsignedbv_Type (Get_Subtype (I), Get_Width (I));")
+        write(b, "end if;")
         write(b, "if Kind (I) = I_Ada_Mod_Type then")
         with indent(b):
             write(b, "return Make_Unsignedbv_Type (Make_Nil_Type, Get_Width (I));")

testsuite/gnat2goto/tests/loop_range_mod_type/test.adb

@@ -0,0 +1,33 @@
+procedure Test is
+   type Unsigned_16 is mod 2 ** 4;
+   RAM_Start : constant Unsigned_16 := 5;
+   RAM_End   : constant Unsigned_16 := 12;
+   Sum : Unsigned_16 := 0;
+
+   Test_Passed   : Boolean := True;
+
+   subtype Sub16 is Unsigned_16 range RAM_Start .. RAM_End;
+   SubVar : Sub16 := RAM_Start;
+
+   function Address_OK
+     (Address    : in Unsigned_16) return Boolean;
+   function Address_OK
+     (Address    : in Unsigned_16)
+     return Boolean
+   is
+   begin
+      Sum := Sum + 1;
+      return Test_Passed;
+   end Address_OK;
+begin
+   SubVar := SubVar + 1; -- invokes range check
+   for I in Unsigned_16 range RAM_Start .. RAM_End loop
+      if Address_OK (Address => I)
+      then
+         Test_Passed := False;
+      end if;
+
+   end loop;
+   pragma Assert (Sum = RAM_End - RAM_Start + 1);
+
+end Test;

testsuite/gnat2goto/tests/loop_range_mod_type/test.out

@@ -0,0 +1,3 @@
+[assertion.1] Range Check: SUCCESS
+[1] file test.adb line 31 assertion: SUCCESS
+VERIFICATION SUCCESSFUL

testsuite/gnat2goto/tests/loop_range_mod_type/test.py

@@ -0,0 +1,3 @@
+from test_support import *
+
+prove()