Skip to content

Commit 75e6b45

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

File tree

1 file changed

+28
-34
lines changed

1 file changed

+28
-34
lines changed

src/goto-programs/interpreter_evaluate.cpp

+28-34
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,40 @@ 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+
// extract_from will be non-empty, otherwise evaluate_address would have
920+
// returned address == 0
921+
mp_vectort extract_from;
922+
evaluate(expr.op0(), extract_from);
923+
const mp_integer memory_offset =
924+
address - evaluate_address(expr.op0(), true);
925+
const typet &target_type = expr.type();
926+
mp_integer target_type_leaves;
927+
if(!count_type_leaves(target_type, target_type_leaves) &&
928+
target_type_leaves > 0)
929+
{
930+
dest.insert(
931+
dest.end(),
932+
extract_from.begin() + numeric_cast_v<std::size_t>(memory_offset),
933+
extract_from.begin() +
934+
numeric_cast_v<std::size_t>(memory_offset + target_type_leaves));
935+
return;
936+
}
937+
// we fail
938+
}
946939
if(!unbounded_size(expr.type()))
947940
{
948941
dest.resize(integer2size_t(get_size(expr.type())));
949942
read(address, dest);
943+
return;
950944
}
951945
else
952946
{
953947
read_unbounded(address, dest);
948+
return;
954949
}
955-
return;
956950
}
957951
}
958952
else if(expr.id()==ID_typecast)

0 commit comments

Comments
 (0)