Skip to content

Commit dc4ff25

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

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
@@ -854,42 +854,12 @@ void interpretert::evaluate(
854854
}
855855
return;
856856
}
857-
else if(expr.id()==ID_byte_extract_little_endian ||
858-
expr.id()==ID_byte_extract_big_endian)
859-
{
860-
if(expr.operands().size()!=2)
861-
throw "byte_extract should have two operands";
862-
mp_vectort extract_offset;
863-
evaluate(expr.op1(), extract_offset);
864-
mp_vectort extract_from;
865-
evaluate(expr.op0(), extract_from);
866-
if(extract_offset.size()==1 && extract_from.size()!=0)
867-
{
868-
const typet &target_type=expr.type();
869-
mp_integer memory_offset;
870-
// If memory offset is found (which should normally be the case)
871-
// extract the corresponding data from the appropriate memory location
872-
if(!byte_offset_to_memory_offset(
873-
expr.op0().type(),
874-
extract_offset[0],
875-
memory_offset))
876-
{
877-
mp_integer target_type_leaves;
878-
if(!count_type_leaves(target_type, target_type_leaves) &&
879-
target_type_leaves>0)
880-
{
881-
dest.insert(dest.end(),
882-
extract_from.begin()+memory_offset.to_long(),
883-
extract_from.begin()+(memory_offset+target_type_leaves).to_long());
884-
return;
885-
}
886-
}
887-
}
888-
}
889857
else if(expr.id()==ID_dereference ||
890858
expr.id()==ID_index ||
891859
expr.id()==ID_symbol ||
892-
expr.id()==ID_member)
860+
expr.id()==ID_member ||
861+
expr.id() == ID_byte_extract_little_endian ||
862+
expr.id() == ID_byte_extract_big_endian)
893863
{
894864
mp_integer address=evaluate_address(
895865
expr,
@@ -943,16 +913,41 @@ void interpretert::evaluate(
943913
}
944914
else if(!address.is_zero())
945915
{
916+
if(expr.id()==ID_byte_extract_little_endian ||
917+
expr.id()==ID_byte_extract_big_endian)
918+
{
919+
mp_vectort extract_from;
920+
evaluate(expr.op0(), extract_from);
921+
INVARIANT(
922+
!extract_from.empty(),
923+
"evaluate_address should have returned address == 0");
924+
const mp_integer memory_offset =
925+
address - evaluate_address(expr.op0(), true);
926+
const typet &target_type = expr.type();
927+
mp_integer target_type_leaves;
928+
if(!count_type_leaves(target_type, target_type_leaves) &&
929+
target_type_leaves > 0)
930+
{
931+
dest.insert(
932+
dest.end(),
933+
extract_from.begin() + numeric_cast_v<std::size_t>(memory_offset),
934+
extract_from.begin() +
935+
numeric_cast_v<std::size_t>(memory_offset + target_type_leaves));
936+
return;
937+
}
938+
// we fail
939+
}
946940
if(!unbounded_size(expr.type()))
947941
{
948942
dest.resize(integer2size_t(get_size(expr.type())));
949943
read(address, dest);
944+
return;
950945
}
951946
else
952947
{
953948
read_unbounded(address, dest);
949+
return;
954950
}
955-
return;
956951
}
957952
}
958953
else if(expr.id()==ID_typecast)

0 commit comments

Comments
 (0)