bv_get_rec: ensure all expressions are properly typed #7020
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 |
|---|---|---|
| @@ -0,0 +1,12 @@ | ||
| struct S | ||
| { | ||
| int x; | ||
| }; | ||
|
|
||
| int main() | ||
| { | ||
| unsigned size; | ||
| __CPROVER_assume(size > 0); | ||
| struct S array[size]; | ||
| __CPROVER_assert(array[0].x == 0, "not always zero"); | ||
| } |
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 |
|---|---|---|
| @@ -0,0 +1,10 @@ | ||
| CORE | ||
| main.c | ||
| --trace | ||
| ^VERIFICATION FAILED$ | ||
| ^EXIT=10$ | ||
| ^SIGNAL=0$ | ||
| -- | ||
| ^Invariant check failed | ||
| -- | ||
| This test requires that bv_get_rec always uses properly typed expressions. |
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
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 |
|---|---|---|
|
|
@@ -6,17 +6,18 @@ Author: Daniel Kroening, [email protected] | |
|
|
||
| \*******************************************************************/ | ||
|
|
||
| #include <util/arith_tools.h> | ||
| #include <util/c_types.h> | ||
| #include <util/namespace.h> | ||
| #include <util/simplify_expr.h> | ||
| #include <util/std_expr.h> | ||
| #include <util/threeval.h> | ||
|
|
||
| #include "boolbv.h" | ||
| #include "boolbv_type.h" | ||
|
|
||
| #include <iostream> | ||
|
|
||
| exprt boolbvt::get(const exprt &expr) const | ||
| { | ||
| if(expr.id()==ID_symbol || | ||
|
|
@@ -33,21 +34,26 @@ exprt boolbvt::get(const exprt &expr) const | |
| // the value of clock symbols, which do not have a fixed type as the clock | ||
| // type is computed during symbolic execution) or match the type stored in | ||
| // the mapping | ||
| if(expr.type() == map_entry.type) | ||
| return bv_get_rec(expr, map_entry.literal_map, 0); | ||
| else | ||
| { | ||
| PRECONDITION(expr.type() == typet{}); | ||
| exprt skeleton = expr; | ||
| skeleton.type() = map_entry.type; | ||
| return bv_get_rec(skeleton, map_entry.literal_map, 0); | ||
| } | ||
| } | ||
| } | ||
|
|
||
| return SUB::get(expr); | ||
| } | ||
|
|
||
| exprt boolbvt::bv_get_rec(const exprt &expr, const bvt &bv, std::size_t offset) | ||
| const | ||
| { | ||
| const typet &type = expr.type(); | ||
|
|
||
| if(type.id()==ID_bool) | ||
| { | ||
| PRECONDITION(bv.size() > offset); | ||
|
|
@@ -91,7 +97,7 @@ exprt boolbvt::bv_get_rec( | |
| const index_exprt index{ | ||
| expr, | ||
| from_integer(new_offset / sub_width, array_type.index_type())}; | ||
| op.push_back(bv_get_rec(index, bv, offset + new_offset)); | ||
| } | ||
|
|
||
| exprt dest=exprt(ID_array, type); | ||
|
|
@@ -103,24 +109,12 @@ exprt boolbvt::bv_get_rec( | |
| return array_exprt{{}, array_type}; | ||
| } | ||
| } | ||
| else if(type.id() == ID_struct || type.id() == ID_struct_tag) | ||
| { | ||
| const struct_typet::componentst &components = | ||
| type.id() == ID_struct | ||
| ? to_struct_type(type).components() | ||
| : ns.follow_tag(to_struct_tag_type(type)).components(); | ||
| std::size_t new_offset=0; | ||
| exprt::operandst op; | ||
| op.reserve(components.size()); | ||
|
|
@@ -130,17 +124,19 @@ exprt boolbvt::bv_get_rec( | |
| const typet &subtype = c.type(); | ||
|
|
||
| const member_exprt member{expr, c.get_name(), subtype}; | ||
| op.push_back(bv_get_rec(member, bv, offset + new_offset)); | ||
|
|
||
| new_offset += boolbv_width(subtype); | ||
| } | ||
|
|
||
| return struct_exprt(std::move(op), type); | ||
| } | ||
| else if(type.id() == ID_union || type.id() == ID_union_tag) | ||
| { | ||
| const union_typet::componentst &components = | ||
| type.id() == ID_union | ||
| ? to_union_type(type).components() | ||
| : ns.follow_tag(to_union_tag_type(type)).components(); | ||
|
|
||
| if(components.empty()) | ||
| return empty_union_exprt(type); | ||
|
|
@@ -154,8 +150,8 @@ exprt boolbvt::bv_get_rec( | |
| expr, components[component_nr].get_name(), subtype}; | ||
| return union_exprt( | ||
| components[component_nr].get_name(), | ||
| bv_get_rec(member, bv, offset), | ||
| type); | ||
| } | ||
| else if(type.id()==ID_vector) | ||
| { | ||
|
|
@@ -176,8 +172,7 @@ exprt boolbvt::bv_get_rec( | |
| { | ||
| const index_exprt index{expr, | ||
| from_integer(i, vector_type.index_type())}; | ||
| value.operands().push_back(bv_get_rec(index, bv, i * element_width)); | ||
| } | ||
|
|
||
| return std::move(value); | ||
|
|
@@ -195,8 +190,8 @@ exprt boolbvt::bv_get_rec( | |
| "complex type has two elements of equal bit width"); | ||
|
|
||
| return complex_exprt{ | ||
| bv_get_rec(complex_real_exprt{expr}, bv, 0 * sub_width), | ||
| bv_get_rec(complex_imag_exprt{expr}, bv, 1 * sub_width), | ||
| to_complex_type(type)}; | ||
| } | ||
| } | ||
|
|
@@ -274,7 +269,9 @@ exprt boolbvt::bv_get_rec( | |
|
|
||
| exprt boolbvt::bv_get(const bvt &bv, const typet &type) const | ||
|
There was a problem hiding this comment. Can we get rid of this method? There was a problem hiding this comment. Not unless we get rid of |
||
| { | ||
| nil_exprt skeleton; | ||
| skeleton.type() = type; | ||
| return bv_get_rec(skeleton, bv, 0); | ||
| } | ||
|
|
||
| exprt boolbvt::bv_get_cache(const exprt &expr) const | ||
|
|
||
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
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
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.
This gives me lots of "I don't think types are supposed to work like that" feelings. But I recognise that this is an improvement on what is there and not what the patch is addressing.