Replace use of #ifdef by template parameter in symex_assign #4840
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -22,6 +22,15 @@ Author: Daniel Kroening, [email protected] | |
| // update_exprt. | ||
| // #define USE_UPDATE | ||
|
|
||
| constexpr bool use_update() | ||
| { | ||
| #ifdef USE_UPDATE | ||
| return true; | ||
| #else | ||
| return false; | ||
| #endif | ||
| } | ||
|
|
||
| /// 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. | ||
|
|
@@ -71,12 +80,15 @@ void symex_assignt::assign_rec( | |
| assign_symbol(to_ssa_expr(lhs), full_lhs, rhs, guard); | ||
| } | ||
| else if(lhs.id() == ID_index) | ||
| assign_array<use_update()>(to_index_expr(lhs), full_lhs, rhs, guard); | ||
| else if(lhs.id()==ID_member) | ||
| { | ||
| const typet &type = to_member_expr(lhs).struct_op().type(); | ||
| if(type.id() == ID_struct || type.id() == ID_struct_tag) | ||
| { | ||
| assign_struct_member<use_update()>( | ||
| to_member_expr(lhs), full_lhs, rhs, guard); | ||
| } | ||
| else if(type.id() == ID_union || type.id() == ID_union_tag) | ||
| { | ||
| // should have been replaced by byte_extract | ||
|
|
@@ -147,92 +159,102 @@ struct assignmentt final | |
| /// \ref symex_assignt::assign_struct_member have done, but now making use | ||
| /// of the index/member that may only be known after renaming to L2 has taken | ||
| /// place. | ||
| /// \tparam use_update: use update_exprt instead of with_exprt when building | ||
| /// expressions that modify components of an array or a struct | ||
| /// \param [in, out] state: symbolic execution state to perform renaming | ||
| /// \param assignment: an assignment to rewrite | ||
| /// \param ns: namespace | ||
| /// \return the updated assignment | ||
| template <bool use_update> | ||
| static assignmentt rewrite_with_to_field_symbols( | ||
| goto_symext::statet &state, | ||
| assignmentt assignment, | ||
| const namespacet &ns) | ||
| { | ||
| exprt &ssa_rhs = assignment.rhs; | ||
| ssa_exprt &lhs_mod = assignment.lhs; | ||
| if(use_update) | ||
| { | ||
| while(ssa_rhs.id() == ID_update && | ||
| to_update_expr(ssa_rhs).designator().size() == 1 && | ||
| (lhs_mod.type().id() == ID_array || | ||
| lhs_mod.type().id() == ID_struct || | ||
| lhs_mod.type().id() == ID_struct_tag)) | ||
| { | ||
| exprt field_sensitive_lhs; | ||
| const update_exprt &update = to_update_expr(ssa_rhs); | ||
| PRECONDITION(update.designator().size() == 1); | ||
| const exprt &designator = update.designator().front(); | ||
|
|
||
| if(lhs_mod.type().id() == ID_array) | ||
| { | ||
| field_sensitive_lhs = | ||
| index_exprt(lhs_mod, to_index_designator(designator).index()); | ||
| } | ||
| else | ||
| { | ||
| field_sensitive_lhs = member_exprt( | ||
| lhs_mod, | ||
| to_member_designator(designator).get_component_name(), | ||
| update.new_value().type()); | ||
| } | ||
|
|
||
| state.field_sensitivity.apply(ns, state, field_sensitive_lhs, true); | ||
|
|
||
| if(field_sensitive_lhs.id() != ID_symbol) | ||
| break; | ||
|
|
||
| ssa_rhs = update.new_value(); | ||
| lhs_mod = to_ssa_expr(field_sensitive_lhs); | ||
| } | ||
| } | ||
| else | ||
| { | ||
| while( | ||
| ssa_rhs.id() == ID_with && to_with_expr(ssa_rhs).operands().size() == 3 && | ||
| (lhs_mod.type().id() == ID_array || lhs_mod.type().id() == ID_struct || | ||
| lhs_mod.type().id() == ID_struct_tag)) | ||
| { | ||
| exprt field_sensitive_lhs; | ||
| const with_exprt &with_expr = to_with_expr(ssa_rhs); | ||
|
|
||
| if(lhs_mod.type().id() == ID_array) | ||
| { | ||
| field_sensitive_lhs = index_exprt(lhs_mod, with_expr.where()); | ||
| } | ||
| else | ||
| { | ||
| field_sensitive_lhs = member_exprt( | ||
| lhs_mod, | ||
| with_expr.where().get(ID_component_name), | ||
| with_expr.new_value().type()); | ||
| } | ||
|
|
||
| field_sensitive_lhs = state.field_sensitivity.apply( | ||
| ns, state, std::move(field_sensitive_lhs), true); | ||
|
|
||
| if(field_sensitive_lhs.id() != ID_symbol) | ||
| break; | ||
|
|
||
| ssa_rhs = with_expr.new_value(); | ||
| lhs_mod = to_ssa_expr(field_sensitive_lhs); | ||
| } | ||
| } | ||
| return assignment; | ||
| } | ||
|
|
||
| /// Replace byte-update operations that only affect individual fields of an | ||
| /// expression by assignments to just those fields. May generate "with" (or | ||
| /// "update") expressions, which \ref rewrite_with_to_field_symbols will then | ||
| /// take care of. | ||
| /// \tparam use_update: use update_exprt instead of with_exprt when building | ||
| /// expressions that modify components of an array or a struct | ||
| /// \param [in, out] state: symbolic execution state to perform renaming | ||
| /// \param assignment: assignment to transform | ||
| /// \param ns: namespace | ||
| /// \param do_simplify: set to true if, and only if, simplification is enabled | ||
| /// \return updated assignment | ||
| template <bool use_update> | ||
| static assignmentt shift_indexed_access_to_lhs( | ||
| goto_symext::statet &state, | ||
| assignmentt assignment, | ||
|
|
@@ -269,31 +291,38 @@ static assignmentt shift_indexed_access_to_lhs( | |
| if(byte_extract.id() == ID_index) | ||
| { | ||
| index_exprt &idx = to_index_expr(byte_extract); | ||
| ssa_rhs = [&]() -> exprt { | ||
| if(use_update) | ||
| { | ||
| update_exprt new_rhs{idx.array(), exprt{}, ssa_rhs}; | ||
| new_rhs.designator().push_back(index_designatort{idx.index()}); | ||
| return std::move(new_rhs); | ||
| } | ||
| else | ||
| return with_exprt{idx.array(), idx.index(), ssa_rhs}; | ||
| }(); | ||
| byte_extract = idx.array(); | ||
| } | ||
| else | ||
| { | ||
| member_exprt &member = to_member_expr(byte_extract); | ||
| const irep_idt &component_name = member.get_component_name(); | ||
| ssa_rhs = [&]() -> exprt { | ||
| if(use_update) | ||
| { | ||
| update_exprt new_rhs{member.compound(), exprt{}, ssa_rhs}; | ||
| new_rhs.designator().push_back( | ||
| member_designatort{component_name}); | ||
| return std::move(new_rhs); | ||
| } | ||
| else | ||
| { | ||
| with_exprt new_rhs( | ||
| member.compound(), exprt(ID_member_name), ssa_rhs); | ||
| new_rhs.where().set(ID_component_name, component_name); | ||
| return std::move(new_rhs); | ||
| } | ||
| }(); | ||
|
There was a problem hiding this comment. Again, no idea why a lambda is the right thing here? |
||
| byte_extract = member.compound(); | ||
| } | ||
| } | ||
|
|
@@ -361,9 +390,10 @@ void symex_assignt::assign_non_struct_symbol( | |
| // introduced by assign_struct_member, are transformed into member | ||
| // expressions on the LHS. If we add an option to disable field-sensitivity | ||
| // in the future these should be omitted. | ||
| auto assignment = shift_indexed_access_to_lhs<use_update()>( | ||
| state, assignmentt{lhs, std::move(l2_rhs)}, ns, symex_config.simplify_opt); | ||
| assignment = rewrite_with_to_field_symbols<use_update()>( | ||
| state, std::move(assignment), ns); | ||
|
|
||
| if(symex_config.simplify_opt) | ||
| assignment.rhs = simplify_expr(std::move(assignment.rhs), ns); | ||
|
|
@@ -437,6 +467,7 @@ void symex_assignt::assign_typecast( | |
| assign_rec(lhs.op(), new_full_lhs, rhs_typecasted, guard); | ||
| } | ||
|
|
||
| template <bool use_update> | ||
| void symex_assignt::assign_array( | ||
| const index_exprt &lhs, | ||
| const exprt &full_lhs, | ||
|
|
@@ -449,36 +480,29 @@ void symex_assignt::assign_array( | |
|
|
||
| PRECONDITION(lhs_index_type.id() == ID_array); | ||
|
|
||
| if(use_update) | ||
| { | ||
| // turn | ||
| // a[i]=e | ||
| // into | ||
| // a'==UPDATE(a, [i], e) | ||
| const update_exprt new_rhs{lhs_array, index_designatort(lhs_index), rhs}; | ||
| const exprt new_full_lhs = add_to_lhs(full_lhs, lhs); | ||
| assign_rec(lhs_array, new_full_lhs, new_rhs, guard); | ||
| } | ||
| else | ||
| { | ||
| // turn | ||
| // a[i]=e | ||
| // into | ||
| // a'==a WITH [i:=e] | ||
| const with_exprt new_rhs{lhs_array, lhs_index, rhs}; | ||
| const exprt new_full_lhs = add_to_lhs(full_lhs, lhs); | ||
| assign_rec(lhs_array, new_full_lhs, new_rhs, guard); | ||
| } | ||
| } | ||
|
|
||
| template <bool use_update> | ||
| void symex_assignt::assign_struct_member( | ||
| const member_exprt &lhs, | ||
| const exprt &full_lhs, | ||
|
|
@@ -514,35 +538,30 @@ void symex_assignt::assign_struct_member( | |
|
|
||
| const irep_idt &component_name=lhs.get_component_name(); | ||
|
|
||
| if(use_update) | ||
| { | ||
| // turn | ||
| // a.c=e | ||
| // into | ||
| // a'==UPDATE(a, .c, e) | ||
| const update_exprt new_rhs{ | ||
| lhs_struct, member_designatort(component_name), rhs}; | ||
| const exprt new_full_lhs = add_to_lhs(full_lhs, lhs); | ||
| assign_rec(lhs_struct, new_full_lhs, new_rhs, guard); | ||
| } | ||
| else | ||
| { | ||
| // turn | ||
| // a.c=e | ||
| // into | ||
| // a'==a WITH [c:=e] | ||
|
|
||
| with_exprt new_rhs(lhs_struct, exprt(ID_member_name), rhs); | ||
| new_rhs.where().set(ID_component_name, component_name); | ||
|
|
||
| exprt new_full_lhs = add_to_lhs(full_lhs, lhs); | ||
| assign_rec(lhs_struct, new_full_lhs, new_rhs, guard); | ||
| } | ||
| } | ||
|
|
||
| void symex_assignt::assign_if( | ||
|
|
||
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't get the point of this lambda function?!
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This is to make clear that this part of the code is just to find the new value of ssa_rhs. The alternative is to have directly an
ifstatement and we wouldn't know what it's mutating without looking at the code inside the branches.