Merge pull request #212 from xbauch/feature/function-bodies

petr-bauch · web-flow · commit bd18b024cbc9 · 2019-05-31T20:56:23.000+01:00
Support for function bodies
diff --git a/gnat2goto/driver/driver.adb b/gnat2goto/driver/driver.adb
@@ -366,9 +366,14 @@ package body Driver is
       Initial_Call      : constant Irep := New_Irep (I_Code_Function_Call);
       Initial_Call_Args : constant Irep := New_Irep (I_Argument_List);
 
-      Add_Start : Boolean;
-      Program_Symbol : constant Symbol := Do_Compilation_Unit (GNAT_Root,
-                                                               Add_Start);
+      Unit_Is_Subprogram : Boolean;
+      Program_Symbol : constant Symbol :=
+        Do_Compilation_Unit (GNAT_Root, Unit_Is_Subprogram);
+
+      --  Only add CPROVER_Start if the unit is subprogram and the user did not
+      --  suppress it (by cmdl option).
+      Add_Start : constant Boolean :=
+        Unit_Is_Subprogram and not Suppress_Cprover_Start;
 
       Sym_Tab_File : File_Type;
       Base_Name  : constant String :=
@@ -404,20 +409,6 @@ package body Driver is
       end;
 
       if not Add_Start then
-         --  If the compilation unit is not a subprogram body then there is
-         --  no function/procedure to call
-         --  CBMC does not like that so we add cprover_start with empty body
-         Start_Symbol.Name       := Start_Name;
-         Start_Symbol.PrettyName := Start_Name;
-         Start_Symbol.BaseName   := Start_Name;
-
-         Set_Return_Type (Start_Type, Void_Type);
-
-         Start_Symbol.SymType := Start_Type;
-         Start_Symbol.Value   := Start_Body;
-         Start_Symbol.Mode    := Intern ("C");
-
-         Global_Symbol_Table.Insert (Start_Name, Start_Symbol);
          Sanitise_Type_Declarations (Global_Symbol_Table,
                                      Sanitised_Symbol_Table);
          Put_Line (Sym_Tab_File,
@@ -553,6 +544,9 @@ package body Driver is
          then
             Dump_Statement_AST_On_Error := True;
             return True;
+         elsif Switch (First .. Last) = "-no-cprover-start" then
+            Suppress_Cprover_Start := True;
+            return True;
          end if;
       end if;
       return False;
diff --git a/gnat2goto/driver/driver.ads b/gnat2goto/driver/driver.ads
@@ -24,6 +24,7 @@
 with Types; use Types;
 
 package Driver is
+   Suppress_Cprover_Start : Boolean := False;
 
    procedure GNAT_To_Goto (GNAT_Root : Node_Id);
    procedure Translate_Compilation_Unit (GNAT_Root : Node_Id);
diff --git a/gnat2goto/driver/tree_walk.adb b/gnat2goto/driver/tree_walk.adb
@@ -991,7 +991,7 @@ package body Tree_Walk is
    -- Do_Compilation_Unit --
    -------------------------
 
-   function Do_Compilation_Unit (N : Node_Id; Add_Start : out Boolean)
+   function Do_Compilation_Unit (N : Node_Id; Unit_Is_Subprogram : out Boolean)
      return Symbol
    is
       U           : constant Node_Id := Unit (N);
@@ -1018,15 +1018,15 @@ package body Tree_Walk is
 
                --  and update the symbol table entry for this subprogram.
                Global_Symbol_Table.Replace (Unit_Name, Unit_Symbol);
-               Add_Start := True;
+               Unit_Is_Subprogram := True;
             end;
 
          when N_Package_Body =>
             declare
                Dummy : constant Irep := Do_Subprogram_Or_Block (U);
                pragma Unreferenced (Dummy);
             begin
-               Add_Start := False;
+               Unit_Is_Subprogram := False;
             end;
 
          when others =>
diff --git a/gnat2goto/driver/tree_walk.ads b/gnat2goto/driver/tree_walk.ads
@@ -75,7 +75,7 @@ package Tree_Walk is
 
    Check_Function_Symbol : Irep := Ireps.Empty;
 
-   function Do_Compilation_Unit (N : Node_Id; Add_Start : out Boolean)
+   function Do_Compilation_Unit (N : Node_Id; Unit_Is_Subprogram : out Boolean)
                                  return Symbol
      with Pre => Nkind (N) = N_Compilation_Unit;
 
diff --git a/testsuite/gnat2goto/lib/python/test_support.py b/testsuite/gnat2goto/lib/python/test_support.py
@@ -29,21 +29,18 @@ def filter_timing(results):
 
     return re.sub(skip, r'', results)
 
-
-def process(debug, file, cbmcargs):
+def process_gnat2goto(debug, file, is_main):
     """Process Ada file with gnat2goto and cbmc"""
     unit = os.path.splitext(file)[0]
     jsout    = unit + ".json_symtab"
-    symtab   = unit + ".symtab"
-    gotoprog = unit + ".goto_functions"
-    out      = unit + ".out"
     errout   = unit + ".error"
     stdoutp  = unit + "stdoutp"
-    cbmcerr  = unit + "cbmc_error"
+    gnat2gotoargs = []
+    if not is_main: gnat2gotoargs.append("--no-cprover-start")
 
-    cmd = ["gnat2goto", file]
+    cmd = ["gnat2goto", file] + gnat2gotoargs
 
-    g2go_results = Run(["gnat2goto", file], output=stdoutp, error=errout)
+    g2go_results = Run(cmd, output=stdoutp, error=errout)
 
     stdout_file = open (stdoutp)
     errout_file = open (errout)
@@ -60,12 +57,22 @@ def process(debug, file, cbmcargs):
     if g2go_results.status != 0:
         print "ERROR code ", g2go_results.status, " returned by gnat2goto when translating " + unit
         print "CBMC not run"
-        return ""
+        return False
+
+    return True
+
+# only run the following if gnat2goto succeeded
+def process_cbmc(debug, files, cbmcargs):
+    """Process Ada file with gnat2goto and cbmc"""
+    jsout = []
+    for file in files:
+        unit          = os.path.splitext(file)[0]
+        file_jsout    = unit + ".json_symtab"
+        jsout.append(file_jsout)
+
+    cbmcerr = TEST_NAME + "cbmc_error"
 
-    # only run the following if gnat2goto succeeded
-    # Run(["cbmc", jsout, "--show-symbol-table"], output=symtab)
-    # Run(["cbmc", jsout, "--show-goto-functions"], output=gotoprog)
-    cmdline = ["cbmc", jsout]
+    cmdline = ["cbmc"] + jsout
     if cbmcargs: cmdline += cbmcargs.split(" ")
     results = Run(cmdline, error=cbmcerr)
 
@@ -80,7 +87,6 @@ def process(debug, file, cbmcargs):
 
     return filter_timing(results.out)
 
-
 def cbmc_match(line):
     return ('FAILURE' in line or
            'SUCCESS' in line or
@@ -91,16 +97,21 @@ def filter_cbmc_output(cbmc_output):
     lines = cbmc_output.split("\n")
     return "\n".join(filter(cbmc_match, lines))
 
-def prove(cbmcargs="", debug=False):
+def prove(cbmcargs="", main="", debug=False):
     """Call gnat2goto (and cbmc) on all *.adb files from the current directory
 
     PARAMETERS
-      none: yet
+      cbmcargs: arguments to be passed to CBMC
+      main: name of the file containing the entry point
+      debug: flag indicating if debug output should be printed out
     """
     for file in ada_body_files():
-        out = process(debug, file, cbmcargs)
-        if debug:
-            print('<<< DEBUG ' + file + ' >>>')
-            print(out)
-            print('<<< END DEBUG ' + file + ' >>>')
-        print(filter_cbmc_output(out))
+        gnat2goto_success = process_gnat2goto(debug, file, main == "" or file == main)
+        if not gnat2goto_success:
+            return ""
+    out = process_cbmc(debug, ada_body_files(), cbmcargs)
+    if debug:
+        print('<<< DEBUG ' + file + ' >>>')
+        print(out)
+        print('<<< END DEBUG ' + file + ' >>>')
+    print(filter_cbmc_output(out))
diff --git a/testsuite/gnat2goto/tests/absolute/absolute.adb b/testsuite/gnat2goto/tests/absolute/absolute.adb
diff --git a/testsuite/gnat2goto/tests/absolute/test.out b/testsuite/gnat2goto/tests/absolute/test.out
@@ -0,0 +1,4 @@
+[1] file absolute.adb line 7 assertion: SUCCESS
+[2] file absolute.adb line 8 assertion: SUCCESS
+[3] file absolute.adb line 10 assertion: FAILURE
+VERIFICATION FAILED
diff --git a/testsuite/gnat2goto/tests/absolute/test.py b/testsuite/gnat2goto/tests/absolute/test.py
diff --git a/testsuite/gnat2goto/tests/absolute_float/absolute_float.adb b/testsuite/gnat2goto/tests/absolute_float/absolute_float.adb
diff --git a/testsuite/gnat2goto/tests/absolute_float/test.out b/testsuite/gnat2goto/tests/absolute_float/test.out
@@ -1,7 +1,3 @@
-[1] file absolute.adb line 7 assertion: SUCCESS
-[2] file absolute.adb line 8 assertion: SUCCESS
-[3] file absolute.adb line 10 assertion: FAILURE
-VERIFICATION FAILED
 [1] file absolute_float.adb line 7 assertion: SUCCESS
 [2] file absolute_float.adb line 8 assertion: SUCCESS
 [3] file absolute_float.adb line 10 assertion: FAILURE
diff --git a/testsuite/gnat2goto/tests/absolute_float/test.py b/testsuite/gnat2goto/tests/absolute_float/test.py
@@ -0,0 +1,3 @@
+from test_support import *
+
+prove()
diff --git a/testsuite/gnat2goto/tests/constant_declarations/const_decs.adb b/testsuite/gnat2goto/tests/constant_declarations/const_decs.adb
@@ -1,7 +1,7 @@
 package body Const_Decs is
-   procedure Inc (P : in out Integer) is
+   procedure Add_46 (P : in out Integer) is
    begin
       P := P + Read_Only_Var;
-   end Inc;
-   
+   end Add_46;
+
 end Const_Decs;
diff --git a/testsuite/gnat2goto/tests/constant_declarations/const_decs.ads b/testsuite/gnat2goto/tests/constant_declarations/const_decs.ads
@@ -6,8 +6,7 @@ package Const_Decs is
    SC1 : constant Integer := Static_Const + 1;
    
    Read_Only_Var : constant Integer := SC1 + Var;
-   
-   procedure Inc (P : in out Integer);
-   
-end Const_Decs;
 
+   procedure Add_46 (P : in out Integer);
+
+end Const_Decs;
diff --git a/testsuite/gnat2goto/tests/constant_declarations/test.adb b/testsuite/gnat2goto/tests/constant_declarations/test.adb
@@ -0,0 +1,9 @@
+with Const_Decs; use Const_Decs;
+
+procedure Test is
+   My_P : Integer := 4;
+begin
+   Add_46 (My_P);
+   --  Will fail: symex does not see the value
+   pragma Assert (My_P = 50);
+end Test;
diff --git a/testsuite/gnat2goto/tests/constant_declarations/test.out b/testsuite/gnat2goto/tests/constant_declarations/test.out
@@ -1 +1,2 @@
-VERIFICATION SUCCESSFUL
+[1] file test.adb line 8 assertion: FAILURE
+VERIFICATION FAILED
diff --git a/testsuite/gnat2goto/tests/deferred_constant/test.adb b/testsuite/gnat2goto/tests/deferred_constant/test.adb
@@ -0,0 +1,7 @@
+with Deferred_Const; use Deferred_Const;
+
+procedure Test is
+   My_P : Integer := 4;
+begin
+   pragma Assert (My_P = 4);
+end Test;
diff --git a/testsuite/gnat2goto/tests/deferred_constant/test.out b/testsuite/gnat2goto/tests/deferred_constant/test.out
@@ -1,2 +1,3 @@
 [assertion.1] Range Check: SUCCESS
+[1] file test.adb line 6 assertion: SUCCESS
 VERIFICATION SUCCESSFUL
diff --git a/testsuite/gnat2goto/tests/incomplete_dec/incomplete_dec.adb b/testsuite/gnat2goto/tests/incomplete_dec/incomplete_dec.adb
@@ -1,6 +1,6 @@
 package body Incomplete_Dec is
-   procedure P (X : in out Partial_Dec) is
+   procedure Inc (X : in out Partial_Dec) is
    begin
       X.A := X.A + 1;
-   end P;
+   end Inc;
 end Incomplete_Dec;
diff --git a/testsuite/gnat2goto/tests/incomplete_dec/incomplete_dec.ads b/testsuite/gnat2goto/tests/incomplete_dec/incomplete_dec.ads
@@ -1,8 +1,8 @@
 package Incomplete_Dec is
    type Partial_Dec;
-   
-   procedure P (X : in out Partial_Dec);
-   
+
+   procedure Inc (X : in out Partial_Dec);
+
    type Partial_Dec is record
       A : Integer;
    end record;
diff --git a/testsuite/gnat2goto/tests/incomplete_dec/test.adb b/testsuite/gnat2goto/tests/incomplete_dec/test.adb
@@ -0,0 +1,8 @@
+with Incomplete_Dec; use Incomplete_Dec;
+
+procedure Test is
+   My_Rec : Partial_Dec := (A=>1);
+begin
+   Inc (My_Rec);
+   pragma Assert (My_Rec.A = 2);
+end Test;
diff --git a/testsuite/gnat2goto/tests/incomplete_dec/test.out b/testsuite/gnat2goto/tests/incomplete_dec/test.out
@@ -1 +1,2 @@
+[1] file test.adb line 7 assertion: SUCCESS
 VERIFICATION SUCCESSFUL
diff --git a/testsuite/gnat2goto/tests/incomplete_dec_priv/incomplete_dec_priv.adb b/testsuite/gnat2goto/tests/incomplete_dec_priv/incomplete_dec_priv.adb
@@ -3,4 +3,11 @@ package body Incomplete_Dec_Priv is
    begin
       X.A := X.A + 1;
    end P;
+   procedure Q (X : in out Integer) is
+      X_Rec : Incomplete_Dec;
+   begin
+      X_Rec.A := X;
+      P(X_Rec);
+      X := X_Rec.A;
+   end Q;
 end Incomplete_Dec_Priv;
diff --git a/testsuite/gnat2goto/tests/incomplete_dec_priv/incomplete_dec_priv.ads b/testsuite/gnat2goto/tests/incomplete_dec_priv/incomplete_dec_priv.ads
@@ -1,8 +1,9 @@
 package Incomplete_Dec_Priv is
    type Incomplete_Dec;
-   
+
    procedure P (X : in out Incomplete_Dec);
-   
+   procedure Q (X : in out Integer);
+
    type Incomplete_Dec is private;
 private
    type Incomplete_Dec is record
diff --git a/testsuite/gnat2goto/tests/incomplete_dec_priv/test.adb b/testsuite/gnat2goto/tests/incomplete_dec_priv/test.adb
@@ -0,0 +1,8 @@
+with Incomplete_Dec_Priv; use Incomplete_Dec_Priv;
+
+procedure Test is
+   My_Int : Integer := 4;
+begin
+   Q(My_Int);
+   pragma Assert (My_Int = 5);
+end Test;
diff --git a/testsuite/gnat2goto/tests/incomplete_dec_priv/test.out b/testsuite/gnat2goto/tests/incomplete_dec_priv/test.out
@@ -1 +1,2 @@
+[1] file test.adb line 7 assertion: SUCCESS
 VERIFICATION SUCCESSFUL
diff --git a/testsuite/gnat2goto/tests/op_and/test.out b/testsuite/gnat2goto/tests/op_and/test.out
@@ -4,7 +4,3 @@
 [4] file op_and.adb line 13 assertion: FAILURE
 [5] file op_and.adb line 15 assertion: FAILURE
 VERIFICATION FAILED
-[1] file op_and_example.adb line 11 assertion: SUCCESS
-[2] file op_and_example.adb line 15 assertion: SUCCESS
-[3] file op_and_example.adb line 16 assertion: FAILURE
-VERIFICATION FAILED
diff --git a/testsuite/gnat2goto/tests/op_and_example/op_and_example.adb b/testsuite/gnat2goto/tests/op_and_example/op_and_example.adb
diff --git a/testsuite/gnat2goto/tests/op_and_example/test.out b/testsuite/gnat2goto/tests/op_and_example/test.out
@@ -0,0 +1,4 @@
+[1] file op_and_example.adb line 11 assertion: SUCCESS
+[2] file op_and_example.adb line 15 assertion: SUCCESS
+[3] file op_and_example.adb line 16 assertion: FAILURE
+VERIFICATION FAILED
diff --git a/testsuite/gnat2goto/tests/op_and_example/test.py b/testsuite/gnat2goto/tests/op_and_example/test.py
@@ -0,0 +1,3 @@
+from test_support import *
+
+prove()
diff --git a/testsuite/gnat2goto/tests/op_or/test.out b/testsuite/gnat2goto/tests/op_or/test.out
@@ -4,7 +4,3 @@
 [4] file op_or.adb line 9 assertion: FAILURE
 [5] file op_or.adb line 10 assertion: SUCCESS
 VERIFICATION FAILED
-[1] file op_or_example.adb line 11 assertion: SUCCESS
-[2] file op_or_example.adb line 15 assertion: SUCCESS
-[3] file op_or_example.adb line 16 assertion: FAILURE
-VERIFICATION FAILED
diff --git a/testsuite/gnat2goto/tests/op_or_example/op_or_example.adb b/testsuite/gnat2goto/tests/op_or_example/op_or_example.adb
diff --git a/testsuite/gnat2goto/tests/op_or_example/test.out b/testsuite/gnat2goto/tests/op_or_example/test.out
@@ -0,0 +1,4 @@
+[1] file op_or_example.adb line 11 assertion: SUCCESS
+[2] file op_or_example.adb line 15 assertion: SUCCESS
+[3] file op_or_example.adb line 16 assertion: FAILURE
+VERIFICATION FAILED
diff --git a/testsuite/gnat2goto/tests/op_or_example/test.py b/testsuite/gnat2goto/tests/op_or_example/test.py
@@ -0,0 +1,3 @@
+from test_support import *
+
+prove()
diff --git a/testsuite/gnat2goto/tests/package_use_type_N_Use_Type_Clause/test.out b/testsuite/gnat2goto/tests/package_use_type_N_Use_Type_Clause/test.out
@@ -1,7 +1,3 @@
-VERIFICATION SUCCESSFUL
-Error from cbmc use_type_clause:
-**** WARNING: no body for function count_types__double
-
 [1] file use_type_clause.adb line 21 assertion: SUCCESS
-[2] file use_type_clause.adb line 24 assertion: FAILURE
-VERIFICATION FAILED
+[2] file use_type_clause.adb line 24 assertion: SUCCESS
+VERIFICATION SUCCESSFUL
diff --git a/testsuite/gnat2goto/tests/private_type_dec/private_dec.adb b/testsuite/gnat2goto/tests/private_type_dec/private_dec.adb
@@ -3,4 +3,11 @@ package body Private_Dec is
    begin
       X.A := X.A + 1;
    end P;
+   procedure Q (X : in out Integer) is
+      X_Dec : Dec;
+   begin
+      X_Dec.A := X;
+      P(X_Dec);
+      X := X_Dec.A;
+   end Q;
 end Private_Dec;
diff --git a/testsuite/gnat2goto/tests/private_type_dec/private_dec.ads b/testsuite/gnat2goto/tests/private_type_dec/private_dec.ads
@@ -1,7 +1,8 @@
 package Private_Dec is
    type Dec is private;
-   
+
    procedure P (X : in out Dec);
+   procedure Q (X : in out Integer);
 
 private
    type Dec is record
diff --git a/testsuite/gnat2goto/tests/private_type_dec/test.adb b/testsuite/gnat2goto/tests/private_type_dec/test.adb
@@ -0,0 +1,8 @@
+with Private_Dec; use Private_Dec;
+
+procedure Test is
+   My_Int : Integer := 4;
+begin
+   Q(My_Int);
+   pragma Assert (My_Int = 5);
+end Test;
diff --git a/testsuite/gnat2goto/tests/private_type_dec/test.out b/testsuite/gnat2goto/tests/private_type_dec/test.out
@@ -1 +1,2 @@
+[1] file test.adb line 7 assertion: SUCCESS
 VERIFICATION SUCCESSFUL
diff --git a/testsuite/gnat2goto/tests/private_type_dec_array/test.adb b/testsuite/gnat2goto/tests/private_type_dec_array/test.adb
diff --git a/testsuite/gnat2goto/tests/private_type_dec_array/test.py b/testsuite/gnat2goto/tests/private_type_dec_array/test.py
diff --git a/testsuite/gnat2goto/tests/private_type_decl/test.adb b/testsuite/gnat2goto/tests/private_type_decl/test.adb
diff --git a/testsuite/gnat2goto/tests/two_subprog_bodies/test.opt b/testsuite/gnat2goto/tests/two_subprog_bodies/test.opt
diff --git a/testsuite/gnat2goto/tests/two_subprog_bodies/test.out b/testsuite/gnat2goto/tests/two_subprog_bodies/test.out
diff --git a/testsuite/gnat2goto/tests/two_subprog_bodies/test.py b/testsuite/gnat2goto/tests/two_subprog_bodies/test.py
diff --git a/testsuite/gnat2goto/tests/two_subprog_bodies/two.adb b/testsuite/gnat2goto/tests/two_subprog_bodies/two.adb
