diff --git a/jbmc/regression/jbmc-strings/StartsWith/test_nondet.desc b/jbmc/regression/jbmc-strings/StartsWith/test_nondet.desc index 3e02ea3ee0f..183387d7d51 100644 --- a/jbmc/regression/jbmc-strings/StartsWith/test_nondet.desc +++ b/jbmc/regression/jbmc-strings/StartsWith/test_nondet.desc @@ -1,4 +1,4 @@ -CORE +KNOWNBUG Test.class --max-nondet-string-length 100 --unwind 10 --function Test.checkNonDet ^EXIT=10$ @@ -6,3 +6,8 @@ Test.class assertion at file Test.java line 66 .*: SUCCESS assertion at file Test.java line 69 .*: FAILURE -- +-- +The nondet test currently breaks the invariant at string_refinement.cpp:2162 +("Indices not equal..."), which checks that a given string is not used with +multiple distinct indices. As the test checks s.substring(s, 1), two distinct +indices are indeed used. diff --git a/jbmc/regression/jbmc/clean_derefs/Container.class b/jbmc/regression/jbmc/clean_derefs/Container.class new file mode 100644 index 00000000000..ac0f01ac141 Binary files /dev/null and b/jbmc/regression/jbmc/clean_derefs/Container.class differ diff --git a/jbmc/regression/jbmc/clean_derefs/Test.class b/jbmc/regression/jbmc/clean_derefs/Test.class new file mode 100644 index 00000000000..f0486e49eb1 Binary files /dev/null and b/jbmc/regression/jbmc/clean_derefs/Test.class differ diff --git a/jbmc/regression/jbmc/clean_derefs/Test.java b/jbmc/regression/jbmc/clean_derefs/Test.java new file mode 100644 index 00000000000..b971b769b6b --- /dev/null +++ b/jbmc/regression/jbmc/clean_derefs/Test.java @@ -0,0 +1,50 @@ + +public class Test { + + public int field; + + public Test(int f) { field = f; } + + public static void main(int nondet) { + + // This test creates and uses objects in a few different contexts to check + // that in all cases goto-symex realises that the dereferenced object cannot + // be null (due to the NullPointerException check that guards all derefs), + // therefore symex never generates a reference to any $failed_object symbol + // that for a C program would stand in for an unknown or invalid object such + // as a dereferenced null pointer. + + Test t1 = new Test(nondet); + Test t2 = new Test(nondet); + + Test[] tarray = new Test[5]; + tarray[0] = null; + tarray[1] = t2; + tarray[2] = t1; + + t1.field++; + (nondet == 10 ? t1 : t2).field--; + tarray[nondet % 5].field++; + (nondet == 20 ? t1 : tarray[2]).field++; + + Container c1 = new Container(t1); + Container c2 = new Container(t2); + Container c3 = new Container(null); + + c1.t.field++; + (nondet == 30 ? c1 : c3).t.field++; + (nondet == 40 ? c2.t : tarray[3]).field--; + + assert false; + + } + +} + +class Container { + + public Container(Test _t) { t = _t; } + + public Test t; + +} diff --git a/jbmc/regression/jbmc/clean_derefs/test.desc b/jbmc/regression/jbmc/clean_derefs/test.desc new file mode 100644 index 00000000000..6554cae36f5 --- /dev/null +++ b/jbmc/regression/jbmc/clean_derefs/test.desc @@ -0,0 +1,11 @@ +CORE +Test.class +--function Test.main --show-vcc +^EXIT=0$ +^SIGNAL=0$ +-- +invalid +-- +This checks that no invalid_object references are generated -- these would be created if +symex thought it might follow a null or other invalid pointer, whereas Java dereferences +should always be checked not-null beforehand. diff --git a/src/analyses/local_safe_pointers.cpp b/src/analyses/local_safe_pointers.cpp index cd632bd8c37..213bdecabc2 100644 --- a/src/analyses/local_safe_pointers.cpp +++ b/src/analyses/local_safe_pointers.cpp @@ -11,68 +11,68 @@ Author: Diffblue Ltd #include "local_safe_pointers.h" +#include #include +#include #include -/// If `expr` is of the form `x != nullptr`, return x. Otherwise return null -static const exprt *get_null_checked_expr(const exprt &expr) -{ - if(expr.id() == ID_notequal) - { - const exprt *op0 = &expr.op0(), *op1 = &expr.op1(); - if(op0->type().id() == ID_pointer && - *op0 == null_pointer_exprt(to_pointer_type(op0->type()))) - { - std::swap(op0, op1); - } - - if(op1->type().id() == ID_pointer && - *op1 == null_pointer_exprt(to_pointer_type(op1->type()))) - { - while(op0->id() == ID_typecast) - op0 = &op0->op0(); - return op0; - } - } - - return nullptr; -} - -/// Return structure for `get_conditional_checked_expr` +/// Return structure for `get_null_checked_expr` and +/// `get_conditional_checked_expr` struct goto_null_checkt { - /// If true, the given GOTO tests that a pointer expression is non-null on the - /// taken branch; otherwise, on the not-taken branch. + /// If true, the given GOTO/ASSUME tests that a pointer expression is non-null + /// on the taken branch or passing case; otherwise, on the not-taken branch + /// or on failure. bool checked_when_taken; /// Null-tested pointer expression exprt checked_expr; }; -/// Check if a GOTO guard expression tests if a pointer is null -/// \param goto_guard: expression to check +/// Check if `expr` tests if a pointer is null +/// \param expr: expression to check /// \return a `goto_null_checkt` indicating what expression is tested and /// whether the check applies on the taken or not-taken branch, or an empty /// optionalt if this isn't a null check. -static optionalt -get_conditional_checked_expr(const exprt &goto_guard) +static optionalt get_null_checked_expr(const exprt &expr) { - exprt normalized_guard = goto_guard; + exprt normalized_expr = expr; + // If true, then a null check is made when test `expr` passes; if false, + // one is made when it fails. bool checked_when_taken = true; - while(normalized_guard.id() == ID_not || normalized_guard.id() == ID_equal) + + // Reduce some roundabout ways of saying "x != null", e.g. "!(x == null)". + while(normalized_expr.id() == ID_not) { - if(normalized_guard.id() == ID_not) - normalized_guard = normalized_guard.op0(); - else - normalized_guard.id(ID_notequal); + normalized_expr = normalized_expr.op0(); checked_when_taken = !checked_when_taken; } - const exprt *checked_expr = get_null_checked_expr(normalized_guard); - if(!checked_expr) - return {}; - else - return goto_null_checkt { checked_when_taken, *checked_expr }; + if(normalized_expr.id() == ID_equal) + { + normalized_expr.id(ID_notequal); + checked_when_taken = !checked_when_taken; + } + + if(normalized_expr.id() == ID_notequal) + { + const exprt &op0 = skip_typecast(normalized_expr.op0()); + const exprt &op1 = skip_typecast(normalized_expr.op1()); + + if(op0.type().id() == ID_pointer && + op0 == null_pointer_exprt(to_pointer_type(op0.type()))) + { + return { { checked_when_taken, op1 } }; + } + + if(op1.type().id() == ID_pointer && + op1 == null_pointer_exprt(to_pointer_type(op1.type()))) + { + return { { checked_when_taken, op0 } }; + } + } + + return {}; } /// Compute safe dereference expressions for a given GOTO program. This @@ -82,7 +82,8 @@ get_conditional_checked_expr(const exprt &goto_guard) /// \param goto_program: program to analyse void local_safe_pointerst::operator()(const goto_programt &goto_program) { - std::set checked_expressions; + std::set checked_expressions( + base_type_comparet{ns}); for(const auto &instruction : goto_program.instructions) { @@ -91,11 +92,23 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program) checked_expressions.clear(); // Retrieve working set for forward GOTOs: else if(instruction.is_target()) - checked_expressions = non_null_expressions[instruction.location_number]; + { + auto findit = non_null_expressions.find(instruction.location_number); + if(findit != non_null_expressions.end()) + checked_expressions = findit->second; + else + { + checked_expressions = + std::set(base_type_comparet{ns}); + } + } // Save the working set at this program point: if(!checked_expressions.empty()) - non_null_expressions[instruction.location_number] = checked_expressions; + { + non_null_expressions.emplace( + instruction.location_number, checked_expressions); + } switch(instruction.type) { @@ -113,35 +126,44 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program) // Possible checks: case ASSUME: + if(auto assume_check = get_null_checked_expr(instruction.guard)) { - const exprt *checked_expr; - if((checked_expr = get_null_checked_expr(instruction.guard)) != nullptr) - { - checked_expressions.insert(*checked_expr); - } - break; + if(assume_check->checked_when_taken) + checked_expressions.insert(assume_check->checked_expr); } + break; + case GOTO: if(!instruction.is_backwards_goto()) { - if(auto conditional_check = - get_conditional_checked_expr(instruction.guard)) - { - auto &taken_checked_expressions = - non_null_expressions[instruction.get_target()->location_number]; - taken_checked_expressions = checked_expressions; + // Copy current state to GOTO target: - if(conditional_check->checked_when_taken) - taken_checked_expressions.insert(conditional_check->checked_expr); - else - checked_expressions.insert(conditional_check->checked_expr); + auto target_emplace_result = + non_null_expressions.emplace( + instruction.get_target()->location_number, checked_expressions); - break; + // If the target already has a state entry then it is a control-flow + // merge point and everything will be assumed maybe-null in any case. + if(target_emplace_result.second) + { + if(auto conditional_check = get_null_checked_expr(instruction.guard)) + { + // Add the GOTO condition to either the target or current state, + // as appropriate: + if(conditional_check->checked_when_taken) + { + target_emplace_result.first->second.insert( + conditional_check->checked_expr); + } + else + checked_expressions.insert(conditional_check->checked_expr); + } } - // Otherwise fall through to... } + break; + default: // Pessimistically assume all other instructions might overwrite any // pointer with a possibly-null value. @@ -157,7 +179,7 @@ void local_safe_pointerst::operator()(const goto_programt &goto_program) /// operator()) /// \param ns: global namespace void local_safe_pointerst::output( - std::ostream &out, const goto_programt &goto_program, const namespacet &ns) + std::ostream &out, const goto_programt &goto_program) { forall_goto_program_instructions(i_it, goto_program) { @@ -199,7 +221,7 @@ void local_safe_pointerst::output( /// operator()) /// \param ns: global namespace void local_safe_pointerst::output_safe_dereferences( - std::ostream &out, const goto_programt &goto_program, const namespacet &ns) + std::ostream &out, const goto_programt &goto_program) { forall_goto_program_instructions(i_it, goto_program) { @@ -251,3 +273,12 @@ bool local_safe_pointerst::is_non_null_at_program_point( tocheck = &tocheck->op0(); return findit->second.count(*tocheck) != 0; } + +bool local_safe_pointerst::base_type_comparet::operator()( + const exprt &e1, const exprt &e2) const +{ + if(base_type_eq(e1, e2, ns)) + return false; + else + return e1 < e2; +} diff --git a/src/analyses/local_safe_pointers.h b/src/analyses/local_safe_pointers.h index 4d0a43b3043..6239a9364f3 100644 --- a/src/analyses/local_safe_pointers.h +++ b/src/analyses/local_safe_pointers.h @@ -23,9 +23,45 @@ Author: Diffblue Ltd /// possibly-aliasing operations are handled pessimistically. class local_safe_pointerst { - std::map> non_null_expressions; + /// Comparator that regards base_type_eq expressions as equal, and otherwise + /// uses the natural (operator<) ordering on irept. + /// An expression is base_type_eq another one if their types, and types of + /// their subexpressions, are identical except that one may use a symbol_typet + /// while the other uses that type's expanded (namespacet::follow'd) form. + class base_type_comparet + { + const namespacet &ns; + + public: + explicit base_type_comparet(const namespacet &ns) + : ns(ns) + { + } + + base_type_comparet(const base_type_comparet &other) + : ns(other.ns) + { + } + + base_type_comparet &operator=(const base_type_comparet &other) + { + INVARIANT(&ns == &other.ns, "base_type_comparet: clashing namespaces"); + return *this; + } + + bool operator()(const exprt &e1, const exprt &e2) const; + }; + + std::map> non_null_expressions; + + const namespacet &ns; + +public: + local_safe_pointerst(const namespacet &ns) + : ns(ns) + { + } - public: void operator()(const goto_programt &goto_program); bool is_non_null_at_program_point( @@ -38,11 +74,10 @@ class local_safe_pointerst return is_non_null_at_program_point(deref.op0(), program_point); } - void output( - std::ostream &stream, const goto_programt &program, const namespacet &ns); + void output(std::ostream &stream, const goto_programt &program); void output_safe_dereferences( - std::ostream &stream, const goto_programt &program, const namespacet &ns); + std::ostream &stream, const goto_programt &program); }; #endif // CPROVER_ANALYSES_LOCAL_SAFE_POINTERS_H diff --git a/src/goto-instrument/goto_instrument_parse_options.cpp b/src/goto-instrument/goto_instrument_parse_options.cpp index 0151f563507..4582509df7d 100644 --- a/src/goto-instrument/goto_instrument_parse_options.cpp +++ b/src/goto-instrument/goto_instrument_parse_options.cpp @@ -297,17 +297,17 @@ int goto_instrument_parse_optionst::doit() forall_goto_functions(it, goto_model.goto_functions) { - local_safe_pointerst local_safe_pointers; + local_safe_pointerst local_safe_pointers(ns); local_safe_pointers(it->second.body); std::cout << ">>>>\n"; std::cout << ">>>> " << it->first << '\n'; std::cout << ">>>>\n"; if(cmdline.isset("show-local-safe-pointers")) - local_safe_pointers.output(std::cout, it->second.body, ns); + local_safe_pointers.output(std::cout, it->second.body); else { local_safe_pointers.output_safe_dereferences( - std::cout, it->second.body, ns); + std::cout, it->second.body); } std::cout << '\n'; } diff --git a/src/goto-symex/symex_function_call.cpp b/src/goto-symex/symex_function_call.cpp index 1953e898a4c..dc2aaa9ec67 100644 --- a/src/goto-symex/symex_function_call.cpp +++ b/src/goto-symex/symex_function_call.cpp @@ -223,7 +223,7 @@ void goto_symext::symex_function_call_code( state.dirty.populate_dirty_for_function(identifier, goto_function); auto emplace_safe_pointers_result = - safe_pointers.emplace(identifier, local_safe_pointerst{}); + safe_pointers.emplace(identifier, local_safe_pointerst{ns}); if(emplace_safe_pointers_result.second) emplace_safe_pointers_result.first->second(goto_function.body); diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index 63f1aa1d3b1..5e576e7d488 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -136,7 +136,7 @@ void goto_symext::initialize_entry_point( const goto_functiont &entry_point_function = get_goto_function(pc->function); auto emplace_safe_pointers_result = - safe_pointers.emplace(pc->function, local_safe_pointerst{}); + safe_pointers.emplace(pc->function, local_safe_pointerst{ns}); if(emplace_safe_pointers_result.second) emplace_safe_pointers_result.first->second(entry_point_function.body);