Merge pull request #225 from xbauch/feature/type-cast-range-check

Range check for non-bounded numeric types

Author: petr-bauch

experiments/golden-results/StratoX-summary.txt

@@ -8,7 +8,7 @@ Calling function: Process_Declaration
 Error message: Unknown declaration kind
 Nkind: N_Freeze_Generic_Entity
 --
-Occurs: 104 times
+Occurs: 105 times
 Calling function: Do_Function_Call
 Error message: func name not in symbol table
 Nkind: N_Function_Call
@@ -23,7 +23,7 @@ Calling function: Do_Type_Definition
 Error message: Access type unsupported
 Nkind: N_Access_To_Object_Definition
 --
-Occurs: 42 times
+Occurs: 43 times
 Calling function: Do_Expression
 Error message: Unknown attribute
 Nkind: N_Attribute_Reference
@@ -93,6 +93,11 @@ Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Global
 Nkind: N_Pragma
 --
+Occurs: 10 times
+Calling function: Process_Statement
+Error message: Raise statement
+Nkind: N_Raise_Statement
+--
 Occurs: 9 times
 Calling function: Process_Declaration
 Error message: Unknown declaration kind
@@ -103,11 +108,6 @@ Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Elaborate Body
 Nkind: N_Pragma
 --
-Occurs: 9 times
-Calling function: Process_Statement
-Error message: Raise statement
-Nkind: N_Raise_Statement
---
 Occurs: 8 times
 Calling function: Process_Declaration
 Error message: Generic instantiation declaration
@@ -193,6 +193,11 @@ Calling function: Do_Procedure_Call_Statement
 Error message: sym id not in symbol table
 Nkind: N_Procedure_Call_Statement
 --
+Occurs: 2 times
+Calling function: Do_Function_Call
+Error message: function entity not defining identifier
+Nkind: N_Function_Call
+--
 Occurs: 1 times
 Calling function: Do_Compilation_Unit
 Error message: Unknown tree node
@@ -204,11 +209,6 @@ Error message: Constant Type not in Class_Bitvector_Type
 Nkind: N_Integer_Literal
 --
 Occurs: 1 times
-Calling function: Do_Function_Call
-Error message: function entity not defining identifier
-Nkind: N_Function_Call
---
-Occurs: 1 times
 Calling function: Do_Itype_Integer_Subtype
 Error message: Non-literal bound unsupported
 Nkind: N_Defining_Identifier

gnat2goto/driver/range_check.adb

@@ -72,7 +72,56 @@ package body Range_Check is
       return All_Bounds_Table.Element (Bound_Index);
    end Get_Bound_Type;
 
-   function Get_Bound (Bound_Type : Irep; Pos : Bound_Low_Or_High) return Irep
+   function Get_Bound (N : Node_Id; Bound_Type : Irep; Pos : Bound_Low_Or_High)
+                             return Irep
+   is
+   begin
+      case Kind (Bound_Type) is
+         when I_Bounded_Signedbv_Type
+            | I_Bounded_Unsignedbv_Type
+            | I_Bounded_Floatbv_Type =>
+            return Get_Bound_Of_Bounded_Type (Bound_Type, Pos);
+         when I_Unsignedbv_Type =>
+            --  this case is probably unnecessary:
+            --  1: how does one create non-bounded unsigned types anyway
+            --  2: CBMC has facilities to check unsigned overflow
+            declare
+               Type_Width : constant Integer := Get_Width (Bound_Type);
+               Bound_Value : constant Uint :=
+                 (if Pos = Bound_Low
+                  then Uint_0
+                  else UI_From_Int (2 ** Type_Width - 1));
+            begin
+               return Make_Constant_Expr (Source_Location => No_Location,
+                                          I_Type          => Bound_Type,
+                                          Range_Check     => False,
+                                          Value =>
+                                            Convert_Uint_To_Hex (Bound_Value,
+                                              Types.Pos (Type_Width)));
+            end;
+         when I_Signedbv_Type =>
+            declare
+               Type_Width : constant Integer := Get_Width (Bound_Type);
+               Bound_Value : constant Uint :=
+                 (if Pos = Bound_Low
+                  then UI_From_Int (-(2 ** (Type_Width - 1)))
+                  else UI_From_Int (2 ** (Type_Width - 1) - 1));
+            begin
+               return Make_Constant_Expr (Source_Location => No_Location,
+                                          I_Type          => Bound_Type,
+                                          Range_Check     => False,
+                                          Value =>
+                                            Convert_Uint_To_Hex (Bound_Value,
+                                              Types.Pos (Type_Width)));
+            end;
+         when others =>
+               return Report_Unhandled_Node_Irep (N, "Get_Bound",
+                                                  "Unsupported range type");
+      end case;
+   end Get_Bound;
+
+   function Get_Bound_Of_Bounded_Type (Bound_Type : Irep;
+                                       Pos : Bound_Low_Or_High) return Irep
    is
       Bound_Index : constant Integer := (if Pos = Bound_Low
                                          then Get_Lower_Bound (Bound_Type)
@@ -93,7 +142,7 @@ package body Range_Check is
          when Symb_Bound =>
             return Load_Symbol_Bound (Bound_Index);
       end case;
-   end Get_Bound;
+   end Get_Bound_Of_Bounded_Type;
 
    ----------------------------
    -- Make_Range_Assert_Expr --
@@ -185,9 +234,9 @@ package body Range_Check is
       end Build_Assert_Function;
 
       Lower_Bound : constant Irep :=
-        Get_Bound (Followed_Bound_Type, Bound_Low);
+        Get_Bound (N, Followed_Bound_Type, Bound_Low);
       Upper_Bound : constant Irep :=
-        Get_Bound (Followed_Bound_Type, Bound_High);
+        Get_Bound (N, Followed_Bound_Type, Bound_High);
    begin
       Append_Argument (Call_Args, Value);
       Append_Argument (Call_Args, Lower_Bound);
@@ -230,7 +279,9 @@ package body Range_Check is
       pragma Assert (Kind (Bound_Type) in
                        I_Bounded_Unsignedbv_Type
                        | I_Bounded_Signedbv_Type
-                       | I_Bounded_Floatbv_Type);
+                       | I_Bounded_Floatbv_Type
+                       | I_Unsignedbv_Type
+                       | I_Signedbv_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

@@ -19,16 +19,27 @@ package Range_Check is
    function Store_Real_Bound (Number : Bound_Type_Real) return Integer;
    function Store_Symbol_Bound (Number : Bound_Type_Symbol) return Integer;
 
-   function Get_Bound (Bound_Type : Irep; Pos : Bound_Low_Or_High) return Irep
+   function Get_Bound (N : Node_Id; Bound_Type : Irep; Pos : Bound_Low_Or_High)
+                             return Irep
      with Pre => Kind (Bound_Type) in
      I_Bounded_Unsignedbv_Type | I_Bounded_Signedbv_Type
-     | I_Bounded_Floatbv_Type,
+     | I_Bounded_Floatbv_Type | I_Unsignedbv_Type | I_Signedbv_Type,
+
      Post => Kind (Get_Bound'Result) in Class_Expr;
 
+   function Get_Bound_Of_Bounded_Type (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,
+       Post => Kind (Get_Bound_Of_Bounded_Type'Result) in Class_Expr;
+
    function Make_Range_Assert_Expr (N : Node_Id; Value : Irep;
                                     Bounds_Type : Irep) return Irep
      with Pre => Kind (Bounds_Type) in
-     I_Bounded_Signedbv_Type | I_Bounded_Floatbv_Type | I_Symbol_Type;
+     I_Bounded_Signedbv_Type | I_Bounded_Floatbv_Type | I_Symbol_Type
+       | I_Unsignedbv_Type | I_Signedbv_Type;
 
    function Make_Range_Expression (Value_Expr : Irep; Lower_Bound : Irep;
                                    Upper_Bound : Irep)

gnat2goto/driver/tree_walk.adb

@@ -1541,12 +1541,17 @@ package body Tree_Walk is
    begin
       --  TODO: Range expressions for non-bounded types are outside
       --        the scope of this PR
-      if Kind (Type_Of_Val) in I_Bounded_Signedbv_Type | I_Bounded_Floatbv_Type
-      then
-         return Make_Range_Assert_Expr (N, Typecast_Expr, Type_Of_Val);
-      else
-         return Typecast_Expr;
-      end if;
+      case Kind (Type_Of_Val) is
+         when I_Bounded_Signedbv_Type
+            | I_Bounded_Floatbv_Type
+            | I_Bounded_Unsignedbv_Type
+            | I_Unsignedbv_Type
+            | I_Signedbv_Type
+            | I_Bounded_Mod_Type =>
+            return Make_Range_Assert_Expr (N, Typecast_Expr, Type_Of_Val);
+         when others =>
+            return Typecast_Expr;
+      end case;
    end Do_Qualified_Expression;
 
    -----------------------------
@@ -1592,8 +1597,8 @@ package body Tree_Walk is
                Set_Lhs (Assume_And_Yield,
                         Make_Assume_Expr (N,
                           Make_Range_Expression (Sym_Nondet,
-                            Get_Bound (Followed_Type, Bound_Low),
-                            Get_Bound (Followed_Type, Bound_High))));
+                            Get_Bound (N, Followed_Type, Bound_Low),
+                            Get_Bound (N, Followed_Type, Bound_High))));
             else
                Set_Lhs (Assume_And_Yield,
                         Make_Assume_Expr (N,

testsuite/gnat2goto/tests/range_check_non_bounded/test.adb

@@ -0,0 +1,8 @@
+procedure Test is
+   type Uint_8 is mod 2**8;
+   Uint_Var : Uint_8 := 5;
+   Int_Var : Integer;
+begin
+   Int_Var := Integer'(Integer (Uint_Var));
+   pragma Assert (Int_Var = 5);
+end Test;

testsuite/gnat2goto/tests/range_check_non_bounded/test.out

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

testsuite/gnat2goto/tests/range_check_non_bounded/test.py

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