Merge pull request #3966 from tautschnig/reinstate-limited-symex-renaming
Reinstate limited symex renaming [blocks: #4164]
This commit is contained in:
commit
b43753a12b
|
@ -0,0 +1,30 @@
|
|||
#include <assert.h>
|
||||
|
||||
int main(int argc, char *argv[])
|
||||
{
|
||||
unsigned char x = argc;
|
||||
// make sure int multiplication below won't overflow - type casting to
|
||||
// unsigned long long would be possible, but puts yields a challenging problem
|
||||
// for the SAT solver
|
||||
__CPROVER_assume(x < 1ULL << (sizeof(int) * 8 / 2 - 1));
|
||||
|
||||
struct S
|
||||
{
|
||||
int a;
|
||||
int b[x];
|
||||
int c;
|
||||
};
|
||||
|
||||
if(x % 2 == 0)
|
||||
x = 3;
|
||||
|
||||
struct S s[x];
|
||||
|
||||
__CPROVER_assume(x < 255);
|
||||
++x;
|
||||
|
||||
assert(sizeof(struct S) == ((unsigned char)argc + 2) * sizeof(int));
|
||||
assert(sizeof(s) == (x - 1) * ((unsigned char)argc + 2) * sizeof(int));
|
||||
|
||||
return 0;
|
||||
}
|
|
@ -0,0 +1,12 @@
|
|||
CORE
|
||||
main.c
|
||||
--program-only
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
--
|
||||
^warning: ignoring
|
||||
--
|
||||
\(__CPROVER_size_t\)x\$array_size
|
||||
--
|
||||
There should not be any type cast of x$array_size to __CPROVER_size_t, because
|
||||
it already is of that type.
|
|
@ -0,0 +1,8 @@
|
|||
CORE
|
||||
main.c
|
||||
|
||||
^EXIT=0$
|
||||
^SIGNAL=0$
|
||||
^VERIFICATION SUCCESSFUL$
|
||||
--
|
||||
^warning: ignoring
|
|
@ -16,6 +16,7 @@ Author: Daniel Kroening, kroening@kroening.com
|
|||
#include <util/arith_tools.h>
|
||||
#include <util/c_types.h>
|
||||
#include <util/config.h>
|
||||
#include <util/fresh_symbol.h>
|
||||
#include <util/mathematical_types.h>
|
||||
#include <util/pointer_offset_size.h>
|
||||
#include <util/simplify_expr.h>
|
||||
|
@ -614,41 +615,25 @@ void c_typecheck_baset::typecheck_array_type(array_typet &type)
|
|||
throw 0;
|
||||
}
|
||||
|
||||
// Need to pull out! We insert new symbol.
|
||||
unsigned count = 0;
|
||||
irep_idt temp_identifier;
|
||||
std::string suffix;
|
||||
|
||||
do
|
||||
{
|
||||
suffix = "$array_size" + std::to_string(count);
|
||||
temp_identifier = id2string(current_symbol.name) + suffix;
|
||||
count++;
|
||||
} while(symbol_table.symbols.find(temp_identifier) !=
|
||||
symbol_table.symbols.end());
|
||||
|
||||
// add the symbol to symbol table
|
||||
auxiliary_symbolt new_symbol;
|
||||
new_symbol.name = temp_identifier;
|
||||
new_symbol.pretty_name = id2string(current_symbol.pretty_name) + suffix;
|
||||
new_symbol.base_name = id2string(current_symbol.base_name) + suffix;
|
||||
new_symbol.type = size.type();
|
||||
symbolt &new_symbol = get_fresh_aux_symbol(
|
||||
size_type(),
|
||||
id2string(current_symbol.name) + "$array_size",
|
||||
id2string(current_symbol.base_name) + "$array_size",
|
||||
size_source_location,
|
||||
mode,
|
||||
symbol_table);
|
||||
new_symbol.type.set(ID_C_constant, true);
|
||||
new_symbol.value = size;
|
||||
new_symbol.location = size_source_location;
|
||||
new_symbol.mode = mode;
|
||||
|
||||
symbol_table.add(new_symbol);
|
||||
new_symbol.value = typecast_exprt::conditional_cast(size, size_type());
|
||||
|
||||
// produce the code that declares and initializes the symbol
|
||||
symbol_exprt symbol_expr(temp_identifier, new_symbol.type);
|
||||
symbol_exprt symbol_expr = new_symbol.symbol_expr();
|
||||
|
||||
code_declt declaration(symbol_expr);
|
||||
declaration.add_source_location() = size_source_location;
|
||||
|
||||
code_assignt assignment;
|
||||
assignment.lhs()=symbol_expr;
|
||||
assignment.rhs() = size;
|
||||
assignment.rhs() = new_symbol.value;
|
||||
assignment.add_source_location() = size_source_location;
|
||||
|
||||
// store the code
|
||||
|
|
|
@ -611,12 +611,70 @@ void goto_symex_statet::rename_address(
|
|||
}
|
||||
}
|
||||
|
||||
/// Return true if, and only if, the \p type or one of its subtypes requires SSA
|
||||
/// renaming. Renaming is necessary when symbol expressions occur within the
|
||||
/// type, which is the case for arrays of non-constant size.
|
||||
static bool requires_renaming(const typet &type, const namespacet &ns)
|
||||
{
|
||||
if(type.id() == ID_array)
|
||||
{
|
||||
const auto &array_type = to_array_type(type);
|
||||
return requires_renaming(array_type.subtype(), ns) ||
|
||||
!array_type.size().is_constant();
|
||||
}
|
||||
else if(
|
||||
type.id() == ID_struct || type.id() == ID_union || type.id() == ID_class)
|
||||
{
|
||||
const struct_union_typet &s_u_type = to_struct_union_type(type);
|
||||
const struct_union_typet::componentst &components = s_u_type.components();
|
||||
|
||||
for(auto &component : components)
|
||||
{
|
||||
// be careful, or it might get cyclic
|
||||
if(
|
||||
component.type().id() != ID_pointer &&
|
||||
requires_renaming(component.type(), ns))
|
||||
{
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
||||
return false;
|
||||
}
|
||||
else if(type.id() == ID_pointer)
|
||||
{
|
||||
return requires_renaming(to_pointer_type(type).subtype(), ns);
|
||||
}
|
||||
else if(type.id() == ID_symbol_type)
|
||||
{
|
||||
const symbolt &symbol = ns.lookup(to_symbol_type(type));
|
||||
return requires_renaming(symbol.type, ns);
|
||||
}
|
||||
else if(type.id() == ID_union_tag)
|
||||
{
|
||||
const symbolt &symbol = ns.lookup(to_union_tag_type(type));
|
||||
return requires_renaming(symbol.type, ns);
|
||||
}
|
||||
else if(type.id() == ID_struct_tag)
|
||||
{
|
||||
const symbolt &symbol = ns.lookup(to_struct_tag_type(type));
|
||||
return requires_renaming(symbol.type, ns);
|
||||
}
|
||||
|
||||
return false;
|
||||
}
|
||||
|
||||
void goto_symex_statet::rename(
|
||||
typet &type,
|
||||
const irep_idt &l1_identifier,
|
||||
const namespacet &ns,
|
||||
levelt level)
|
||||
{
|
||||
// check whether there are symbol expressions in the type; if not, there
|
||||
// is no need to expand the struct/union tags in the type
|
||||
if(!requires_renaming(type, ns))
|
||||
return; // no action
|
||||
|
||||
// rename all the symbols with their last known value
|
||||
// to the given level
|
||||
|
||||
|
|
Loading…
Reference in New Issue