Skip to content

Commit 936ca70

Browse files
committed
Interpreter: de-duplicate code
evaluate_address(byte_extract) and evaluate(byte_extract) had almost the same implementation. Instead of the duplication, use `evaluate_address` to implement `evaluate` and just handle the remaining bits in `evaluate`.
1 parent b4d939b commit 936ca70

File tree

1 file changed

+36
-37
lines changed

1 file changed

+36
-37
lines changed

src/goto-programs/interpreter_evaluate.cpp

Lines changed: 36 additions & 37 deletions
Original file line numberDiff line numberDiff line change
@@ -857,41 +857,11 @@ void interpretert::evaluate(
857857
}
858858
return;
859859
}
860-
else if(expr.id()==ID_byte_extract_little_endian ||
861-
expr.id()==ID_byte_extract_big_endian)
862-
{
863-
const auto &byte_extract_expr = to_byte_extract_expr(expr);
864-
865-
mp_vectort extract_offset;
866-
evaluate(byte_extract_expr.op1(), extract_offset);
867-
mp_vectort extract_from;
868-
evaluate(byte_extract_expr.op0(), extract_from);
869-
870-
if(extract_offset.size()==1 && extract_from.size()!=0)
871-
{
872-
const typet &target_type=expr.type();
873-
mp_integer memory_offset;
874-
// If memory offset is found (which should normally be the case)
875-
// extract the corresponding data from the appropriate memory location
876-
if(!byte_offset_to_memory_offset(
877-
byte_extract_expr.op0().type(), extract_offset[0], memory_offset))
878-
{
879-
mp_integer target_type_leaves;
880-
if(!count_type_leaves(target_type, target_type_leaves) &&
881-
target_type_leaves>0)
882-
{
883-
dest.insert(dest.end(),
884-
extract_from.begin()+memory_offset.to_long(),
885-
extract_from.begin()+(memory_offset+target_type_leaves).to_long());
886-
return;
887-
}
888-
}
889-
}
890-
}
891-
else if(expr.id()==ID_dereference ||
892-
expr.id()==ID_index ||
893-
expr.id()==ID_symbol ||
894-
expr.id()==ID_member)
860+
else if(
861+
expr.id() == ID_dereference || expr.id() == ID_index ||
862+
expr.id() == ID_symbol || expr.id() == ID_member ||
863+
expr.id() == ID_byte_extract_little_endian ||
864+
expr.id() == ID_byte_extract_big_endian)
895865
{
896866
mp_integer address=evaluate_address(
897867
expr,
@@ -932,16 +902,45 @@ void interpretert::evaluate(
932902
}
933903
else if(!address.is_zero())
934904
{
935-
if(!unbounded_size(expr.type()))
905+
if(
906+
expr.id() == ID_byte_extract_little_endian ||
907+
expr.id() == ID_byte_extract_big_endian)
908+
{
909+
const auto &byte_extract_expr = to_byte_extract_expr(expr);
910+
911+
mp_vectort extract_from;
912+
evaluate(byte_extract_expr.op(), extract_from);
913+
INVARIANT(
914+
!extract_from.empty(),
915+
"evaluate_address should have returned address == 0");
916+
const mp_integer memory_offset =
917+
address - evaluate_address(byte_extract_expr.op(), true);
918+
const typet &target_type = expr.type();
919+
mp_integer target_type_leaves;
920+
if(
921+
!count_type_leaves(target_type, target_type_leaves) &&
922+
target_type_leaves > 0)
923+
{
924+
dest.insert(
925+
dest.end(),
926+
extract_from.begin() + numeric_cast_v<std::size_t>(memory_offset),
927+
extract_from.begin() +
928+
numeric_cast_v<std::size_t>(memory_offset + target_type_leaves));
929+
return;
930+
}
931+
// we fail
932+
}
933+
else if(!unbounded_size(expr.type()))
936934
{
937935
dest.resize(numeric_cast_v<std::size_t>(get_size(expr.type())));
938936
read(address, dest);
937+
return;
939938
}
940939
else
941940
{
942941
read_unbounded(address, dest);
942+
return;
943943
}
944-
return;
945944
}
946945
}
947946
else if(expr.id()==ID_typecast)

0 commit comments

Comments
 (0)