diff --git a/regression/cbmc-java/json_trace2/Test.class b/regression/cbmc-java/json_trace2/Test.class new file mode 100644 index 00000000000..68771db843a Binary files /dev/null and b/regression/cbmc-java/json_trace2/Test.class differ diff --git a/regression/cbmc-java/json_trace2/Test.java b/regression/cbmc-java/json_trace2/Test.java new file mode 100644 index 00000000000..25608c219d3 --- /dev/null +++ b/regression/cbmc-java/json_trace2/Test.java @@ -0,0 +1,7 @@ +public class Test { + boolean test(Object x) { + if(x==null) + return false; + return true; + } +} diff --git a/regression/cbmc-java/json_trace2/test.desc b/regression/cbmc-java/json_trace2/test.desc new file mode 100644 index 00000000000..13d8774fb25 --- /dev/null +++ b/regression/cbmc-java/json_trace2/test.desc @@ -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 diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index e3cdaa7dd8b..edc7df455e5 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/src/goto-programs/json_goto_trace.cpp @@ -13,11 +13,10 @@ Author: Daniel Kroening #include "json_goto_trace.h" -#include - #include #include #include +#include #include @@ -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); @@ -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); } @@ -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) @@ -276,6 +280,15 @@ 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) @@ -283,7 +296,7 @@ void convert( 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()) diff --git a/src/util/json_expr.cpp b/src/util/json_expr.cpp index 4f5ce44d2fd..fd5db771cf8 100644 --- a/src/util/json_expr.cpp +++ b/src/util/json_expr.cpp @@ -21,6 +21,8 @@ Author: Peter Schrammel #include "config.h" #include "identifier.h" #include "language.h" +#include "invariant.h" + #include #include @@ -228,6 +230,27 @@ json_objectt json( if(expr.id()==ID_constant) { + std::unique_ptr lang; + if(mode==ID_unknown) + lang=std::unique_ptr(get_default_language()); + else + { + lang=std::unique_ptr(get_language_from_mode(mode)); + if(!lang) + lang=std::unique_ptr(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 || @@ -238,32 +261,8 @@ 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 lang; - if(mode==ID_unknown) - lang=std::unique_ptr(get_default_language()); - else - { - lang=std::unique_ptr(get_language_from_mode(mode)); - if(!lang) - lang=std::unique_ptr(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) { @@ -271,12 +270,7 @@ json_objectt json( 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) { @@ -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()); } } @@ -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) { @@ -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