Skip to content

Commit 130596e

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

File tree

1 file changed

+29
-34
lines changed

1 file changed

+29
-34
lines changed

src/goto-programs/interpreter_evaluate.cpp

Lines changed: 29 additions & 34 deletions
Original file line numberDiff line numberDiff line change
@@ -866,42 +866,12 @@ void interpretert::evaluate(
866866
}
867867
return;
868868
}
869-
else if(expr.id()==ID_byte_extract_little_endian ||
870-
expr.id()==ID_byte_extract_big_endian)
871-
{
872-
if(expr.operands().size()!=2)
873-
throw "byte_extract should have two operands";
874-
mp_vectort extract_offset;
875-
evaluate(expr.op1(), extract_offset);
876-
mp_vectort extract_from;
877-
evaluate(expr.op0(), extract_from);
878-
if(extract_offset.size()==1 && extract_from.size()!=0)
879-
{
880-
const typet &target_type=expr.type();
881-
mp_integer memory_offset;
882-
// If memory offset is found (which should normally be the case)
883-
// extract the corresponding data from the appropriate memory location
884-
if(!byte_offset_to_memory_offset(
885-
expr.op0().type(),
886-
extract_offset[0],
887-
memory_offset))
888-
{
889-
mp_integer target_type_leaves;
890-
if(!count_type_leaves(target_type, target_type_leaves) &&
891-
target_type_leaves>0)
892-
{
893-
dest.insert(dest.end(),
894-
extract_from.begin()+memory_offset.to_long(),
895-
extract_from.begin()+(memory_offset+target_type_leaves).to_long());
896-
return;
897-
}
898-
}
899-
}
900-
}
901869
else if(expr.id()==ID_dereference ||
902870
expr.id()==ID_index ||
903871
expr.id()==ID_symbol ||
904-
expr.id()==ID_member)
872+
expr.id()==ID_member ||
873+
expr.id() == ID_byte_extract_little_endian ||
874+
expr.id() == ID_byte_extract_big_endian)
905875
{
906876
mp_integer address=evaluate_address(
907877
expr,
@@ -955,16 +925,41 @@ void interpretert::evaluate(
955925
}
956926
else if(!address.is_zero())
957927
{
928+
if(expr.id()==ID_byte_extract_little_endian ||
929+
expr.id()==ID_byte_extract_big_endian)
930+
{
931+
mp_vectort extract_from;
932+
evaluate(expr.op0(), extract_from);
933+
INVARIANT(
934+
!extract_from.empty(),
935+
"evaluate_address should have returned address == 0");
936+
const mp_integer memory_offset =
937+
address - evaluate_address(expr.op0(), true);
938+
const typet &target_type = expr.type();
939+
mp_integer target_type_leaves;
940+
if(!count_type_leaves(target_type, target_type_leaves) &&
941+
target_type_leaves > 0)
942+
{
943+
dest.insert(
944+
dest.end(),
945+
extract_from.begin() + numeric_cast_v<std::size_t>(memory_offset),
946+
extract_from.begin() +
947+
numeric_cast_v<std::size_t>(memory_offset + target_type_leaves));
948+
return;
949+
}
950+
// we fail
951+
}
958952
if(!unbounded_size(expr.type()))
959953
{
960954
dest.resize(integer2size_t(get_size(expr.type())));
961955
read(address, dest);
956+
return;
962957
}
963958
else
964959
{
965960
read_unbounded(address, dest);
961+
return;
966962
}
967-
return;
968963
}
969964
}
970965
else if(expr.id()==ID_typecast)

0 commit comments

Comments
 (0)