Skip to content

Commit

Permalink
rename op1/op2 to index/new_value in convert_with
Browse files Browse the repository at this point in the history 
This replaces op1/op2 by identifiers that clearly state the purpose of the
operand.
  • Loading branch information
@kroening
kroening committed Feb 4, 2024
1 parent 5bdff46 commit b25f25a
Show file tree
Hide file tree
Showing 2 changed files with 68 additions and 58 deletions.
18 changes: 9 additions & 9 deletions src/solvers/flattening/boolbv.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -198,34 +198,34 @@ class boolbvt:public arrayst

void convert_with(
const typet &type,
const exprt &op1,
const exprt &op2,
const exprt &where,
const exprt &new_value,
const bvt &prev_bv,
bvt &next_bv);

void convert_with_bv(
const exprt &op1,
const exprt &op2,
const exprt &index,
const exprt &new_value,
const bvt &prev_bv,
bvt &next_bv);

void convert_with_array(
const array_typet &type,
const exprt &op1,
const exprt &op2,
const exprt &index,
const exprt &new_value,
const bvt &prev_bv,
bvt &next_bv);

void convert_with_union(
const union_typet &type,
const exprt &op2,
const exprt &new_value,
const bvt &prev_bv,
bvt &next_bv);

void convert_with_struct(
const struct_typet &type,
const exprt &op1,
const exprt &op2,
const exprt &where,
const exprt &new_value,
const bvt &prev_bv,
bvt &next_bv);

Expand Down
108 changes: 59 additions & 49 deletions src/solvers/flattening/boolbv_with.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -47,8 +47,8 @@ bvt boolbvt::convert_with(const with_exprt &expr)

void boolbvt::convert_with(
const typet &type,
const exprt &op1,
const exprt &op2,
const exprt &where,
const exprt &new_value,
const bvt &prev_bv,
bvt &next_bv)
{
Expand All @@ -57,31 +57,40 @@ void boolbvt::convert_with(
next_bv.resize(prev_bv.size());

if(type.id()==ID_array)
return convert_with_array(to_array_type(type), op1, op2, prev_bv, next_bv);
return convert_with_array(
to_array_type(type), where, new_value, prev_bv, next_bv);
else if(type.id()==ID_bv ||
type.id()==ID_unsignedbv ||
type.id()==ID_signedbv)
return convert_with_bv(op1, op2, prev_bv, next_bv);
return convert_with_bv(where, new_value, prev_bv, next_bv);
else if(type.id()==ID_struct)
return
convert_with_struct(to_struct_type(type), op1, op2, prev_bv, next_bv);
return convert_with_struct(
to_struct_type(type), where, new_value, prev_bv, next_bv);
else if(type.id() == ID_struct_tag)
return convert_with(
ns.follow_tag(to_struct_tag_type(type)), op1, op2, prev_bv, next_bv);
ns.follow_tag(to_struct_tag_type(type)),
where,
new_value,
prev_bv,
next_bv);
else if(type.id()==ID_union)
return convert_with_union(to_union_type(type), op2, prev_bv, next_bv);
return convert_with_union(to_union_type(type), new_value, prev_bv, next_bv);
else if(type.id() == ID_union_tag)
return convert_with(
ns.follow_tag(to_union_tag_type(type)), op1, op2, prev_bv, next_bv);
ns.follow_tag(to_union_tag_type(type)),
where,
new_value,
prev_bv,
next_bv);

DATA_INVARIANT_WITH_DIAGNOSTICS(
false, "unexpected with type", irep_pretty_diagnosticst{type});
}

void boolbvt::convert_with_array(
const array_typet &type,
const exprt &op1,
const exprt &op2,
const exprt &index,
const exprt &new_value,
const bvt &prev_bv,
bvt &next_bv)
{
Expand All @@ -100,89 +109,90 @@ void boolbvt::convert_with_array(
"convert_with_array expects constant array size",
irep_pretty_diagnosticst{type});

const bvt &op2_bv=convert_bv(op2);
const bvt &new_value_bv = convert_bv(new_value);

DATA_INVARIANT_WITH_DIAGNOSTICS(
*size * op2_bv.size() == prev_bv.size(),
"convert_with_array: unexpected operand 2 width",
*size * new_value_bv.size() == prev_bv.size(),
"convert_with_array: unexpected new_value operand width",
irep_pretty_diagnosticst{type});

// Is the index a constant?
if(const auto op1_value = numeric_cast<mp_integer>(op1))
if(const auto index_value_opt = numeric_cast<mp_integer>(index))
{
// Yes, it is!
next_bv=prev_bv;

if(*op1_value >= 0 && *op1_value < *size) // bounds check
if(*index_value_opt >= 0 && *index_value_opt < *size) // bounds check
{
const std::size_t offset =
numeric_cast_v<std::size_t>(*op1_value * op2_bv.size());
numeric_cast_v<std::size_t>(*index_value_opt * new_value_bv.size());

for(std::size_t j=0; j<op2_bv.size(); j++)
next_bv[offset+j]=op2_bv[j];
for(std::size_t j = 0; j < new_value_bv.size(); j++)
next_bv[offset + j] = new_value_bv[j];
}

return;
}

typet counter_type=op1.type();
typet counter_type = index.type();

for(mp_integer i=0; i<size; i=i+1)
{
exprt counter=from_integer(i, counter_type);

literalt eq_lit=convert(equal_exprt(op1, counter));
literalt eq_lit = convert(equal_exprt(index, counter));

const std::size_t offset = numeric_cast_v<std::size_t>(i * op2_bv.size());
const std::size_t offset =
numeric_cast_v<std::size_t>(i * new_value_bv.size());

for(std::size_t j=0; j<op2_bv.size(); j++)
next_bv[offset+j]=
prop.lselect(eq_lit, op2_bv[j], prev_bv[offset+j]);
for(std::size_t j = 0; j < new_value_bv.size(); j++)
next_bv[offset + j] =
prop.lselect(eq_lit, new_value_bv[j], prev_bv[offset + j]);
}
}

void boolbvt::convert_with_bv(
const exprt &op1,
const exprt &op2,
const exprt &index,
const exprt &new_value,
const bvt &prev_bv,
bvt &next_bv)
{
literalt l=convert(op2);
literalt l = convert(new_value);

if(const auto op1_value = numeric_cast<mp_integer>(op1))
if(const auto index_value_opt = numeric_cast<mp_integer>(index))
{
next_bv=prev_bv;

if(*op1_value < next_bv.size())
next_bv[numeric_cast_v<std::size_t>(*op1_value)] = l;
if(*index_value_opt >= 0 && *index_value_opt < next_bv.size())
next_bv[numeric_cast_v<std::size_t>(*index_value_opt)] = l;

return;
}

typet counter_type=op1.type();
typet counter_type = index.type();

for(std::size_t i=0; i<prev_bv.size(); i++)
{
exprt counter=from_integer(i, counter_type);

literalt eq_lit=convert(equal_exprt(op1, counter));
literalt eq_lit = convert(equal_exprt(index, counter));

next_bv[i]=prop.lselect(eq_lit, l, prev_bv[i]);
}
}

void boolbvt::convert_with_struct(
const struct_typet &type,
const exprt &op1,
const exprt &op2,
const exprt &where,
const exprt &new_value,
const bvt &prev_bv,
bvt &next_bv)
{
next_bv=prev_bv;

const bvt &op2_bv=convert_bv(op2);
const bvt &new_value_bv = convert_bv(new_value);

const irep_idt &component_name=op1.get(ID_component_name);
const irep_idt &component_name = where.get(ID_component_name);
const struct_typet::componentst &components=
type.components();

Expand All @@ -197,19 +207,19 @@ void boolbvt::convert_with_struct(
if(c.get_name() == component_name)
{
DATA_INVARIANT_WITH_DIAGNOSTICS(
subtype == op2.type(),
subtype == new_value.type(),
"with/struct: component '" + id2string(component_name) +
"' type does not match",
irep_pretty_diagnosticst{subtype},
irep_pretty_diagnosticst{op2.type()});
irep_pretty_diagnosticst{new_value.type()});

DATA_INVARIANT_WITH_DIAGNOSTICS(
sub_width == op2_bv.size(),
"convert_with_struct: unexpected operand op2 width",
sub_width == new_value_bv.size(),
"convert_with_struct: unexpected new_value operand width",
irep_pretty_diagnosticst{type});

for(std::size_t i=0; i<sub_width; i++)
next_bv[offset+i]=op2_bv[i];
next_bv[offset + i] = new_value_bv[i];

break; // done
}
Expand All @@ -220,22 +230,22 @@ void boolbvt::convert_with_struct(

void boolbvt::convert_with_union(
const union_typet &type,
const exprt &op2,
const exprt &new_value,
const bvt &prev_bv,
bvt &next_bv)
{
next_bv=prev_bv;

const bvt &op2_bv=convert_bv(op2);
const bvt &new_value_bv = convert_bv(new_value);

DATA_INVARIANT_WITH_DIAGNOSTICS(
next_bv.size() >= op2_bv.size(),
"convert_with_union: unexpected operand op2 width",
next_bv.size() >= new_value_bv.size(),
"convert_with_union: unexpected new_value operand width",
irep_pretty_diagnosticst{type});

endianness_mapt map_u = endianness_map(type);
endianness_mapt map_op2 = endianness_map(op2.type());
endianness_mapt map_new_value = endianness_map(new_value.type());

for(std::size_t i = 0; i < op2_bv.size(); i++)
next_bv[map_u.map_bit(i)] = op2_bv[map_op2.map_bit(i)];
for(std::size_t i = 0; i < new_value_bv.size(); i++)
next_bv[map_u.map_bit(i)] = new_value_bv[map_new_value.map_bit(i)];
}

0 comments on commit b25f25a

Please sign in to comment.