CODEWITHSUNDEEP
cz3z3py
Robert
Robert

Reputation: 63

How would you implement dereferencing of pointers in z3

Trying to analyze some C programs with z3 in python, and got into trouble with pointers. I am working with terms like:

float * buffer = (float*)malloc(5*sizeof(float))

I interpret buffer as a BitVec(32) value so *buffer should be Real(). That should be ok, but what assertions should I write for the terms like 

*(buffer+3) or *(buffer+i)

How should be the assertions written if I am indexing out like 

*(buffer-1) or *(buffer+10)

Upvotes: 0

Views: 421

Answers (1)

Malte Schwerhoff
Malte Schwerhoff

Reputation: 12852

One solution is to encode the program heap as a map H from locations to values. In Z3, the array theory can be used to encode maps.

Pointers/addresses are integer locations, integer arithmetic encodes pointer arithmetic; this would allow constraints such as H(buffer + i) > 0 in your encoding. If you were to encode an OO-language, you could use the pair (receiver, field name) to encode addresses. E.g. H(r, f) > 0 would correspond to r.f > 0. Note that this map encoding naturally accounts for aliasing, e.g. if buffer1 == buffer2 and i == 3 then H(buffer1 + i) == H(buffer + 3).

See the paper Heaps and Data Structures: A Challenge for Automated Provers for an interesting comparison of map-based heap encodings.

Map-based encodings are typically used by tools based on verification condition, such as Frama-C, Dafny and Boogie. Tools based on symbolic execution, such as Silicon (which is part of the Viper verification infrastructure) and VeriFast typically use a different encoding; see, e.g. Heap-Dependent expressions in separation logic .

Upvotes: 4

Related Questions