Z3 Python API

We describe the API of Z3Mgr class used in Assignment-3 (Python version).

Z3Mgr (Z3 Manager)

Members	Meanings
Z3Mgr.store_value(loc, value)	Stores value to the location loc in loc_to_val_map (which is a Z3 array for handling memory operations)
Z3Mgr.load_value(loc)	Retrieves the value at location loc in loc_to_val_map
Z3Mgr.get_z3_expr(expr_name)	Returns a Z3 expression based on a variable's name
Z3Mgr.update_z3_expr(idx, target)	Updates expression for an index ID with the target expression
Z3Mgr.get_eval_expr(e)	Returns evaluated value of an expression if the expression has a solution (model); asserts unsat otherwise
Z3Mgr.has_z3_expr(expr_name)	Checks if an expression with the given name exists
Z3Mgr.get_z3_val(val)	Returns a Z3 integer value expression for the given integer
Z3Mgr.is_virtual_mem_address(val)	Checks if a value represents a valid virtual memory address
Z3Mgr.get_virtual_mem_address(idx)	Creates a virtual memory address for a given index
Z3Mgr.get_memobj_address(expr_name)	Returns a virtual memory address for an object based on its name
Z3Mgr.get_gepobj_address(base_expr, offset)	Returns the virtual memory address of a field given a base pointer and offset
Z3Mgr.add_to_solver(expr)	Adds a Z3 expression into the solver
Z3Mgr.reset_solver()	Resets the solver, clears all expressions and values
Z3Mgr.print_expr_values()	Prints the values of all Z3 expressions
solver.push()	Creates a new scope by saving the current stack
solver.pop()	Removes any expressions performed between it and the matching push

Helper Functions

Function	Meaning
check_negate_assert(z3_mgr, q)	Checks the negation of the assertion. Returns True if the negation is unsatisfiable, indicating the assertion holds

Test Methods

The Z3Mgr class includes several test methods (test0 through test10) that demonstrate different verification scenarios:

• test0: Simple pointer manipulation with assertion verification
• test1: Simple integer operations with assertion
• test2: One-level pointer operations with assertion
• test3: Multiple-level pointer operations
• test4: Array and pointer operations
• test5: Conditional branches with assertion verification
• test6: Pointer comparison with conditional branching
• test7: Branch verification with assertion
• test8: Array element selection with conditional branching
• test9: Struct and pointer operations
• test10: Function call simulation with assertion verification

Usage Example

# Create Z3 manager with space for 1000 expressions
z3_mgr = Z3Mgr(1000)

# Declare variables
p = z3_mgr.get_z3_expr("p")
q = z3_mgr.get_z3_expr("q")

# Add constraints
z3_mgr.add_to_solver(p == z3_mgr.get_memobj_address("p"))
z3_mgr.add_to_solver(q == 5)

# Perform memory operations
z3_mgr.store_value(p, q)
loaded_value = z3_mgr.load_value(p)

# Add assertion
z3_mgr.add_to_solver(loaded_value == 5)

# Check if constraints are satisfiable
result = z3_mgr.solver.check()
assert result == z3.sat, "Constraints not satisfiable"