diff --git a/jbmc/regression/jbmc/exception-cleanup/Test.class b/jbmc/regression/jbmc/exception-cleanup/Test.class new file mode 100644 index 00000000000..3fd53f09d11 Binary files /dev/null and b/jbmc/regression/jbmc/exception-cleanup/Test.class differ diff --git a/jbmc/regression/jbmc/exception-cleanup/Test.java b/jbmc/regression/jbmc/exception-cleanup/Test.java new file mode 100644 index 00000000000..1b937c87afe --- /dev/null +++ b/jbmc/regression/jbmc/exception-cleanup/Test.java @@ -0,0 +1,44 @@ +public class Test { + + public static void main(int unknown) { + + try { + mayThrow(unknown % 7 == 5); + } + catch(Exception e) { + } + + // This test checks that symex can tell there is no exception in flight + // (i.e. @inflight_exception is null) at this point, requiring it to + // converge the `if @inflight_exception == null` test on mayThrow's return + // with the explicit `@inflight_exception = null;` assignment that concludes + // the catch block. + + // If it knows that, it will also know the following catch block is + // unreachable; if not it will pursue both paths. + try { + mayThrow(false); + } + catch(Exception e) { + unreachable(); + } + + // Try it once more, to check we also know after an unreachable catch that + // there is still no inflight exception + try { + mayThrow(false); + } + catch(Exception e) { + unreachable(); + } + + } + + public static void mayThrow(boolean shouldThrow) throws Exception { + if(shouldThrow) + throw new Exception(); + } + + public static void unreachable() { assert false; } + +} diff --git a/jbmc/regression/jbmc/exception-cleanup/test.desc b/jbmc/regression/jbmc/exception-cleanup/test.desc new file mode 100644 index 00000000000..a3a271c9941 --- /dev/null +++ b/jbmc/regression/jbmc/exception-cleanup/test.desc @@ -0,0 +1,14 @@ +CORE +Test.class +--function Test.main +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +1 remaining after simplification$ +-- +^warning: ignoring +-- +The function "unreachable" should be successfully noted as unreachable by symex, +but the final uncaught-exception test in __CPROVER__start is not yet decidable +in symex, as it requires symex to note that within a catch block +@inflight_exception is definitely *not* null, which it can't just yet. diff --git a/jbmc/regression/jbmc/exception-cleanup/vccs.desc b/jbmc/regression/jbmc/exception-cleanup/vccs.desc new file mode 100644 index 00000000000..4dd86b143ae --- /dev/null +++ b/jbmc/regression/jbmc/exception-cleanup/vccs.desc @@ -0,0 +1,15 @@ +CORE +Test.class +--function Test.main --show-vcc +^EXIT=0$ +^SIGNAL=0$ +file Test\.java line 6 function java::Test.main:\(I\)V +no uncaught exception +-- +file Test\.java line 42 function java::Test\.unreachable:\(\)V bytecode-index 5 +assertion at file Test\.java line 42 function java::Test\.unreachable:\(\)V bytecode-index 5 +java::Test\.unreachable:\(\)V +^warning: ignoring +-- +Supplemental to test.desc, check that the right condition remains to be tested by the solver, +and the unreachable function indeed does not occur in the VCCs. diff --git a/regression/cbmc/condition-propagation-1/test.c b/regression/cbmc/condition-propagation-1/test.c new file mode 100644 index 00000000000..2beeb2e9149 --- /dev/null +++ b/regression/cbmc/condition-propagation-1/test.c @@ -0,0 +1,5 @@ +int main(int argc, char **argv) +{ + if(argc == 1) + assert(argc == 1); +} diff --git a/regression/cbmc/condition-propagation-1/test.desc b/regression/cbmc/condition-propagation-1/test.desc new file mode 100644 index 00000000000..cc3baab01eb --- /dev/null +++ b/regression/cbmc/condition-propagation-1/test.desc @@ -0,0 +1,12 @@ +CORE +test.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +0 remaining after simplification$ +-- +^warning: ignoring +-- +Assumption and GOTO condition propagation means this test should be +entirely decided by symex. diff --git a/regression/cbmc/condition-propagation-2/test.c b/regression/cbmc/condition-propagation-2/test.c new file mode 100644 index 00000000000..c47532f7b43 --- /dev/null +++ b/regression/cbmc/condition-propagation-2/test.c @@ -0,0 +1,5 @@ +int main(int argc, char **argv) +{ + __CPROVER_assume(argc == 1); + assert(argc == 1); +} diff --git a/regression/cbmc/condition-propagation-2/test.desc b/regression/cbmc/condition-propagation-2/test.desc new file mode 100644 index 00000000000..cc3baab01eb --- /dev/null +++ b/regression/cbmc/condition-propagation-2/test.desc @@ -0,0 +1,12 @@ +CORE +test.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +0 remaining after simplification$ +-- +^warning: ignoring +-- +Assumption and GOTO condition propagation means this test should be +entirely decided by symex. diff --git a/regression/cbmc/condition-propagation-3/test.c b/regression/cbmc/condition-propagation-3/test.c new file mode 100644 index 00000000000..e4dd134b94f --- /dev/null +++ b/regression/cbmc/condition-propagation-3/test.c @@ -0,0 +1,10 @@ +int main(int argc, char **argv) +{ + if(argc != 1) + { + } + else + { + assert(argc == 1); + } +} diff --git a/regression/cbmc/condition-propagation-3/test.desc b/regression/cbmc/condition-propagation-3/test.desc new file mode 100644 index 00000000000..cc3baab01eb --- /dev/null +++ b/regression/cbmc/condition-propagation-3/test.desc @@ -0,0 +1,12 @@ +CORE +test.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +0 remaining after simplification$ +-- +^warning: ignoring +-- +Assumption and GOTO condition propagation means this test should be +entirely decided by symex. diff --git a/regression/cbmc/condition-propagation-4/test.c b/regression/cbmc/condition-propagation-4/test.c new file mode 100644 index 00000000000..945fc8c3357 --- /dev/null +++ b/regression/cbmc/condition-propagation-4/test.c @@ -0,0 +1,15 @@ +int main(int argc, char **argv) +{ + int unknown; + + if(argc != 1) + { + } + else + { + if(unknown == argc) + { + assert(unknown == 1); + } + } +} diff --git a/regression/cbmc/condition-propagation-4/test.desc b/regression/cbmc/condition-propagation-4/test.desc new file mode 100644 index 00000000000..cc3baab01eb --- /dev/null +++ b/regression/cbmc/condition-propagation-4/test.desc @@ -0,0 +1,12 @@ +CORE +test.c + +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +0 remaining after simplification$ +-- +^warning: ignoring +-- +Assumption and GOTO condition propagation means this test should be +entirely decided by symex. diff --git a/src/goto-symex/goto_state.cpp b/src/goto-symex/goto_state.cpp index 8326d9915a4..82ca5b40463 100644 --- a/src/goto-symex/goto_state.cpp +++ b/src/goto-symex/goto_state.cpp @@ -7,6 +7,8 @@ Author: Romain Brenguier, romain.brenguier@diffblue.com \*******************************************************************/ #include "goto_state.h" +#include "goto_symex_is_constant.h" +#include "goto_symex_state.h" #include @@ -20,3 +22,74 @@ void goto_statet::output_propagation_map(std::ostream &out) out << name_value.first << " <- " << format(name_value.second) << "\n"; } } + +std::size_t goto_statet::increase_generation( + const irep_idt l1_identifier, + const ssa_exprt &lhs, + std::function fresh_l2_name_provider) +{ + auto current_emplace_res = + level2.current_names.emplace(l1_identifier, std::make_pair(lhs, 0)); + + current_emplace_res.first->second.second = + fresh_l2_name_provider(l1_identifier); + + return current_emplace_res.first->second.second; +} + +/// Given a condition that must hold on this path, propagate as much knowledge +/// as possible. For example, if the condition is (x == 5), whether that's an +/// assumption or a GOTO condition that we just passed through, we can propagate +/// the constant '5' for future 'x' references. If the condition is (y == &o1) +/// then we can use that to populate the value set. +/// \param condition: condition that must hold on this path. Expected to already +/// be L2-renamed. +/// \param previous_state: currently active state, not necessarily the same as +/// *this. For a GOTO instruction this is the state immediately preceding the +/// branch while *this is the state that will be used on the taken- or +/// not-taken path. For an ASSUME instruction \p previous_state and *this are +/// equal. +/// \param ns: global namespace +void goto_statet::apply_condition( + const exprt &condition, + const goto_symex_statet &previous_state, + const namespacet &ns) +{ + if(condition.id() == ID_and) + { + for(const auto &op : condition.operands()) + apply_condition(op, previous_state, ns); + } + else if(condition.id() == ID_equal) + { + exprt lhs = condition.op0(); + exprt rhs = condition.op1(); + if(is_ssa_expr(rhs)) + std::swap(lhs, rhs); + + if(is_ssa_expr(lhs) && goto_symex_is_constantt()(rhs)) + { + const ssa_exprt &ssa_lhs = to_ssa_expr(lhs); + INVARIANT( + !ssa_lhs.get_level_2().empty(), + "apply_condition operand should be L2 renamed"); + + if( + previous_state.threads.size() == 1 || + previous_state.write_is_shared(ssa_lhs, ns) != + goto_symex_statet::write_is_shared_resultt::SHARED) + { + ssa_exprt l1_lhs = ssa_lhs; + l1_lhs.remove_level_2(); + const irep_idt &l1_identifier = l1_lhs.get_identifier(); + + increase_generation( + l1_identifier, l1_lhs, previous_state.get_l2_name_provider()); + + propagation[l1_identifier] = rhs; + + value_set.assign(l1_lhs, rhs, ns, true, false); + } + } + } +} diff --git a/src/goto-symex/goto_state.h b/src/goto-symex/goto_state.h index 23ae0b9c14a..b33235a9870 100644 --- a/src/goto-symex/goto_state.h +++ b/src/goto-symex/goto_state.h @@ -74,6 +74,16 @@ class goto_statet : guard(true_exprt(), guard_manager) { } + + void apply_condition( + const exprt &condition, // L2 + const goto_symex_statet &previous_state, + const namespacet &ns); + + std::size_t increase_generation( + const irep_idt l1_identifier, + const ssa_exprt &lhs, + std::function fresh_l2_name_provider); }; #endif // CPROVER_GOTO_SYMEX_GOTO_STATE_H diff --git a/src/goto-symex/goto_symex_is_constant.h b/src/goto-symex/goto_symex_is_constant.h new file mode 100644 index 00000000000..f218ff53b32 --- /dev/null +++ b/src/goto-symex/goto_symex_is_constant.h @@ -0,0 +1,53 @@ +/*******************************************************************\ + +Module: Symbolic Execution Constant Propagation + +Author: Michael Tautschig, tautschn@amazon.com + +\*******************************************************************/ + +/// \file +/// GOTO Symex constant propagation + +#ifndef CPROVER_GOTO_SYMEX_GOTO_SYMEX_IS_CONSTANT_H +#define CPROVER_GOTO_SYMEX_GOTO_SYMEX_IS_CONSTANT_H + +#include +#include + +class goto_symex_is_constantt : public is_constantt +{ +protected: + bool is_constant(const exprt &expr) const override + { + if(expr.id() == ID_mult) + { + // propagate stuff with sizeof in it + forall_operands(it, expr) + { + if(it->find(ID_C_c_sizeof_type).is_not_nil()) + return true; + else if(!is_constant(*it)) + return false; + } + + return true; + } + else if(expr.id() == ID_with) + { + // this is bad + /* + forall_operands(it, expr) + if(!is_constant(expr.op0())) + return false; + + return true; + */ + return false; + } + + return is_constantt::is_constant(expr); + } +}; + +#endif // CPROVER_GOTO_SYMEX_GOTO_SYMEX_IS_CONSTANT_H diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp index 97d898a60df..772256dd633 100644 --- a/src/goto-symex/goto_symex_state.cpp +++ b/src/goto-symex/goto_symex_state.cpp @@ -10,6 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com /// Symbolic Execution #include "goto_symex_state.h" +#include "goto_symex_is_constant.h" #include #include @@ -130,41 +131,6 @@ static bool check_renaming(const exprt &expr) return false; } -class goto_symex_is_constantt : public is_constantt -{ -protected: - bool is_constant(const exprt &expr) const override - { - if(expr.id() == ID_mult) - { - // propagate stuff with sizeof in it - forall_operands(it, expr) - { - if(it->find(ID_C_c_sizeof_type).is_not_nil()) - return true; - else if(!is_constant(*it)) - return false; - } - - return true; - } - else if(expr.id() == ID_with) - { - // this is bad - /* - forall_operands(it, expr) - if(!is_constant(expr.op0())) - return false; - - return true; - */ - return false; - } - - return is_constantt::is_constant(expr); - } -}; - template <> renamedt goto_symex_statet::set_indices(ssa_exprt ssa_expr, const namespacet &ns) @@ -493,22 +459,6 @@ bool goto_symex_statet::l2_thread_read_encoding( return true; } -/// Allocates a fresh L2 name for the given L1 identifier, and makes it the -/// latest generation on this path. -/// \return the newly allocated generation number -std::size_t goto_symex_statet::increase_generation( - const irep_idt l1_identifier, - const ssa_exprt &lhs) -{ - auto current_emplace_res = - level2.current_names.emplace(l1_identifier, std::make_pair(lhs, 0)); - - current_emplace_res.first->second.second = - fresh_l2_name_provider(l1_identifier); - - return current_emplace_res.first->second.second; -} - /// Allocates a fresh L2 name for the given L1 identifier, and makes it the /// latest generation on this path. Does nothing if there isn't an expression /// keyed by the l1 identifier. @@ -522,32 +472,47 @@ void goto_symex_statet::increase_generation_if_exists(const irep_idt identifier) current_names_iter->second.second = fresh_l2_name_provider(identifier); } -/// thread encoding -bool goto_symex_statet::l2_thread_write_encoding( +goto_symex_statet::write_is_shared_resultt goto_symex_statet::write_is_shared( const ssa_exprt &expr, - const namespacet &ns) + const namespacet &ns) const { if(!record_events) - return false; + return write_is_shared_resultt::NOT_SHARED; - // is it a shared object? - const irep_idt &obj_identifier=expr.get_object_name(); + const irep_idt &obj_identifier = expr.get_object_name(); if( obj_identifier == guard_identifier() || (!ns.lookup(obj_identifier).is_shared() && !(dirty)(obj_identifier))) { - return false; // not shared + return write_is_shared_resultt::NOT_SHARED; } - // see whether we are within an atomic section - if(atomic_section_id!=0) + if(atomic_section_id != 0) + return write_is_shared_resultt::IN_ATOMIC_SECTION; + + return write_is_shared_resultt::SHARED; +} + +/// thread encoding +bool goto_symex_statet::l2_thread_write_encoding( + const ssa_exprt &expr, + const namespacet &ns) +{ + switch(write_is_shared(expr, ns)) { - ssa_exprt ssa_l1=expr; + case write_is_shared_resultt::NOT_SHARED: + return false; + case write_is_shared_resultt::IN_ATOMIC_SECTION: + { + ssa_exprt ssa_l1 = expr; ssa_l1.remove_level_2(); written_in_atomic_section[ssa_l1].push_back(guard); return false; } + case write_is_shared_resultt::SHARED: + break; + } // record a shared write symex_target->shared_write( @@ -557,7 +522,7 @@ bool goto_symex_statet::l2_thread_write_encoding( source); // do we have threads? - return threads.size()>1; + return threads.size() > 1; } template diff --git a/src/goto-symex/goto_symex_state.h b/src/goto-symex/goto_symex_state.h index db38fbc74e3..9fb65bf5bcb 100644 --- a/src/goto-symex/goto_symex_state.h +++ b/src/goto-symex/goto_symex_state.h @@ -181,8 +181,17 @@ class goto_symex_statet final : public goto_statet std::vector threads; + enum class write_is_shared_resultt + { + NOT_SHARED, + IN_ATOMIC_SECTION, + SHARED + }; + bool l2_thread_read_encoding(ssa_exprt &expr, const namespacet &ns); bool l2_thread_write_encoding(const ssa_exprt &expr, const namespacet &ns); + write_is_shared_resultt + write_is_shared(const ssa_exprt &expr, const namespacet &ns) const; bool record_events; @@ -208,7 +217,11 @@ class goto_symex_statet final : public goto_statet /// Allocates a fresh L2 name for the given L1 identifier, and makes it the // latest generation on this path. std::size_t - increase_generation(const irep_idt l1_identifier, const ssa_exprt &lhs); + increase_generation(const irep_idt l1_identifier, const ssa_exprt &lhs) + { + return goto_statet::increase_generation( + l1_identifier, lhs, fresh_l2_name_provider); + } /// Increases the generation of the L1 identifier. Does nothing if there /// isn't an expression keyed by it. @@ -220,6 +233,11 @@ class goto_symex_statet final : public goto_statet level2.current_names.erase(it); } + std::function get_l2_name_provider() const + { + return fresh_l2_name_provider; + } + private: std::function fresh_l2_name_provider; diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 390e03896bd..91e8a923c61 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -22,6 +22,36 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +/// Propagate constants and points-to information implied by a GOTO condition. +/// See \ref goto_statet::apply_condition for aspects of this which are common +/// to GOTO and ASSUME instructions. +/// \param current_state: state prior to the GOTO instruction +/// \param jump_taken_state: state following taking the GOTO +/// \param jump_not_taken_state: fall-through state +/// \param new_guard: GOTO condition, L2 renamed and simplified +/// \param ns: global namespace +static void apply_goto_condition( + const goto_symex_statet ¤t_state, + goto_statet &jump_taken_state, + goto_statet &jump_not_taken_state, + const exprt &new_guard, + const namespacet &ns) +{ + jump_taken_state.apply_condition(new_guard, current_state, ns); + + // Try to find a negative condition that implies an equality constraint on + // the branch-not-taken path. + // Could use not_exprt + simplify, but let's avoid paying that cost on quite + // a hot path: + if(new_guard.id() == ID_not) + jump_not_taken_state.apply_condition(new_guard.op0(), current_state, ns); + else if(new_guard.id() == ID_notequal) + { + jump_not_taken_state.apply_condition( + equal_exprt(new_guard.op0(), new_guard.op1()), current_state, ns); + } +} + void goto_symext::symex_goto(statet &state) { const goto_programt::instructiont &instruction=*state.source.pc; @@ -230,6 +260,17 @@ void goto_symext::symex_goto(statet &state) symex_transition(state, state_pc, backward); + if(!symex_config.doing_path_exploration) + { + // This doesn't work for --paths (single-path mode) yet, as in multi-path + // mode we remove the implied constants at a control-flow merge, but in + // single-path mode we don't run merge_gotos. + auto &taken_state = backward ? state : goto_state_list.back().second; + auto ¬_taken_state = backward ? goto_state_list.back().second : state; + + apply_goto_condition(state, taken_state, not_taken_state, new_guard, ns); + } + // produce new guard symbol exprt guard_expr; diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp index d0e66eb15ca..0745eca1c35 100644 --- a/src/goto-symex/symex_main.cpp +++ b/src/goto-symex/symex_main.cpp @@ -160,6 +160,8 @@ void goto_symext::symex_assume_l2(statet &state, const exprt &cond) if(state.atomic_section_id!=0 && state.guard.is_false()) symex_atomic_end(state); + + state.apply_condition(cond, state, ns); } void goto_symext::rewrite_quantifiers(exprt &expr, statet &state) diff --git a/unit/path_strategies.cpp b/unit/path_strategies.cpp index 5e95f88c872..451be55eb66 100644 --- a/unit/path_strategies.cpp +++ b/unit/path_strategies.cpp @@ -160,14 +160,14 @@ SCENARIO("path strategies") "/* 1 */ int main() \n" "/* 2 */ { \n" "/* 3 */ int x; \n" - "/* 4 */ " CPROVER_PREFIX - "assume(x == 1); \n" + "/* 4 */ if(x == 1) { \n" "/* 5 */ \n" - "/* 6 */ while(x) \n" - "/* 7 */ --x; \n" + "/* 6 */ while(x) \n" + "/* 7 */ --x; \n" "/* 8 */ \n" - "/* 9 */ assert(x); \n" - "/* 10 */ } \n"; + "/* 9 */ assert(x); \n" + "/* 10 */ } \n" + "/* 11 */ } \n"; // clang-format on check_with_strategy( @@ -175,8 +175,12 @@ SCENARIO("path strategies") opts_callback, c, { + // The path where x != 1 and we have nothing to check: + symex_eventt::resume(symex_eventt::enumt::JUMP, 11), + // The path where we skip the loop body. Successful because the path is // implausible, we cannot have skipped the body if x == 1. + symex_eventt::resume(symex_eventt::enumt::NEXT, 6), symex_eventt::resume(symex_eventt::enumt::JUMP, 9), symex_eventt::result(symex_eventt::enumt::SUCCESS), @@ -200,6 +204,12 @@ SCENARIO("path strategies") opts_callback, c, { + // First the path where we enter the if-block at line 4 then on hitting + // the branch at line 6 consider skipping straight to the end, but find + // nothing there to investigate: + symex_eventt::resume(symex_eventt::enumt::NEXT, 6), + symex_eventt::resume(symex_eventt::enumt::JUMP, 11), + // The path where we skip the loop body. Successful because the path is // implausible, we cannot have skipped the body if x == 1. //