replica
/
diffblue-cbmc
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

check type of index operand 

git-svn-id: svn+ssh://svn.cprover.org/srv/svn/cbmc/trunk@3410 6afb6bc1-c8e4-404c-8f48-9ae832c5b171
This commit is contained in:
kroening 2014-01-11 15:44:29 +00:00
parent e578e410f6
commit 10eaa133b4
1 changed files with 117 additions and 110 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

209
src/solvers/flattening/boolbv_index.cpp
View File

@ -37,130 +37,137 @@ void boolbvt::convert_index(const index_exprt &expr, bvt &bv)
const exprt &array=expr.array();
const exprt &index=expr.index();
const array_typet &array_type=
to_array_type(ns.follow(array.type()));
const typet &array_op_type=ns.follow(array.type());
// see if the array size is constant
if(is_unbounded_array(array_type))
if(array_op_type.id()==ID_array)
{
// use array decision procedure
const array_typet &array_type=
to_array_type(array_op_type);
// see if the array size is constant
if(is_unbounded_array(array_type))
{
// use array decision procedure
unsigned width=boolbv_width(expr.type());
if(width==0)
return conversion_failed(expr, bv);
// free variables
bv.resize(width);
for(unsigned i=0; i<width; i++)
bv[i]=prop.new_variable();
record_array_index(expr);
// record type if array is a symbol
if(array.id()==ID_symbol)
map.get_map_entry(
to_symbol_expr(array).get_identifier(), array_type);
// make sure we have the index in the cache
convert_bv(index);
return;
}
// see if the index address is constant
mp_integer index_value;
if(!to_integer(index, index_value))
return convert_index(array, index_value, bv);
unsigned width=boolbv_width(expr.type());
if(width==0)
return conversion_failed(expr, bv);
// free variables
bv.resize(width);
for(unsigned i=0; i<width; i++)
bv[i]=prop.new_variable();
record_array_index(expr);
// record type if array is a symbol
if(array.id()==ID_symbol)
map.get_map_entry(
to_symbol_expr(array).get_identifier(), array_type);
// make sure we have the index in the cache
convert_bv(index);
return;
}
// see if the index address is constant
mp_integer index_value;
if(!to_integer(index, index_value))
return convert_index(array, index_value, bv);
unsigned width=boolbv_width(expr.type());
if(width==0)
return conversion_failed(expr, bv);
mp_integer array_size;
if(to_integer(array_type.size(), array_size))
{
std::cout << to_array_type(array.type()).size().pretty() << std::endl;
throw "failed to convert array size";
}
// get literals for the whole array
const bvt &array_bv=convert_bv(array);
if(array_size*width!=array_bv.size())
throw "unexpected array size";
// TODO: maybe a shifter-like construction would be better
if(prop.has_set_to())
{
// free variables
bv.resize(width);
for(unsigned i=0; i<width; i++)
bv[i]=prop.new_variable();
// add implications
equal_exprt index_equality;
index_equality.lhs()=index; // index operand
bvt equal_bv;
equal_bv.resize(width);
for(mp_integer i=0; i<array_size; i=i+1)
mp_integer array_size;
if(to_integer(array_type.size(), array_size))
{
index_equality.rhs()=from_integer(i, index_equality.lhs().type());
if(index_equality.rhs().is_nil())
throw "number conversion failed (1)";
mp_integer offset=i*width;
for(unsigned j=0; j<width; j++)
equal_bv[j]=prop.lequal(bv[j],
array_bv[integer2long(offset+j)]);
prop.l_set_to_true(
prop.limplies(convert(index_equality), prop.land(equal_bv)));
std::cout << to_array_type(array.type()).size().pretty() << std::endl;
throw "failed to convert array size";
}
}
else
{
bv.resize(width);
equal_exprt equality;
equality.lhs()=index; // index operand
// get literals for the whole array
typet constant_type=index.type(); // type of index operand
const bvt &array_bv=convert_bv(array);
assert(array_size>0);
if(array_size*width!=array_bv.size())
throw "unexpected array size";
for(mp_integer i=0; i<array_size; i=i+1)
// TODO: maybe a shifter-like construction would be better
if(prop.has_set_to())
{
equality.op1()=from_integer(i, constant_type);
// free variables
literalt e=convert(equality);
bv.resize(width);
for(unsigned i=0; i<width; i++)
bv[i]=prop.new_variable();
mp_integer offset=i*width;
// add implications
for(unsigned j=0; j<width; j++)
equal_exprt index_equality;
index_equality.lhs()=index; // index operand
bvt equal_bv;
equal_bv.resize(width);
for(mp_integer i=0; i<array_size; i=i+1)
{
literalt l=array_bv[integer2long(offset+j)];
index_equality.rhs()=from_integer(i, index_equality.lhs().type());
if(i==0) // this initializes bv
bv[j]=l;
else
bv[j]=prop.lselect(e, l, bv[j]);
if(index_equality.rhs().is_nil())
throw "number conversion failed (1)";
mp_integer offset=i*width;
for(unsigned j=0; j<width; j++)
equal_bv[j]=prop.lequal(bv[j],
array_bv[integer2long(offset+j)]);
prop.l_set_to_true(
prop.limplies(convert(index_equality), prop.land(equal_bv)));
}
}
else
{
bv.resize(width);
equal_exprt equality;
equality.lhs()=index; // index operand
typet constant_type=index.type(); // type of index operand
assert(array_size>0);
for(mp_integer i=0; i<array_size; i=i+1)
{
equality.op1()=from_integer(i, constant_type);
literalt e=convert(equality);
mp_integer offset=i*width;
for(unsigned j=0; j<width; j++)
{
literalt l=array_bv[integer2long(offset+j)];
if(i==0) // this initializes bv
bv[j]=l;
else
bv[j]=prop.lselect(e, l, bv[j]);
}
}
}
}
else
return conversion_failed(expr, bv);
}
/*******************************************************************\