Skip to content

Support for function bodies #212

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
xbauch merged 14 commits into from
May 31, 2019
Merged

Support for function bodies #212

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
ba12372
Change private type dec test
May 1, 2019
fed142b
Change incomplete dec priv test
May 1, 2019
55f62fa
Use type clause now works
May 1, 2019
1f96189
Split tests that contain two callables
May 1, 2019
d7b5318
Add callable to constant declarations test
May 1, 2019
097c03f
Add callable to deferred const test
May 1, 2019
687c9c8
Add callable to incomplete dec test
May 1, 2019
a275d33
Add callable to private type decl test
May 1, 2019
74bb72c
Rename add_start to unit_is_subprogram
May 1, 2019
05c2419
Do not add cprover_start unless requested
May 1, 2019
93d71b4
User option to skip cprover_start
May 1, 2019
6750f04
Allow linking JSON symtabs in testsuite
petr-bauch May 31, 2019
9b7e70b
Having two subprogram bodies now work
petr-bauch May 31, 2019
c9b7583
Update tests
petr-bauch May 31, 2019
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
28 changes: 11 additions & 17 deletions gnat2goto/driver/driver.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 :=
Expand Down Expand Up @@ -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,
Expand Down Expand Up @@ -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;
Expand Down
1 change: 1 addition & 0 deletions gnat2goto/driver/driver.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand Down
6 changes: 3 additions & 3 deletions gnat2goto/driver/tree_walk.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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);
Expand All @@ -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 =>
Expand Down
2 changes: 1 addition & 1 deletion gnat2goto/driver/tree_walk.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;

Expand Down
55 changes: 33 additions & 22 deletions testsuite/gnat2goto/lib/python/test_support.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand All @@ -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)

Expand All @@ -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
Expand All @@ -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 + ' >>>')
Copy link
Contributor

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue May 2, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Debug output (I'm guessing this'll go away once the draft phase is done)

Copy link
Contributor Author

@xbauch xbauch May 8, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I did not add it, but I can remove it. Done.

print(out)
print('<<< END DEBUG ' + file + ' >>>')
print(filter_cbmc_output(out))
0 testsuite/gnat2goto/tests/abs/absolute.adb → ...ite/gnat2goto/tests/absolute/absolute.adb
View file
Open in desktop
File renamed without changes.
4 changes: 4 additions & 0 deletions testsuite/gnat2goto/tests/absolute/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
0 testsuite/gnat2goto/tests/abs/test.py → testsuite/gnat2goto/tests/absolute/test.py
View file
Open in desktop
File renamed without changes.
0 ...te/gnat2goto/tests/abs/absolute_float.adb → ...o/tests/absolute_float/absolute_float.adb
View file
Open in desktop
File renamed without changes.
4 changes: 0 additions & 4 deletions testsuite/gnat2goto/tests/abs/test.out → ...e/gnat2goto/tests/absolute_float/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
3 changes: 3 additions & 0 deletions testsuite/gnat2goto/tests/absolute_float/test.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
from test_support import *

prove()
6 changes: 3 additions & 3 deletions testsuite/gnat2goto/tests/constant_declarations/const_decs.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;
7 changes: 3 additions & 4 deletions testsuite/gnat2goto/tests/constant_declarations/const_decs.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
9 changes: 9 additions & 0 deletions testsuite/gnat2goto/tests/constant_declarations/test.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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);
Copy link
Contributor

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue May 2, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

With this one I'm confused. Is this supposed to happen or not? Because I'd think after Inc (My_P) My_P would be 5, not 50?

Copy link
Collaborator

@tjj2017 tjj2017 May 3, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Perhaps the name for Inc is inappropriate. The subprogram actually adds a number based on the variable Var in the constant_decs package. Using the value that Var is initialised with, Inc adds 46 to its parameter. I think a more usual scenario that I think we should test is when a private type and deferred constant is used (as in the test below.

Copy link
Contributor Author

@xbauch xbauch May 8, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Renamed to Add_46.

end Test;
3 changes: 2 additions & 1 deletion testsuite/gnat2goto/tests/constant_declarations/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1,2 @@
VERIFICATION SUCCESSFUL
[1] file test.adb line 8 assertion: FAILURE
VERIFICATION FAILED
7 changes: 7 additions & 0 deletions testsuite/gnat2goto/tests/deferred_constant/test.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
with Deferred_Const; use Deferred_Const;
Copy link
Contributor

@hannes-steffenhagen-diffblue hannes-steffenhagen-diffblue May 2, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

?

Copy link
Collaborator

@tjj2017 tjj2017 May 3, 2019 •
edited by hannes-steffenhagen-diffblue
Loading

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I am not sure what this test is checking. Originally I provide a test program called use_deferred_const

with Deferred_Const; use Deferred_Const;
procedure Use_Deferred_Const is
   No_Use : Priv := Def_Const;
begin
   Inc (No_Use);
end Use_Deferred_Const;

If we add another priv constant to the package Deferred_Const as below:

package Deferred_Const is
   type Priv is private;
   
   Def_Const : constant Priv;
   Def_Const_Plus_1 : constant Priv;
   
   procedure Inc (P : in out Priv);
   
private
   type Priv is range 1 .. 10;
   
   Def_Const : constant Priv := 1;
   Def_Const_Plus_1 := Def_Const + 1;
end Deferred_Const;

Then in Use_Deferred_Constant after the call to Inc we could place the
pragma Assert (No_Use = Def_Const_Plus_1);

Which should succeed.

Copy link
Contributor Author

@xbauch xbauch May 8, 2019

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I haven't added the test, I just wanted it to reach symex. This way the the range-check for Def_Const is included in the verification. Even if we don't actually refer to anything from the package.


procedure Test is
My_P : Integer := 4;
begin
pragma Assert (My_P = 4);
end Test;
1 change: 1 addition & 0 deletions testsuite/gnat2goto/tests/deferred_constant/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,2 +1,3 @@
[assertion.1] Range Check: SUCCESS
[1] file test.adb line 6 assertion: SUCCESS
VERIFICATION SUCCESSFUL
4 changes: 2 additions & 2 deletions testsuite/gnat2goto/tests/incomplete_dec/incomplete_dec.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;
6 changes: 3 additions & 3 deletions testsuite/gnat2goto/tests/incomplete_dec/incomplete_dec.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;
Expand Down
8 changes: 8 additions & 0 deletions testsuite/gnat2goto/tests/incomplete_dec/test.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;
1 change: 1 addition & 0 deletions testsuite/gnat2goto/tests/incomplete_dec/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1,2 @@
[1] file test.adb line 7 assertion: SUCCESS
VERIFICATION SUCCESSFUL
7 changes: 7 additions & 0 deletions testsuite/gnat2goto/tests/incomplete_dec_priv/incomplete_dec_priv.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
5 changes: 3 additions & 2 deletions testsuite/gnat2goto/tests/incomplete_dec_priv/incomplete_dec_priv.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
8 changes: 8 additions & 0 deletions testsuite/gnat2goto/tests/incomplete_dec_priv/test.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;
1 change: 1 addition & 0 deletions testsuite/gnat2goto/tests/incomplete_dec_priv/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1,2 @@
[1] file test.adb line 7 assertion: SUCCESS
VERIFICATION SUCCESSFUL
4 changes: 0 additions & 4 deletions testsuite/gnat2goto/tests/op_and/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
0 ...gnat2goto/tests/op_and/op_and_example.adb → ...o/tests/op_and_example/op_and_example.adb
View file
Open in desktop
File renamed without changes.
4 changes: 4 additions & 0 deletions testsuite/gnat2goto/tests/op_and_example/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
3 changes: 3 additions & 0 deletions testsuite/gnat2goto/tests/op_and_example/test.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
from test_support import *

prove()
4 changes: 0 additions & 4 deletions testsuite/gnat2goto/tests/op_or/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
0 ...e/gnat2goto/tests/op_or/op_or_example.adb → ...oto/tests/op_or_example/op_or_example.adb
View file
Open in desktop
File renamed without changes.
4 changes: 4 additions & 0 deletions testsuite/gnat2goto/tests/op_or_example/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
3 changes: 3 additions & 0 deletions testsuite/gnat2goto/tests/op_or_example/test.py
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -0,0 +1,3 @@
from test_support import *

prove()
8 changes: 2 additions & 6 deletions testsuite/gnat2goto/tests/package_use_type_N_Use_Type_Clause/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
7 changes: 7 additions & 0 deletions testsuite/gnat2goto/tests/private_type_dec/private_dec.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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;
3 changes: 2 additions & 1 deletion testsuite/gnat2goto/tests/private_type_dec/private_dec.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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
Expand Down
8 changes: 8 additions & 0 deletions testsuite/gnat2goto/tests/private_type_dec/test.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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;
1 change: 1 addition & 0 deletions testsuite/gnat2goto/tests/private_type_dec/test.out
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1,2 @@
[1] file test.adb line 7 assertion: SUCCESS
VERIFICATION SUCCESSFUL
Loading