diff --git a/regression/strings-smoke-tests/jsonArrays/test.class b/regression/strings-smoke-tests/jsonArrays/test.class new file mode 100644 index 00000000000..e1e896095a3 Binary files /dev/null and b/regression/strings-smoke-tests/jsonArrays/test.class differ diff --git a/regression/strings-smoke-tests/jsonArrays/test.desc b/regression/strings-smoke-tests/jsonArrays/test.desc new file mode 100644 index 00000000000..e59f08d44b4 --- /dev/null +++ b/regression/strings-smoke-tests/jsonArrays/test.desc @@ -0,0 +1,10 @@ +CORE +test.class +--refine-strings --function test.check --json-ui --trace --string-max-length 100 --cover location +^EXIT=0$ +^SIGNAL=0$ +\"data\".*\"tmp_object_factory\$6.*\" +-- +This checks that tmp_object_factory$6 gets affected to the data field +of some strings, which was not the case in previous versions of cbmc, +as it was just ignored by the json output. \ No newline at end of file diff --git a/regression/strings-smoke-tests/jsonArrays/test.java b/regression/strings-smoke-tests/jsonArrays/test.java new file mode 100644 index 00000000000..c7b07e0fdec --- /dev/null +++ b/regression/strings-smoke-tests/jsonArrays/test.java @@ -0,0 +1,8 @@ +public class test +{ + public static int check(String s) + { + int i=Integer.parseInt(s); + return i; + } +} diff --git a/src/goto-programs/json_goto_trace.cpp b/src/goto-programs/json_goto_trace.cpp index eaa84f6654b..538bad49eff 100644 --- a/src/goto-programs/json_goto_trace.cpp +++ b/src/goto-programs/json_goto_trace.cpp @@ -14,11 +14,112 @@ Author: Daniel Kroening #include #include +#include #include #include "json_goto_trace.h" +/// Replaces in src, expressions of the form pointer_offset(constant) by that +/// constant. +/// \param src: an expression +void remove_pointer_offsets(exprt &src) +{ + if(src.id()==ID_pointer_offset && src.op0().id()==ID_constant) + src=src.op0(); + else + for(auto &op : src.operands()) + remove_pointer_offsets(op); +} + +/// Replaces in src, expressions of the form pointer_offset(array_symbol) by a +/// constant value of 0. This is meant to simplify array expressions. +/// \param src: an expression +/// \param array_symbol: a symbol expression representing an array +void remove_pointer_offsets(exprt &src, const symbol_exprt &array_symbol) +{ + if(src.id()==ID_pointer_offset && + src.op0().id()==ID_constant && + src.op0().op0().id()==ID_address_of && + src.op0().op0().op0().id()==ID_index) + { + const index_exprt &idx=to_index_expr(src.op0().op0().op0()); + const irep_idt &array_id=to_symbol_expr(idx.array()).get_identifier(); + if(idx.array().id()==ID_symbol && + array_id==array_symbol.get_identifier() && + to_constant_expr(idx.index()).value_is_zero_string()) + src=from_integer(0, src.type()); + } + else + for(auto &op : src.operands()) + remove_pointer_offsets(op, array_symbol); +} + +/// Simplify the expression in index as much as possible to try to get an +/// unsigned constant. +/// \param idx: an expression representing an index in an array +/// \param out: a reference to an unsigned value of type size_t, which will hold +/// the result of the simplification if it is successful +/// \return Boolean flag that is true if the `idx` expression could not be +/// simplified into a unsigned constant value. +bool simplify_index(const exprt &idx, std::size_t &out) +{ + if(idx.id()==ID_constant) + { + std::string value_str(id2string(to_constant_expr(idx).get_value())); + mp_integer int_value=binary2integer(value_str, false); + if(int_value>std::numeric_limits::max()) + return true; + out=int_value.to_long(); + return false; + } + else if(idx.id()==ID_plus) + { + std::size_t l, r; + if(!simplify_index(idx.op0(), l) && !simplify_index(idx.op1(), r)) + { + out=l+r; + return false; + } + } + + return true; +} + +/// Simplify an expression before putting it in the json format +/// \param src: an expression potentialy containing array accesses (index_expr) +/// \return an expression similar in meaning to src but where array accesses +/// have been simplified +exprt simplify_array_access(const exprt &src) +{ + if(src.id()==ID_index && to_index_expr(src).array().id()==ID_symbol) + { + // Case where the array is a symbol. + const symbol_exprt &array_symbol=to_symbol_expr(to_index_expr(src).array()); + exprt simplified_index=to_index_expr(src).index(); + // We remove potential appearances of `pointer_offset(array_symbol)` + remove_pointer_offsets(simplified_index, array_symbol); + return index_exprt(array_symbol, simplified_index); + } + else if(src.id()==ID_index && to_index_expr(src).array().id()==ID_array) + { + // Case where the array is given by an array of expressions + exprt index=to_index_expr(src).index(); + remove_pointer_offsets(index); + + // We look for an actual integer value for the index + std::size_t i; + if(!simplify_index(index, i)) + return to_index_expr(src).array().operands()[i]; + } + return src; +} + +/// Produce a json representation of a trace. +/// \param ns: a namespace +/// \param goto_trace: a trace in a goto program +/// \param dest: referecence to a json object in which the goto trace will be +/// added void convert( const namespacet &ns, const goto_tracet &goto_trace, @@ -84,7 +185,8 @@ void convert( json_objectt full_lhs_value; assert(step.full_lhs.is_not_nil()); - full_lhs_string=from_expr(ns, identifier, step.full_lhs); + exprt simplified=simplify_array_access(step.full_lhs); + full_lhs_string=from_expr(ns, identifier, simplified); const symbolt *symbol; irep_idt base_name, display_name; @@ -98,7 +200,8 @@ void convert( json_assignment["mode"]=json_stringt(id2string(symbol->mode)); assert(step.full_lhs_value.is_not_nil()); - full_lhs_value=json(step.full_lhs_value, ns, symbol->mode); + exprt simplified=simplify_array_access(step.full_lhs_value); + full_lhs_value=json(simplified, ns, symbol->mode); } else { diff --git a/src/util/json_expr.cpp b/src/util/json_expr.cpp index a9135f9f5ce..fd8be8bff71 100644 --- a/src/util/json_expr.cpp +++ b/src/util/json_expr.cpp @@ -52,16 +52,26 @@ static exprt simplify_json_expr( id2string(to_member_expr( src.op0()).get_component_name()).find("@")!=std::string::npos) { - // simplify things of the form &member_expr(object, @class_identifier) + // simplify expressions of the form &member_expr(object, @class_identifier) return simplify_json_expr(src.op0(), ns); } + else if(src.id()==ID_address_of && + src.operands().size()==1 && + src.op0().id()==ID_index && + to_index_expr(src.op0()).index().id()==ID_constant && + to_constant_expr( + to_index_expr(src.op0()).index()).value_is_zero_string()) + { + // simplify expressions of the form &array[0] + return simplify_json_expr(to_index_expr(src.op0()).array(), ns); + } else if(src.id()==ID_member && src.operands().size()==1 && id2string( to_member_expr(src).get_component_name()) .find("@")!=std::string::npos) { - // simplify things of the form member_expr(object, @class_identifier) + // simplify expressions of the form member_expr(object, @class_identifier) return simplify_json_expr(src.op0(), ns); }