Skip to content

Commit 9bae4ad

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

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
@@ -862,42 +862,12 @@ void interpretert::evaluate(
862862
}
863863
return;
864864
}
865-
else if(expr.id()==ID_byte_extract_little_endian ||
866-
expr.id()==ID_byte_extract_big_endian)
867-
{
868-
if(expr.operands().size()!=2)
869-
throw "byte_extract should have two operands";
870-
mp_vectort extract_offset;
871-
evaluate(expr.op1(), extract_offset);
872-
mp_vectort extract_from;
873-
evaluate(expr.op0(), extract_from);
874-
if(extract_offset.size()==1 && extract_from.size()!=0)
875-
{
876-
const typet &target_type=expr.type();
877-
mp_integer memory_offset;
878-
// If memory offset is found (which should normally be the case)
879-
// extract the corresponding data from the appropriate memory location
880-
if(!byte_offset_to_memory_offset(
881-
expr.op0().type(),
882-
extract_offset[0],
883-
memory_offset))
884-
{
885-
mp_integer target_type_leaves;
886-
if(!count_type_leaves(target_type, target_type_leaves) &&
887-
target_type_leaves>0)
888-
{
889-
dest.insert(dest.end(),
890-
extract_from.begin()+memory_offset.to_long(),
891-
extract_from.begin()+(memory_offset+target_type_leaves).to_long());
892-
return;
893-
}
894-
}
895-
}
896-
}
897865
else if(expr.id()==ID_dereference ||
898866
expr.id()==ID_index ||
899867
expr.id()==ID_symbol ||
900-
expr.id()==ID_member)
868+
expr.id()==ID_member ||
869+
expr.id() == ID_byte_extract_little_endian ||
870+
expr.id() == ID_byte_extract_big_endian)
901871
{
902872
mp_integer address=evaluate_address(
903873
expr,
@@ -937,16 +907,41 @@ void interpretert::evaluate(
937907
}
938908
else if(!address.is_zero())
939909
{
910+
if(expr.id()==ID_byte_extract_little_endian ||
911+
expr.id()==ID_byte_extract_big_endian)
912+
{
913+
mp_vectort extract_from;
914+
evaluate(expr.op0(), extract_from);
915+
INVARIANT(
916+
!extract_from.empty(),
917+
"evaluate_address should have returned address == 0");
918+
const mp_integer memory_offset =
919+
address - evaluate_address(expr.op0(), true);
920+
const typet &target_type = expr.type();
921+
mp_integer target_type_leaves;
922+
if(!count_type_leaves(target_type, target_type_leaves) &&
923+
target_type_leaves > 0)
924+
{
925+
dest.insert(
926+
dest.end(),
927+
extract_from.begin() + numeric_cast_v<std::size_t>(memory_offset),
928+
extract_from.begin() +
929+
numeric_cast_v<std::size_t>(memory_offset + target_type_leaves));
930+
return;
931+
}
932+
// we fail
933+
}
940934
if(!unbounded_size(expr.type()))
941935
{
942936
dest.resize(integer2size_t(get_size(expr.type())));
943937
read(address, dest);
938+
return;
944939
}
945940
else
946941
{
947942
read_unbounded(address, dest);
943+
return;
948944
}
949-
return;
950945
}
951946
}
952947
else if(expr.id()==ID_typecast)

0 commit comments

Comments
 (0)