Skip to content

Commit 83575f5

Browse files
committed
Avoid redundant expressions when dereferencing
Our dereferencing code currently special-cases nested dereferences, allowing us to turn **x directly into something like (x == &o1 ? 1 : 2) in the best case where 'x' has two possible aliases, rather than going via an intermediary like '*(x == &o1 ? o1 : o2)' ==> '((x == &o1 ? o1 : o2) == &o3 ? 1 : 2)'. However, this can lead to redundnacy when o1 and o2 have overlapping alias sets, such as (x == &o1 ? (o1 == &o3 ? o3 : o4) : (o2 == &o3 ? o3 : o4)) In this case it is better to use a temporary: derefd_pointer = x == &o1 ? o1 : o2 result = derefd_pointer == &o3 ? o3 : o4 This restructuring of value_set_dereferencet::dereference attempts to keep the best of both worlds by dividing the algorithm into two stages: one which determines the alias sets that would be created, using placeholder symbols to mark where they occur in the overall expression, followed by a commit stage which decides whether to commit the tentative result or to combine the alias sets and use an intermediate temporary symbol instead. The result should be that when alias sets overlap we use an intermediate variable, but when they are disjoint we apply the double-dereference in-place.
1 parent 5d2e8b9 commit 83575f5

File tree

3 files changed

+344
-81
lines changed

3 files changed

+344
-81
lines changed

regression/cbmc/double_deref/double_deref_with_pointer_arithmetic_single_alias.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
double_deref_with_pointer_arithmetic_single_alias.c
33
--show-vcc
4-
\{1\} \(derefd_pointer::derefd_pointer!0#1 = address_of\(symex_dynamic::dynamic_object2\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)
4+
\{1\} \(symex_dynamic::dynamic_object1#2\[cast\(mod #source_location=""\(main::argc!0@1#1, 2\), signedbv\[64\]\)\] = address_of\(symex_dynamic::dynamic_object2\) \? main::argc!0@1#1 = 1 : symex::invalid_object!0#0 = main::argc!0@1#1\)
55
^EXIT=0$
66
^SIGNAL=0$
77
--

0 commit comments

Comments
 (0)