Merge pull request #238 from NlightNFotis/Range_Exception

Fix UKNI range issue, and add symbols earlier to the symbol table

Author: NlightNFotis

experiments/golden-results/SPARK-tetris-summary.txt

@@ -3,11 +3,6 @@ Calling function: Process_Declaration
 Error message: Package declaration
 Nkind: N_Package_Declaration
 --
-Occurs: 10 times
-Calling function: Do_Base_Range_Constraint
-Error message: range expression not bitvector type
-Nkind: N_Range
---
 Occurs: 9 times
 Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Volatile

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: 157 times
+Occurs: 155 times
 Calling function: Do_Function_Call
 Error message: func name not in symbol table
 Nkind: N_Function_Call
@@ -74,15 +74,15 @@ Error message: Unknown declaration kind
 Nkind: N_Null_Statement
 --
 Occurs: 13 times
-Calling function: Do_Constant
-Error message: Constant Type not in symbol table
-Nkind: N_Integer_Literal
---
-Occurs: 13 times
 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
@@ -104,21 +104,11 @@ Error message: Unsupported pragma: Global
 Nkind: N_Pragma
 --
 Occurs: 9 times
-Calling function: Do_Procedure_Call_Statement
-Error message: sym id not in symbol table
-Nkind: N_Procedure_Call_Statement
---
-Occurs: 9 times
 Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Elaborate Body
 Nkind: N_Pragma
 --
 Occurs: 8 times
-Calling function: Do_Base_Range_Constraint
-Error message: range expression not bitvector type
-Nkind: N_Range
---
-Occurs: 8 times
 Calling function: Process_Declaration
 Error message: Generic instantiation declaration
 Nkind: N_Package_Instantiation
@@ -204,6 +194,11 @@ Error message: Generic declaration
 Nkind: N_Generic_Package_Declaration
 --
 Occurs: 3 times
+Calling function: Do_Procedure_Call_Statement
+Error message: sym id not in symbol table
+Nkind: N_Procedure_Call_Statement
+--
+Occurs: 3 times
 Calling function: Process_Statement
 Error message: Unknown expression kind
 Nkind: N_Object_Declaration

experiments/golden-results/Tokeneer-summary.txt

@@ -84,16 +84,6 @@ Error message: Abstract type declaration unsupported
 Nkind: N_Private_Type_Declaration
 --
 Occurs: 8 times
-Calling function: Do_Base_Range_Constraint
-Error message: range expression not bitvector type
-Nkind: N_Range
---
-Occurs: 8 times
-Calling function: Do_Base_Range_Constraint
-Error message: unsupported upper range kind
-Nkind: N_Identifier
---
-Occurs: 8 times
 Calling function: Process_Pragma_Declaration
 Error message: Unknown pragma
 Nkind: N_Pragma

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

@@ -18,11 +18,6 @@ Calling function: Do_Itype_Definition
 Error message: Unknown Ekind
 Nkind: N_Defining_Identifier
 --
-Occurs: 2 times
-Calling function: Do_Base_Range_Constraint
-Error message: range expression not bitvector type
-Nkind: N_Range
---
 Occurs: 1 times
 Calling function: Process_Declaration
 Error message: Use package clause declaration

experiments/golden-results/muen-summary.txt

@@ -54,16 +54,16 @@ Error message: Unsupported pragma: Abstract state
 Nkind: N_Pragma
 --
 Occurs: 11 times
-Calling function: Do_Constant
-Error message: Constant Type not in symbol table
-Nkind: N_Integer_Literal
---
-Occurs: 11 times
 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: 10 times
 Calling function: Do_Type_Definition
 Error message: Unknown expression kind
 Nkind: N_Access_Function_Definition
@@ -73,11 +73,6 @@ Calling function: Process_Declaration
 Error message: Package declaration
 Nkind: N_Package_Declaration
 --
-Occurs: 9 times
-Calling function: Do_Function_Call
-Error message: func name not in symbol table
-Nkind: N_Function_Call
---
 Occurs: 8 times
 Calling function: Do_Itype_Integer_Subtype
 Error message: Non-literal bound unsupported
@@ -99,16 +94,16 @@ Error message: Unsupported pragma: Global
 Nkind: N_Pragma
 --
 Occurs: 7 times
+Calling function: Do_Function_Call
+Error message: func name not in symbol table
+Nkind: N_Function_Call
+--
+Occurs: 7 times
 Calling function: Process_Declaration
 Error message: Generic instantiation declaration
 Nkind: N_Function_Instantiation
 --
 Occurs: 6 times
-Calling function: Do_Base_Range_Constraint
-Error message: range expression not bitvector type
-Nkind: N_Range
---
-Occurs: 6 times
 Calling function: Process_Pragma_Declaration
 Error message: Unsupported pragma: Precondition
 Nkind: N_Pragma
@@ -149,11 +144,6 @@ Error message: Etype not a type
 Nkind: N_Identifier
 --
 Occurs: 2 times
-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_Type_Definition
 Error message: Unknown expression kind
 Nkind: N_Access_Procedure_Definition

experiments/golden-results/vct-summary.txt

@@ -3,11 +3,6 @@ Calling function: Process_Declaration
 Error message: Exception declaration
 Nkind: N_Exception_Declaration
 --
-Occurs: 32 times
-Calling function: Do_Base_Range_Constraint
-Error message: unsupported upper range kind
-Nkind: N_Identifier
---
 Occurs: 18 times
 Calling function: Do_Operator_General
 Error message: Concat unsupported
@@ -132,3 +127,13 @@ Occurs: 1 times
 +===========================GNAT BUG DETECTED==============================+
 | GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:29|
 | Error detected at system.ads:156:5                                       |
+--
+Occurs: 1 times
++===========================GNAT BUG DETECTED==============================+
+| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:29|
+| Error detected at system.ads:156:5                                       |
+--
+Occurs: 1 times
++===========================GNAT BUG DETECTED==============================+
+| GNU Ada (ada2goto) Assert_Failure failed precondition from range_check.ads:29|
+| Error detected at system.ads:156:5                                       |

gnat2goto/driver/goto_utils.adb

@@ -473,4 +473,21 @@ package body GOTO_Utils is
            (Get_Type (Function_Expr)),
          Source_Location => Source_Location);
    end Make_Simple_Side_Effect_Expr_Function_Call;
+
+   procedure Register_Identifier_In_Symbol_Table
+      (N : Irep; Val : Irep; Symtab : in out Symbol_Table) is
+      Identifier_Name : constant Symbol_Id :=
+         Intern (Get_Identifier (N));
+      Identifier_Symbol : Symbol;
+   begin
+      Identifier_Symbol.Name       := Identifier_Name;
+      Identifier_Symbol.BaseName   := Identifier_Name;
+      Identifier_Symbol.PrettyName := Identifier_Name;
+      Identifier_Symbol.SymType    := Get_Type (N);
+      Identifier_Symbol.IsLValue   := True;
+      Identifier_Symbol.IsStaticLifetime := True;
+      Identifier_Symbol.Mode       := Intern ("C");
+      Identifier_Symbol.Value      := Val;
+      Symtab.Insert (Identifier_Name, Identifier_Symbol);
+   end Register_Identifier_In_Symbol_Table;
 end GOTO_Utils;

gnat2goto/driver/goto_utils.ads

@@ -138,4 +138,8 @@ package GOTO_Utils is
       Function_Expr : Irep;
       Source_Location : Source_Ptr) return Irep;
 
+   procedure Register_Identifier_In_Symbol_Table
+      (N : Irep; Val : Irep; Symtab : in out Symbol_Table)
+      with Pre => Kind (N) = I_Symbol_Expr;
+
 end GOTO_Utils;

gnat2goto/driver/tree_walk.adb

@@ -743,7 +743,9 @@ package body Tree_Walk is
 
       Result_Type : constant Irep := New_Irep (I_Bounded_Signedbv_Type);
    begin
-      if not (Kind (Resolved_Underlying) in Class_Bitvector_Type) then
+      if not (Kind (Resolved_Underlying) in Class_Bitvector_Type or
+              Kind (Resolved_Underlying) = I_C_Enum_Type)
+      then
          return Report_Unhandled_Node_Type (Range_Expr,
                                             "Do_Base_Range_Constraint",
                                         "range expression not bitvector type");
@@ -754,6 +756,9 @@ package body Tree_Walk is
               Store_Nat_Bound (Bound_Type_Nat (Intval (Lower_Bound)));
          when N_Attribute_Reference => Lower_Bound_Value :=
               Store_Symbol_Bound (Get_Array_Attr_Bound_Symbol (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",
@@ -765,13 +770,21 @@ package body Tree_Walk is
               Store_Nat_Bound (Bound_Type_Nat (Intval (Upper_Bound)));
          when N_Attribute_Reference => Upper_Bound_Value :=
               Store_Symbol_Bound (Get_Array_Attr_Bound_Symbol (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;
 
-      Set_Width (Result_Type, Get_Width (Resolved_Underlying));
+      if Kind (Resolved_Underlying) = I_C_Enum_Type then
+         Set_Width (Result_Type,
+          Get_Width (Get_Subtype (Resolved_Underlying)));
+      else
+         Set_Width (Result_Type, Get_Width (Resolved_Underlying));
+      end if;
       Set_Lower_Bound (Result_Type, Lower_Bound_Value);
       Set_Upper_Bound (Result_Type, Upper_Bound_Value);
       return Result_Type;
@@ -792,23 +805,46 @@ package body Tree_Walk is
 
       procedure Handle_Parameter (Formal : Entity_Id; Actual : Node_Id);
 
+      function Handle_Enum_Symbol_Members (Mem : Irep) return Irep;
+      function Handle_Enum_Symbol_Members (Mem : Irep) return Irep is
+         Followed_Type_Symbol : constant Irep :=
+            Follow_Symbol_Type (Get_Type (Mem), Global_Symbol_Table);
+      begin
+         if Kind (Followed_Type_Symbol) = I_C_Enum_Type then
+            declare
+               Val : constant Irep := Global_Symbol_Table
+                 (Intern
+                    (Get_Identifier
+                     (Mem)))
+                 .Value;
+            begin
+               return
+                 (if Kind (Val) = I_Op_Typecast
+                  then Get_Op0 (Val) else Val);
+            end;
+         else
+            return Mem;
+         end if;
+      end Handle_Enum_Symbol_Members;
+
       ----------------------
       -- Handle_Parameter --
       ----------------------
 
       procedure Handle_Parameter (Formal : Entity_Id; Actual : Node_Id) is
          Is_Out        : constant Boolean := Out_Present (Parent (Formal));
          Actual_Irep   : Irep;
-
+         Expression    : constant Irep := Do_Expression (Actual);
       begin
          if Is_Out and then
-           not (Kind (Get_Type (Do_Expression (Actual))) in Class_Type)
+           not (Kind (Get_Type (Expression)) in Class_Type)
          then
             Report_Unhandled_Node_Empty (Actual, "Handle_Parameter",
                                          "Kind of actual not in class type");
             return;
          end if;
-         Actual_Irep := Wrap_Argument (Do_Expression (Actual), Is_Out);
+         Actual_Irep := Wrap_Argument (
+          Handle_Enum_Symbol_Members (Expression), Is_Out);
          Append_Argument (Args, Actual_Irep);
       end Handle_Parameter;
 
@@ -2882,6 +2918,8 @@ package body Tree_Walk is
 
       --  Begin processing for Do_Object_Declaration_Full_Declaration
 
+      Is_In_Symtab : constant Boolean :=
+        Global_Symbol_Table.Contains (Intern (Get_Identifier (Id)));
    begin
       Set_Source_Location (Decl, (Sloc (N)));
       Set_Symbol (Decl, Id);
@@ -2907,6 +2945,12 @@ package body Tree_Walk is
                                              Rhs => Init_Expr,
                                              Source_Location => Sloc (N)));
       end if;
+
+      if not Is_In_Symtab then
+         Register_Identifier_In_Symbol_Table
+            (Id, Init_Expr, Global_Symbol_Table);
+      end if;
+
    end Do_Object_Declaration_Full;
 
    -------------------------

testsuite/gnat2goto/tests/enum_symbols_range_constraint/range_constraint.adb

@@ -0,0 +1,14 @@
+procedure Range_Constraint is
+  type Indicator_Type is (
+    CALIBRATION_MODE,
+    MEASUREMENT_MODE,
+    CALIBRATION_PASS,
+    CALIBRATION_FAIL,
+    MEASUREMENT_NOT_PROVEN,
+    MEASUREMENT_PRESENT);
+  
+  --  this particular test is testing a syntactic fix for ranges constraint by enum symbols.
+  subtype Result_Indicator_Type is Indicator_Type range CALIBRATION_PASS .. MEASUREMENT_NOT_PROVEN;
+begin
+  null;
+end Range_Constraint;

testsuite/gnat2goto/tests/enum_symbols_range_constraint/test.out

@@ -0,0 +1 @@
+VERIFICATION SUCCESSFUL

testsuite/gnat2goto/tests/enum_symbols_range_constraint/test.py

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

testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/range_constraint.adb

@@ -0,0 +1,16 @@
+procedure Range_Constraint is
+  type Indicator_Type is (
+    CALIBRATION_MODE,
+    MEASUREMENT_MODE,
+    CALIBRATION_PASS,
+    CALIBRATION_FAIL,
+    MEASUREMENT_NOT_PROVEN,
+    MEASUREMENT_PRESENT);
+  
+  subtype Result_Indicator_Type is Indicator_Type range CALIBRATION_PASS .. MEASUREMENT_NOT_PROVEN;
+
+  --  this test is here because subtype assignment is broken and needs to be activated againt when fixed
+  Value : constant Result_Indicator_Type := CALIBRATION_FAIL;
+begin
+  pragma assert (Value = CALIBRATION_FAIL);
+end Range_Constraint;

testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.opt

@@ -0,0 +1 @@
+ALL XFAIL symex is crashing at the assignment because of wrong code generation.

testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.out

@@ -0,0 +1 @@
+VERIFICATION SUCCESSFUL

testsuite/gnat2goto/tests/enum_symbols_range_constraint_assignment/test.py

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

testsuite/gnat2goto/tests/range_second/range_second.adb

@@ -0,0 +1,20 @@
+procedure Range_Second is
+  type Indicator_Type is (
+    CALIBRATION_MODE,
+    MEASUREMENT_MODE,
+    CALIBRATION_PASS,
+    CALIBRATION_FAIL,
+    MEASUREMENT_NOT_PROVEN,
+    MEASUREMENT_PRESENT);
+
+  subtype Result_Indicator_Type is Indicator_Type range CALIBRATION_PASS .. MEASUREMENT_NOT_PROVEN;
+
+  procedure Testable (Result : Result_Indicator_Type) is
+  begin
+    null;
+  end Testable;
+
+begin
+  Testable (CALIBRATION_PASS);
+  Testable (MEASUREMENT_PRESENT);
+end Range_Second;

testsuite/gnat2goto/tests/range_second/range_third.adb

@@ -0,0 +1,14 @@
+procedure Range_Second is
+  type An_Int is range 1..1000;
+  subtype Another_Int is An_Int range 5..100;
+
+  procedure Testable (Result : An_Int) is
+    test_val : Another_Int := Result;
+  begin
+    null;
+  end Testable;
+
+begin
+  Testable (50);
+  Testable (200);
+end Range_Second;

testsuite/gnat2goto/tests/range_second/test.opt

@@ -0,0 +1,2 @@
+ALL XFAIL Doesn't crash anymore but cbmc does not perform range assertion checks 
+

testsuite/gnat2goto/tests/range_second/test.py

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