From 0399f89b62e3ab7e55fcd93035bb979df3ed55a1 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Tue, 28 May 2019 16:19:09 +0100 Subject: [PATCH 1/8] Do not expose add_to_lhs in goto_symex interface This is only used in symex_assign.cpp so does not need to be exposed. --- src/goto-symex/goto_symex.h | 8 -------- src/goto-symex/symex_assign.cpp | 10 +++++++--- 2 files changed, 7 insertions(+), 11 deletions(-) diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 273bb50e962..7b5fe4af8d8 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -602,14 +602,6 @@ class goto_symext exprt::operandst &, assignment_typet); - /// Store the \p what expression by recursively descending into the operands - /// of \p lhs until the first operand \c op0 is _nil_: this _nil_ operand - /// is then replaced with \p what. - /// \param lhs: Non-symbol pointed-to expression - /// \param what: The expression to be added to the \p lhs - /// \return The resulting expression - static exprt add_to_lhs(const exprt &lhs, const exprt &what); - virtual void symex_va_start(statet &, const exprt &lhs, const side_effect_exprt &); diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 0b91b7b71d6..c96db412499 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -79,9 +79,13 @@ void goto_symext::symex_assign(statet &state, const code_assignt &code) } } -exprt goto_symext::add_to_lhs( - const exprt &lhs, - const exprt &what) +/// Store the \p what expression by recursively descending into the operands +/// of \p lhs until the first operand \c op0 is _nil_: this _nil_ operand +/// is then replaced with \p what. +/// \param lhs: Non-symbol pointed-to expression +/// \param what: The expression to be added to the \p lhs +/// \return The resulting expression +static exprt add_to_lhs(const exprt &lhs, const exprt &what) { PRECONDITION(lhs.id() != ID_symbol); exprt tmp_what=what; From efb8960a00970429d092fe30c0d3f726f70ea365 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 29 May 2019 08:57:51 +0100 Subject: [PATCH 2/8] Remove unecessary type assignment The with_exprt constructor already sets the type to the array type. --- src/goto-symex/symex_assign.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index c96db412499..72463113caa 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -569,8 +569,6 @@ void goto_symext::symex_assign_array( // a'==a WITH [i:=e] with_exprt new_rhs(lhs_array, lhs_index, rhs); - new_rhs.type() = lhs_index_type; - exprt new_full_lhs=add_to_lhs(full_lhs, lhs); symex_assign_rec( From 7deec89ae74478b2b4e0a50a6a1548154d129af5 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 29 May 2019 08:58:57 +0100 Subject: [PATCH 3/8] Add missing const Makes explicit that these won't be changed. --- src/goto-symex/symex_assign.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 72463113caa..3843e960af8 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -568,8 +568,8 @@ void goto_symext::symex_assign_array( // into // a'==a WITH [i:=e] - with_exprt new_rhs(lhs_array, lhs_index, rhs); - exprt new_full_lhs=add_to_lhs(full_lhs, lhs); + const with_exprt new_rhs{lhs_array, lhs_index, rhs}; + const exprt new_full_lhs = add_to_lhs(full_lhs, lhs); symex_assign_rec( state, lhs_array, new_full_lhs, new_rhs, guard, assignment_type); From eb83306e8459edb65cfd646777e10292c93da8ac Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 29 May 2019 10:03:30 +0100 Subject: [PATCH 4/8] Add an SSA_assignment_stept class with constructor Without this, it is not clear what are the fields of SSA_stept which are required to describe an assignement. --- src/goto-symex/ssa_step.cpp | 22 +++++++++++++++++++ src/goto-symex/ssa_step.h | 15 +++++++++++++ src/goto-symex/symex_target_equation.cpp | 28 +++++++++++------------- 3 files changed, 50 insertions(+), 15 deletions(-) diff --git a/src/goto-symex/ssa_step.cpp b/src/goto-symex/ssa_step.cpp index 24f29942125..3deac1253ac 100644 --- a/src/goto-symex/ssa_step.cpp +++ b/src/goto-symex/ssa_step.cpp @@ -213,3 +213,25 @@ irep_idt SSA_stept::get_property_id() const return property_id; } + +SSA_assignment_stept::SSA_assignment_stept( + symex_targett::sourcet source, + exprt _guard, + ssa_exprt _ssa_lhs, + exprt _ssa_full_lhs, + exprt _original_full_lhs, + exprt _ssa_rhs, + exprt _cond_expr, + symex_targett::assignment_typet _assignment_type, + bool _hidden) + : SSA_stept(source, goto_trace_stept::typet::ASSIGNMENT) +{ + guard = std::move(_guard); + ssa_lhs = std::move(_ssa_lhs); + ssa_full_lhs = std::move(_ssa_full_lhs); + original_full_lhs = std::move(_original_full_lhs); + ssa_rhs = std::move(_ssa_rhs); + assignment_type = _assignment_type; + cond_expr = std::move(_cond_expr); + hidden = _hidden; +} diff --git a/src/goto-symex/ssa_step.h b/src/goto-symex/ssa_step.h index 386c1adac2d..84bcbe92642 100644 --- a/src/goto-symex/ssa_step.h +++ b/src/goto-symex/ssa_step.h @@ -195,4 +195,19 @@ class SSA_stept void validate(const namespacet &ns, const validation_modet vm) const; }; +class SSA_assignment_stept : public SSA_stept +{ +public: + SSA_assignment_stept( + symex_targett::sourcet source, + exprt guard, + ssa_exprt ssa_lhs, + exprt ssa_full_lhs, + exprt original_full_lhs, + exprt ssa_rhs, + exprt cond_expr, + symex_targett::assignment_typet assignment_type, + bool hidden); +}; + #endif // CPROVER_GOTO_SYMEX_SSA_STEP_H diff --git a/src/goto-symex/symex_target_equation.cpp b/src/goto-symex/symex_target_equation.cpp index 9d04578b48c..affa572a95e 100644 --- a/src/goto-symex/symex_target_equation.cpp +++ b/src/goto-symex/symex_target_equation.cpp @@ -114,21 +114,19 @@ void symex_target_equationt::assignment( { PRECONDITION(ssa_lhs.is_not_nil()); - SSA_steps.emplace_back(source, goto_trace_stept::typet::ASSIGNMENT); - SSA_stept &SSA_step=SSA_steps.back(); - - SSA_step.guard=guard; - SSA_step.ssa_lhs=ssa_lhs; - SSA_step.ssa_full_lhs=ssa_full_lhs; - SSA_step.original_full_lhs=original_full_lhs; - SSA_step.ssa_rhs=ssa_rhs; - SSA_step.assignment_type=assignment_type; - - SSA_step.cond_expr=equal_exprt(SSA_step.ssa_lhs, SSA_step.ssa_rhs); - SSA_step.hidden=(assignment_type!=assignment_typet::STATE && - assignment_type!=assignment_typet::VISIBLE_ACTUAL_PARAMETER); - - merge_ireps(SSA_step); + SSA_steps.emplace_back(SSA_assignment_stept{ + source, + guard, + ssa_lhs, + ssa_full_lhs, + original_full_lhs, + ssa_rhs, + equal_exprt(ssa_lhs, ssa_rhs), + assignment_type, + assignment_type != assignment_typet::STATE && + assignment_type != assignment_typet::VISIBLE_ACTUAL_PARAMETER}); + + merge_ireps(SSA_steps.back()); } void symex_target_equationt::decl( From 5119a018e14f0a17989de383627b4395cb28574f Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 29 May 2019 10:28:25 +0100 Subject: [PATCH 5/8] Move make_and to expr_util This can be useful in other modules than BDDs. --- src/solvers/prop/bdd_expr.cpp | 12 ------------ src/util/expr_util.cpp | 10 ++++++++++ src/util/expr_util.h | 4 ++++ 3 files changed, 14 insertions(+), 12 deletions(-) diff --git a/src/solvers/prop/bdd_expr.cpp b/src/solvers/prop/bdd_expr.cpp index 64db506c640..ecdeb6507c9 100644 --- a/src/solvers/prop/bdd_expr.cpp +++ b/src/solvers/prop/bdd_expr.cpp @@ -91,18 +91,6 @@ bddt bdd_exprt::from_expr(const exprt &expr) return from_expr_rec(expr); } -/// Conjunction of two expressions. If the second is already an `and_exprt` -/// add to its operands instead of creating a new expression. -static exprt make_and(exprt a, exprt b) -{ - if(b.id() == ID_and) - { - b.add_to_operands(std::move(a)); - return b; - } - return and_exprt{std::move(a), std::move(b)}; -} - /// Disjunction of two expressions. If the second is already an `or_exprt` /// add to its operands instead of creating a new expression. static exprt make_or(exprt a, exprt b) diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index 85f3534667a..3cbe5c9165c 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -289,3 +289,13 @@ constant_exprt make_boolean_expr(bool value) else return false_exprt(); } + +exprt make_and(exprt a, exprt b) +{ + if(b.id() == ID_and) + { + b.add_to_operands(std::move(a)); + return b; + } + return and_exprt{std::move(a), std::move(b)}; +} diff --git a/src/util/expr_util.h b/src/util/expr_util.h index e669e457b0f..d82e48298c5 100644 --- a/src/util/expr_util.h +++ b/src/util/expr_util.h @@ -100,4 +100,8 @@ class is_constantt /// returns true_exprt if given true and false_exprt otherwise constant_exprt make_boolean_expr(bool); +/// Conjunction of two expressions. If the second is already an `and_exprt` +/// add to its operands instead of creating a new expression. +exprt make_and(exprt a, exprt b); + #endif // CPROVER_UTIL_EXPR_UTIL_H From 070cef9d813bb5a760d884b67d16fa0c277d7a93 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 29 May 2019 10:52:38 +0100 Subject: [PATCH 6/8] Avoid modifying guard argument in symex assign This allows guard to be constant in the signatures which makes it explicit that it is left unmodified by the function. --- src/goto-symex/goto_symex.h | 4 ++-- src/goto-symex/symex_assign.cpp | 14 ++++++-------- 2 files changed, 8 insertions(+), 10 deletions(-) diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h index 7b5fe4af8d8..12be632efb2 100644 --- a/src/goto-symex/goto_symex.h +++ b/src/goto-symex/goto_symex.h @@ -557,14 +557,14 @@ class goto_symext const ssa_exprt &lhs, const exprt &full_lhs, const struct_exprt &rhs, - exprt::operandst &, + const exprt::operandst &, assignment_typet); void symex_assign_symbol( statet &, const ssa_exprt &lhs, const exprt &full_lhs, const exprt &rhs, - exprt::operandst &, + const exprt::operandst &, assignment_typet); void symex_assign_typecast( statet &, diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index 3843e960af8..b0320f1bc22 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -391,7 +392,7 @@ void goto_symext::symex_assign_from_struct( const ssa_exprt &lhs, // L1 const exprt &full_lhs, const struct_exprt &rhs, - exprt::operandst &guard, + const exprt::operandst &guard, assignment_typet assignment_type) { const struct_typet &type = to_struct_type(ns.follow(lhs.type())); @@ -423,7 +424,7 @@ void goto_symext::symex_assign_symbol( const ssa_exprt &lhs, // L1 const exprt &full_lhs, const exprt &rhs, - exprt::operandst &guard, + const exprt::operandst &guard, assignment_typet assignment_type) { // Shortcut the common case of a whole-struct initializer: @@ -485,12 +486,12 @@ void goto_symext::symex_assign_symbol( << messaget::eom; }); - // Temporarily add the state guard - guard.emplace_back(state.guard.as_expr()); + const exprt assignment_guard = + make_and(state.guard.as_expr(), conjunction(guard)); const exprt original_lhs = get_original_name(l2_full_lhs); target.assignment( - conjunction(guard), + assignment_guard, l2_lhs, l2_full_lhs, original_lhs, @@ -509,9 +510,6 @@ void goto_symext::symex_assign_symbol( state.propagation.erase_if_exists(l1_lhs.get_identifier()); state.value_set.erase_symbol(l1_lhs, ns); } - - // Restore the guard - guard.pop_back(); } void goto_symext::symex_assign_typecast( From 8391c1716214c8860866373a39b520201c2708da Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Wed, 29 May 2019 11:08:16 +0100 Subject: [PATCH 7/8] Add missing const --- src/goto-symex/symex_assign.cpp | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp index b0320f1bc22..2be9a9262cf 100644 --- a/src/goto-symex/symex_assign.cpp +++ b/src/goto-symex/symex_assign.cpp @@ -457,16 +457,16 @@ void goto_symext::symex_assign_symbol( do_simplify(assignment.rhs); - ssa_exprt &l1_lhs = assignment.lhs; - ssa_exprt l2_lhs = state - .assignment( - assignment.lhs, - assignment.rhs, - ns, - symex_config.simplify_opt, - symex_config.constant_propagation, - symex_config.allow_pointer_unsoundness) - .get(); + const ssa_exprt &l1_lhs = assignment.lhs; + const ssa_exprt l2_lhs = state + .assignment( + assignment.lhs, + assignment.rhs, + ns, + symex_config.simplify_opt, + symex_config.constant_propagation, + symex_config.allow_pointer_unsoundness) + .get(); exprt ssa_full_lhs = add_to_lhs(full_lhs, l2_lhs); state.record_events.push(false); From 63e01d9bf47bc49a3f4231927db3c6f5a0b51662 Mon Sep 17 00:00:00 2001 From: Romain Brenguier Date: Fri, 31 May 2019 11:31:28 +0100 Subject: [PATCH 8/8] make_and simplifies trivial expressions This is to avoid generating expressions like TRUE && TRUE --- src/util/expr_util.cpp | 13 +++++++++++++ src/util/expr_util.h | 3 ++- 2 files changed, 15 insertions(+), 1 deletion(-) diff --git a/src/util/expr_util.cpp b/src/util/expr_util.cpp index 3cbe5c9165c..de980d2c56e 100644 --- a/src/util/expr_util.cpp +++ b/src/util/expr_util.cpp @@ -292,6 +292,19 @@ constant_exprt make_boolean_expr(bool value) exprt make_and(exprt a, exprt b) { + PRECONDITION(a.type().id() == ID_bool && b.type().id() == ID_bool); + if(b.is_constant()) + { + if(b.get(ID_value) == ID_false) + return false_exprt{}; + return a; + } + if(a.is_constant()) + { + if(a.get(ID_value) == ID_false) + return false_exprt{}; + return b; + } if(b.id() == ID_and) { b.add_to_operands(std::move(a)); diff --git a/src/util/expr_util.h b/src/util/expr_util.h index d82e48298c5..cd798fd04a0 100644 --- a/src/util/expr_util.h +++ b/src/util/expr_util.h @@ -101,7 +101,8 @@ class is_constantt constant_exprt make_boolean_expr(bool); /// Conjunction of two expressions. If the second is already an `and_exprt` -/// add to its operands instead of creating a new expression. +/// add to its operands instead of creating a new expression. If one is `true`, +/// return the other expression. If one is `false` returns `false`. exprt make_and(exprt a, exprt b); #endif // CPROVER_UTIL_EXPR_UTIL_H