Skip to content

Bump CBMC submodule and prettify JSON output #118

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
merged 6 commits into from
Jan 31, 2019
Merged

Bump CBMC submodule and prettify JSON output #118

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
8ba80da
Specify branch for the CBMC submodule
chrisr-diffblue Jan 30, 2019
8f7913f
Bump CBMC submodule
chrisr-diffblue Jan 31, 2019
8e800dc
Generate fully indented JSON output
chrisr-diffblue Jan 30, 2019
b7954f7
Don't output Comment JSON object
chrisr-diffblue Jan 31, 2019
0a27e17
Only output JSON objects/arrays if they are non-empty.
chrisr-diffblue Jan 30, 2019
eeb69f5
Temporarily make string literals have __CPROVER_string type
chrisr-diffblue Jan 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
1 change: 1 addition & 0 deletions .gitmodules
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
[submodule "lib/cbmc"]
path = lib/cbmc
branch = develop
url = https://github.com/diffblue/cbmc.git
4 changes: 2 additions & 2 deletions gnat2goto/driver/driver.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -272,7 +272,7 @@ package body Driver is

Global_Symbol_Table.Insert (Start_Name, Start_Symbol);
Put_Line (Sym_Tab_File,
Create (SymbolTable2Json (Global_Symbol_Table)).Write);
SymbolTable2Json (Global_Symbol_Table).Write (False));
else
Initialize_CProver_Internal_Variables (Start_Body);
declare
Expand Down Expand Up @@ -380,7 +380,7 @@ package body Driver is
Global_Symbol_Table.Insert (Start_Name, Start_Symbol);
Follow_Type_Declarations (Global_Symbol_Table, Followed_Symbol_Table);
Put_Line (Sym_Tab_File,
Create (SymbolTable2Json (Followed_Symbol_Table)).Write);
SymbolTable2Json (Followed_Symbol_Table).Write (False));
end if;

Close (Sym_Tab_File);
Expand Down
36 changes: 19 additions & 17 deletions gnat2goto/driver/tree_walk.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1394,25 +1394,27 @@ package body Tree_Walk is

function Do_String_Constant (N : Node_Id) return Irep is
Ret : constant Irep := New_Irep (I_String_Constant_Expr);
Element_Type_Ent : constant Entity_Id := Get_Array_Component_Type (N);
Element_Type : constant Irep := Do_Type_Reference (Element_Type_Ent);
-- Element_Type_Ent : constant Entity_Id := Get_Array_Component_Type (N);
-- Element_Type : constant Irep := Do_Type_Reference (Element_Type_Ent);
StrLen : constant Integer :=
Integer (String_Length (Strval (N)));
String_Length_Expr : constant Irep := New_Irep (I_Constant_Expr);
Integer (String_Length (Strval (N)));
-- String_Length_Expr : constant Irep := New_Irep (I_Constant_Expr);
begin
-- FIXME: The size of this signedbv should probably not be a hardcoded
-- magic number...(e.g. 32 on a 32bit system) this should be set
-- programatically some how.
Set_Type (String_Length_Expr,
Make_Signedbv_Type (Ireps.Empty, 64));
Set_Value (String_Length_Expr,
Convert_Uint_To_Hex (UI_From_Int (Int (String_Length
(Strval (N)))), 64));

Set_Type (Ret,
Make_Array_Type (
I_Subtype => Element_Type,
Size => String_Length_Expr));
-- FIXME: Need to set a proper type, something like this:
-- Set_Type (String_Length_Expr,
-- Make_Signedbv_Type (Ireps.Empty, 64));
-- Set_Value (String_Length_Expr,
-- Convert_Uint_To_Hex (UI_From_Int (Int (String_Length
-- (Strval (N)))), 64));

Set_Type (Ret, Make_String_Type);
-- FIXME: We really need some sort of array type here, such as:
-- Make_Array_Type (
-- I_Subtype => Element_Type,
-- Size => String_Length_Expr));
String_To_Name_Buffer (Strval (N));
Set_Value (Ret, Name_Buffer (1 .. StrLen));
Set_Source_Location (Ret, Sloc (N));
Expand Down Expand Up @@ -1554,7 +1556,7 @@ package body Tree_Walk is
begin
Set_Value (Element, Val_String);
Set_Identifier (Element, Val_Name);
Set_Base_Name (Element, Base_Name);
Set_Basename (Element, Base_Name);
Append_Member (Enum_Body, Element);
Member_Symbol.Name := Intern (Val_Name);
Member_Symbol.PrettyName := Intern (Base_Name);
Expand Down Expand Up @@ -4963,8 +4965,8 @@ package body Tree_Walk is
Set_Anonymous (Ret, False);
-- Real attributes:
Set_Name (Ret, Name);
Set_Pretty_Name (Ret, Name);
Set_Base_Name (Ret, Name);
Set_Prettyname (Ret, Name);
Set_Basename (Ret, Name);
Set_Type (Ret, Ty);
return Ret;
end Make_Struct_Component;
Expand Down
2 changes: 1 addition & 1 deletion gnat2goto/ireps/irep_specs/c_enum_member.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,6 @@
"namedSub": {
"value": {"type": "string"},
"identifier": {"type": "string"},
"base_name": {"type": "string"}
"baseName": {"type": "string"}
}
}
4 changes: 2 additions & 2 deletions gnat2goto/ireps/irep_specs/struct_union_component.json
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,9 +2,9 @@
"parent": "expr",
"namedSub": {
"name": {"type": "string"},
"base_name": {"type": "string"},
"baseName": {"type": "string"},
"access": {"type": "string"},
"pretty_name": {"type": "string"},
"prettyName": {"type": "string"},
"anonymous": {"type": "bool"}
},
"comment": {
Expand Down
21 changes: 10 additions & 11 deletions gnat2goto/ireps/ireps_generator.py
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -380,7 +380,6 @@ def to_json_set_all_namedsubs_and_comments(self, b, sn, setter_name, needs_null)
tbl_field = "N." + ada_component_name(layout_kind,
layout_index)

obj = "Comment" if is_comment else "Named_Sub"
if kind == "irep":
val = "To_JSON (Irep (%s))" % tbl_field
elif layout_kind == "str":
Expand All @@ -399,7 +398,7 @@ def to_json_set_all_namedsubs_and_comments(self, b, sn, setter_name, needs_null)
else:
key_name = setter_name

tmp = "%s.Set_Field (" % obj
tmp = "Named_Sub.Set_Field ("
write(b, tmp + '"' + key_name + '",')
write(b, " " * len(tmp) + val + ");")
continuation(b)
Expand All @@ -418,7 +417,6 @@ def follow_irep_set_all_namedsubs_and_comments(self, b, sn, setter_name, needs_n
layout_index)
tbl_field = "N." + tbl_index

obj = "Comment" if is_comment else "Named_Sub"
if kind == "irep":
write(b, "Irep_Table.Table (I).%s :=" % tbl_index)
with indent(b):
Expand All @@ -429,10 +427,8 @@ def follow_irep_set_all_namedsubs_and_comments(self, b, sn, setter_name, needs_n
def to_json_set_all_constants(self, b, sn, kind, data, needs_null):
if kind == "id":
return needs_null
elif kind == "namedSub":
elif kind == "namedSub" or kind == "comment":
obj = "Named_Sub"
elif kind == "comment":
obj = "Comment"
else:
print sn, kind, self.const[sn]
assert False
Expand Down Expand Up @@ -1831,7 +1827,6 @@ def generate_code(self, optimize, schema_file_names):
write(b, 'V.Set_Field ("id", S);')
write(b, 'V.Set_Field ("sub", Empty_Array);')
write(b, 'V.Set_Field ("namedSub", Create_Object);')
write(b, 'V.Set_Field ("comment", Create_Object);')
write(b, "end return;")
write(b, "end Trivial_Irep;")
write(b, "")
Expand Down Expand Up @@ -1902,7 +1897,6 @@ def generate_code(self, optimize, schema_file_names):
write(b, "")
write(b, "Sub : JSON_Array := Empty_Array;")
write(b, "Named_Sub : constant JSON_Value := Create_Object;")
write(b, "Comment : constant JSON_Value := Create_Object;")
write(b, "begin")
manual_indent(b)
write(b, 'V.Set_Field ("id", Id (I));')
Expand All @@ -1916,9 +1910,14 @@ def generate_code(self, optimize, schema_file_names):
self.to_json_single_schema_name(b, sn)
write(b, "end case;")
write(b, "")
write(b, 'V.Set_Field ("sub", Sub);')
write(b, 'V.Set_Field ("namedSub", Named_Sub);')
write(b, 'V.Set_Field ("comment", Comment);')
write(b, "if not Is_Empty (Sub) then")
with indent(b):
write(b, 'V.Set_Field ("sub", Sub);')
write(b, "end if;")
write(b, "if not Is_Empty (Named_Sub) then")
with indent(b):
write(b, 'V.Set_Field ("namedSub", Named_Sub);')
write(b, "end if;")
manual_outdent(b)
write(b, "end;")
write(b, "return V;")
Expand Down
44 changes: 23 additions & 21 deletions gnat2goto/ireps/symbol_table_info.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,36 +17,38 @@ package body Symbol_Table_Info is
Ret.Set_Field ("location", To_JSON (Sym.Location));
Ret.Set_Field ("name", Unintern (Sym.Name));
Ret.Set_Field ("module", Unintern (Sym.Module));
Ret.Set_Field ("base_name", Unintern (Sym.BaseName));
Ret.Set_Field ("baseName", Unintern (Sym.BaseName));
Ret.Set_Field ("mode", Unintern (Sym.Mode));
Ret.Set_Field ("pretty_name", Unintern (Sym.PrettyName));
Ret.Set_Field ("is_type", Sym.IsType);
Ret.Set_Field ("is_macro", Sym.IsMacro);
Ret.Set_Field ("is_exported", Sym.IsExported);
Ret.Set_Field ("is_input", Sym.IsInput);
Ret.Set_Field ("is_output", Sym.IsOutput);
Ret.Set_Field ("is_state_var", Sym.IsStateVar);
Ret.Set_Field ("is_property", Sym.IsProperty);
Ret.Set_Field ("is_static_lifetime", Sym.IsStaticLifetime);
Ret.Set_Field ("is_thread_local", Sym.IsThreadLocal);
Ret.Set_Field ("is_lvalue", Sym.IsLValue);
Ret.Set_Field ("is_file_local", Sym.IsFileLocal);
Ret.Set_Field ("is_extern", Sym.IsExtern);
Ret.Set_Field ("is_volatile", Sym.IsVolatile);
Ret.Set_Field ("is_parameter", Sym.IsParameter);
Ret.Set_Field ("is_auxiliary", Sym.IsAuxiliary);
Ret.Set_Field ("is_weak", Sym.IsWeak);
Ret.Set_Field ("prettyName", Unintern (Sym.PrettyName));
Ret.Set_Field ("isType", Sym.IsType);
Ret.Set_Field ("isMacro", Sym.IsMacro);
Ret.Set_Field ("isExported", Sym.IsExported);
Ret.Set_Field ("isInput", Sym.IsInput);
Ret.Set_Field ("isOutput", Sym.IsOutput);
Ret.Set_Field ("isStateVar", Sym.IsStateVar);
Ret.Set_Field ("isProperty", Sym.IsProperty);
Ret.Set_Field ("isStaticLifetime", Sym.IsStaticLifetime);
Ret.Set_Field ("isThreadLocal", Sym.IsThreadLocal);
Ret.Set_Field ("isLvalue", Sym.IsLValue);
Ret.Set_Field ("isFileLocal", Sym.IsFileLocal);
Ret.Set_Field ("isExtern", Sym.IsExtern);
Ret.Set_Field ("isVolatile", Sym.IsVolatile);
Ret.Set_Field ("isParameter", Sym.IsParameter);
Ret.Set_Field ("isAuxiliary", Sym.IsAuxiliary);
Ret.Set_Field ("isWeak", Sym.IsWeak);
return Ret;
end Symbol2Json;

function SymbolTable2Json (Symtab : Symbol_Table) return JSON_Array is
Ret : JSON_Array := Empty_Array;
function SymbolTable2Json (Symtab : Symbol_Table) return JSON_Value is
Ret : constant JSON_Value := Create_Object;
Symbol_Table_Json : constant JSON_Value := Create_Object;
Symbol_Json : JSON_Value;
begin
for Symbol of Symtab loop
Symbol_Json := Symbol2Json (Symbol);
Append (Ret, Symbol_Json);
Symbol_Table_Json.Set_Field (Unintern (Symbol.Name), Symbol_Json);
end loop;
Ret.Set_Field ("symbolTable", Symbol_Table_Json);
return Ret;
end SymbolTable2Json;

Expand Down
2 changes: 1 addition & 1 deletion gnat2goto/ireps/symbol_table_info.ads
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -69,6 +69,6 @@ package Symbol_Table_Info is

subtype Symbol_Table is Symbol_Maps.Map;

function SymbolTable2Json (Symtab : Symbol_Table) return JSON_Array;
function SymbolTable2Json (Symtab : Symbol_Table) return JSON_Value;

end Symbol_Table_Info;
36 changes: 18 additions & 18 deletions irep_utils/src/symbol_table_info.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,25 +8,25 @@ package body Symbol_Table_Info is
Ret.Set_Field ("location", Iinfo.Irep_To_Json (Sym.Location));
Ret.Set_Field ("name", To_String (Sym.Name));
Ret.Set_Field ("module", To_String (Sym.Module));
Ret.Set_Field ("base_name", To_String (Sym.BaseName));
Ret.Set_Field ("baseName", To_String (Sym.BaseName));
Ret.Set_Field ("mode", To_String (Sym.Mode));
Ret.Set_Field ("pretty_name", To_String (Sym.PrettyName));
Ret.Set_Field ("is_type", Sym.IsType);
Ret.Set_Field ("is_macro", Sym.IsMacro);
Ret.Set_Field ("is_exported", Sym.IsExported);
Ret.Set_Field ("is_input", Sym.IsInput);
Ret.Set_Field ("is_output", Sym.IsOutput);
Ret.Set_Field ("is_state_var", Sym.IsStateVar);
Ret.Set_Field ("is_property", Sym.IsProperty);
Ret.Set_Field ("is_static_lifetime", Sym.IsStaticLifetime);
Ret.Set_Field ("is_thread_local", Sym.IsThreadLocal);
Ret.Set_Field ("is_lvalue", Sym.IsLValue);
Ret.Set_Field ("is_file_local", Sym.IsFileLocal);
Ret.Set_Field ("is_extern", Sym.IsExtern);
Ret.Set_Field ("is_volatile", Sym.IsVolatile);
Ret.Set_Field ("is_parameter", Sym.IsParameter);
Ret.Set_Field ("is_auxiliary", Sym.IsAuxiliary);
Ret.Set_Field ("is_weak", Sym.IsWeak);
Ret.Set_Field ("prettyName", To_String (Sym.PrettyName));
Ret.Set_Field ("isType", Sym.IsType);
Ret.Set_Field ("isMacro", Sym.IsMacro);
Ret.Set_Field ("isExported", Sym.IsExported);
Ret.Set_Field ("isInput", Sym.IsInput);
Ret.Set_Field ("isOutput", Sym.IsOutput);
Ret.Set_Field ("isStateVar", Sym.IsStateVar);
Ret.Set_Field ("isProperty", Sym.IsProperty);
Ret.Set_Field ("isStaticLifetime", Sym.IsStaticLifetime);
Ret.Set_Field ("isThreadLocal", Sym.IsThreadLocal);
Ret.Set_Field ("isLvalue", Sym.IsLValue);
Ret.Set_Field ("isFileLocal", Sym.IsFileLocal);
Ret.Set_Field ("isExtern", Sym.IsExtern);
Ret.Set_Field ("isVolatile", Sym.IsVolatile);
Ret.Set_Field ("isParameter", Sym.IsParameter);
Ret.Set_Field ("isAuxiliary", Sym.IsAuxiliary);
Ret.Set_Field ("isWeak", Sym.IsWeak);
return Ret;
end;

Expand Down
2 changes: 1 addition & 1 deletion lib/cbmc
Open in desktop
Submodule cbmc updated 1227 files
5 changes: 4 additions & 1 deletion testsuite/gnat2goto/tests/string_literal/string_literal.adb
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,5 +1,8 @@
procedure string_literal is
A : constant String := "Hello";
B : constant String := "Hello";
C : constant String := "Goodbye";
begin
null;
pragma Assert(A = B);
pragma Assert(A /= C);
end string_literal;