Skip to content

Fix language-specific printing of constants in JSON output #1198

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.

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
Show file tree
Hide file tree
Changes from all commits
Commits
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
Binary file added regression/cbmc-java/json_trace2/Test.class
Binary file not shown.
7 changes: 7 additions & 0 deletions regression/cbmc-java/json_trace2/Test.java
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
public class Test {
boolean test(Object x) {
if(x==null)
return false;
return true;
}
}
10 changes: 10 additions & 0 deletions regression/cbmc-java/json_trace2/test.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
Test.class
--cover location --trace --json-ui --function Test.test
activate-multi-line-match
EXIT=0
SIGNAL=0
"outputID": "return",\n *"sourceLocation": \{\n *"file": "Test\.java",\n *"function": "java::Test\.test:\(Ljava/lang/Object;\)Z",\n *"line": "3"\n *\},\n *"stepType": "output",\n *"thread": 0,\n *"values": \[\n *\{\n *"binary": "00000000",\n *"data": "false",\n *"name": "integer",\n *"type": "boolean",\n *"width": 8
"inputID": "arg1a",\n *"internal": true,\n *"mode": "java",\n *"sourceLocation": \{\n *"file": "Test\.java",\n *"function": "java::Test\.test:\(Ljava/lang/Object;\)Z",\n *"line": "3"\n *\},\n *"stepType": "input",\n *"thread": 0,\n *"values": \[\n *\{\n *"data": "null",\n *"name": "pointer",\n *"type": "struct java\.lang\.Object \{ __CPROVER_string @class_identifier; boolean @lock; \} \*"
--
^warning: ignoring
23 changes: 18 additions & 5 deletions src/goto-programs/json_goto_trace.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -13,11 +13,10 @@ Author: Daniel Kroening

#include "json_goto_trace.h"

#include <cassert>

#include <util/json_expr.h>
#include <util/arith_tools.h>
#include <util/config.h>
#include <util/invariant.h>

#include <langapi/language_util.h>

Expand Down Expand Up @@ -194,7 +193,9 @@ void convert(
std::string value_string, binary_string, type_string, full_lhs_string;
json_objectt full_lhs_value;

assert(step.full_lhs.is_not_nil());
DATA_INVARIANT(
step.full_lhs.is_not_nil(),
"full_lhs in assignment must not be nil");
exprt simplified=simplify_array_access(step.full_lhs);
full_lhs_string=from_expr(ns, identifier, simplified);

Expand All @@ -214,7 +215,9 @@ void convert(
}
else
{
assert(step.full_lhs_value.is_not_nil());
DATA_INVARIANT(
step.full_lhs_value.is_not_nil(),
"full_lhs_value in assignment must not be nil");
full_lhs_value=json(step.full_lhs_value, ns);
}

Expand Down Expand Up @@ -251,6 +254,7 @@ void convert(
mode=ID_unknown;
else
mode=function_name->mode;
json_output["mode"]=json_stringt(id2string(mode));
json_arrayt &json_values=json_output["values"].make_array();

for(const auto &arg : step.io_args)
Expand All @@ -276,14 +280,23 @@ void convert(
json_input["thread"]=json_numbert(std::to_string(step.thread_nr));
json_input["inputID"]=json_stringt(id2string(step.io_id));

// Recovering the mode from the function
irep_idt mode;
const symbolt *function_name;
if(ns.lookup(source_location.get_function(), function_name))
// Failed to find symbol
mode=ID_unknown;
else
mode=function_name->mode;
json_input["mode"]=json_stringt(id2string(mode));
json_arrayt &json_values=json_input["values"].make_array();

for(const auto &arg : step.io_args)
{
if(arg.is_nil())
json_values.push_back(json_stringt(""));
else
json_values.push_back(json(arg, ns));
json_values.push_back(json(arg, ns, mode));
}

if(!json_location.is_null())
Expand Down
83 changes: 40 additions & 43 deletions src/util/json_expr.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,8 @@ Author: Peter Schrammel
#include "config.h"
#include "identifier.h"
#include "language.h"
#include "invariant.h"

#include <langapi/mode.h>

#include <memory>
Expand Down Expand Up @@ -228,6 +230,27 @@ json_objectt json(

if(expr.id()==ID_constant)
{
std::unique_ptr<languaget> lang;
if(mode==ID_unknown)
lang=std::unique_ptr<languaget>(get_default_language());
else
{
lang=std::unique_ptr<languaget>(get_language_from_mode(mode));
if(!lang)
lang=std::unique_ptr<languaget>(get_default_language());
}

const typet &underlying_type=
type.id()==ID_c_bit_field?type.subtype():
type;

std::string type_string;
bool error=lang->from_type(underlying_type, type_string, ns);
CHECK_RETURN(!error);

std::string value_string;
lang->from_expr(expr, value_string, ns);

const constant_exprt &constant_expr=to_constant_expr(expr);
if(type.id()==ID_unsignedbv ||
type.id()==ID_signedbv ||
Expand All @@ -238,45 +261,16 @@ json_objectt json(
result["name"]=json_stringt("integer");
result["binary"]=json_stringt(id2string(constant_expr.get_value()));
result["width"]=json_numbert(std::to_string(width));

const typet &underlying_type=
type.id()==ID_c_bit_field?type.subtype():
type;

std::unique_ptr<languaget> lang;
if(mode==ID_unknown)
lang=std::unique_ptr<languaget>(get_default_language());
else
{
lang=std::unique_ptr<languaget>(get_language_from_mode(mode));
if(!lang)
lang=std::unique_ptr<languaget>(get_default_language());
}

std::string type_string;
if(!lang->from_type(underlying_type, type_string, ns))
result["type"]=json_stringt(type_string);
else
assert(false && "unknown type");

mp_integer i;
if(!to_integer(expr, i))
result["data"]=json_stringt(integer2string(i));
else
assert(false && "could not convert data to integer");
result["type"]=json_stringt(type_string);
result["data"]=json_stringt(value_string);
}
else if(type.id()==ID_c_enum)
{
result["name"]=json_stringt("integer");
result["binary"]=json_stringt(id2string(constant_expr.get_value()));
result["width"]=json_numbert(type.subtype().get_string(ID_width));
result["type"]=json_stringt("enum");

mp_integer i;
if(!to_integer(expr, i))
result["data"]=json_stringt(integer2string(i));
else
assert(false && "could not convert data to integer");
result["data"]=json_stringt(value_string);
}
else if(type.id()==ID_c_enum_tag)
{
Expand Down Expand Up @@ -309,17 +303,20 @@ json_objectt json(
else if(type.id()==ID_pointer)
{
result["name"]=json_stringt("pointer");
result["type"]=json_stringt(type_string);
exprt simpl_expr=simplify_json_expr(expr, ns);
if(simpl_expr.get(ID_value)==ID_NULL ||
// remove typecast on NULL
(simpl_expr.id()==ID_constant && simpl_expr.type().id()==ID_pointer &&
simpl_expr.op0().get(ID_value)==ID_NULL))
result["data"]=json_stringt("NULL");
result["data"]=json_stringt(value_string);
else if(simpl_expr.id()==ID_symbol)
{
const irep_idt &ptr_id=to_symbol_expr(simpl_expr).get_identifier();
identifiert identifier(id2string(ptr_id));
assert(!identifier.components.empty());
DATA_INVARIANT(
!identifier.components.empty(),
"pointer identifier should have non-empty components");
result["data"]=json_stringt(identifier.components.back());
}
}
Expand All @@ -332,11 +329,10 @@ json_objectt json(
else if(type.id()==ID_c_bool)
{
result["name"]=json_stringt("integer");
result["type"]=json_stringt("_Bool");
result["width"]=json_numbert(type.get_string(ID_width));
result["type"]=json_stringt(type_string);
result["binary"]=json_stringt(expr.get_string(ID_value));
mp_integer b;
to_integer(to_constant_expr(expr), b);
result["data"]=json_stringt(integer2string(b));
result["data"]=json_stringt(value_string);
}
else if(type.id()==ID_string)
{
Expand Down Expand Up @@ -372,7 +368,9 @@ json_objectt json(
{
const struct_typet &struct_type=to_struct_type(type);
const struct_typet::componentst &components=struct_type.components();
assert(components.size()==expr.operands().size());
DATA_INVARIANT(
components.size()==expr.operands().size(),
"number of struct components should match with its type");

json_arrayt &members=result["members"].make_array();
for(unsigned m=0; m<expr.operands().size(); m++)
Expand All @@ -387,11 +385,10 @@ json_objectt json(
{
result["name"]=json_stringt("union");

assert(expr.operands().size()==1);

const union_exprt &union_expr=to_union_expr(expr);
json_objectt &e=result["member"].make_object();
e["value"]=json(expr.op0(), ns, mode);
e["name"]=json_stringt(id2string(to_union_expr(expr).get_component_name()));
e["value"]=json(union_expr.op(), ns, mode);
e["name"]=json_stringt(id2string(union_expr.get_component_name()));
}
else
result["name"]=json_stringt("unknown");
Expand Down