Skip to content

Commit f36c08c

Browse files
committed
Interpreter: de-duplicate code
evaluate_address(byte_extract) and evaluate(byte_extract) had almost the same implementation.
1 parent 1a970e3 commit f36c08c

File tree

1 file changed

+33
-37
lines changed

1 file changed

+33
-37
lines changed

src/goto-programs/interpreter_evaluate.cpp

Lines changed: 33 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -885,42 +885,11 @@ void interpretert::evaluate(
885885
}
886886
return;
887887
}
888-
else if(expr.id()==ID_byte_extract_little_endian ||
889-
expr.id()==ID_byte_extract_big_endian)
890-
{
891-
if(expr.operands().size()!=2)
892-
throw "byte_extract should have two operands";
893-
mp_vectort extract_offset;
894-
evaluate(expr.op1(), extract_offset);
895-
mp_vectort extract_from;
896-
evaluate(expr.op0(), extract_from);
897-
if(extract_offset.size()==1 && extract_from.size()!=0)
898-
{
899-
const typet &target_type=expr.type();
900-
mp_integer memory_offset;
901-
// If memory offset is found (which should normally be the case)
902-
// extract the corresponding data from the appropriate memory location
903-
if(!byte_offset_to_memory_offset(
904-
expr.op0().type(),
905-
extract_offset[0],
906-
memory_offset))
907-
{
908-
mp_integer target_type_leaves;
909-
if(!count_type_leaves(target_type, target_type_leaves) &&
910-
target_type_leaves>0)
911-
{
912-
dest.insert(dest.end(),
913-
extract_from.begin()+memory_offset.to_long(),
914-
extract_from.begin()+(memory_offset+target_type_leaves).to_long());
915-
return;
916-
}
917-
}
918-
}
919-
}
920-
else if(expr.id()==ID_dereference ||
921-
expr.id()==ID_index ||
922-
expr.id()==ID_symbol ||
923-
expr.id()==ID_member)
888+
else if(
889+
expr.id() == ID_dereference || expr.id() == ID_index ||
890+
expr.id() == ID_symbol || expr.id() == ID_member ||
891+
expr.id() == ID_byte_extract_little_endian ||
892+
expr.id() == ID_byte_extract_big_endian)
924893
{
925894
mp_integer address=evaluate_address(
926895
expr,
@@ -959,16 +928,43 @@ void interpretert::evaluate(
959928
}
960929
else if(!address.is_zero())
961930
{
931+
if(
932+
expr.id() == ID_byte_extract_little_endian ||
933+
expr.id() == ID_byte_extract_big_endian)
934+
{
935+
mp_vectort extract_from;
936+
evaluate(expr.op0(), extract_from);
937+
INVARIANT(
938+
!extract_from.empty(),
939+
"evaluate_address should have returned address == 0");
940+
const mp_integer memory_offset =
941+
address - evaluate_address(expr.op0(), true);
942+
const typet &target_type = expr.type();
943+
mp_integer target_type_leaves;
944+
if(
945+
!count_type_leaves(target_type, target_type_leaves) &&
946+
target_type_leaves > 0)
947+
{
948+
dest.insert(
949+
dest.end(),
950+
extract_from.begin() + numeric_cast_v<std::size_t>(memory_offset),
951+
extract_from.begin() +
952+
numeric_cast_v<std::size_t>(memory_offset + target_type_leaves));
953+
return;
954+
}
955+
// we fail
956+
}
962957
if(!unbounded_size(expr.type()))
963958
{
964959
dest.resize(numeric_cast_v<std::size_t>(get_size(expr.type())));
965960
read(address, dest);
961+
return;
966962
}
967963
else
968964
{
969965
read_unbounded(address, dest);
966+
return;
970967
}
971-
return;
972968
}
973969
}
974970
else if(expr.id()==ID_typecast)

0 commit comments

Comments
 (0)