Let's do abstraction-refinement

[msooseth]

It turns out that Halmos is doing abstraction-refinement. Their system is 2-state: first run all bitvector operations in a abstract way, then strip away the abstraction if the returned counterexample is not correct.

Their description of arithmetic is:

# uninterpreted arithmetic
f_add  = { 256: Function('evm_bvadd', BitVecSort(256), BitVecSort(256), BitVecSort(256)), 264: Function('evm_bvadd_264', BitVecSort(264), BitVecSort(264), BitVecSort(264)) }
f_sub  = Function('evm_bvsub' , BitVecSort(256), BitVecSort(256), BitVecSort(256))
f_mul  = { 256: Function('evm_bvmul', BitVecSort(256), BitVecSort(256), BitVecSort(256)), 512: Function('evm_bvmul_512', BitVecSort(512), BitVecSort(512), BitVecSort(512)) }
f_div  = Function('evm_bvudiv' , BitVecSort(256), BitVecSort(256), BitVecSort(256))
f_mod  = { 256: Function('evm_bvurem', BitVecSort(256), BitVecSort(256), BitVecSort(256)), 264: Function('evm_bvurem_264', BitVecSort(264), BitVecSort(264), BitVecSort(264)), 512: Function('evm_bvurem_512', BitVecSort(512), BitVecSort(512), BitVecSort(512)) }
f_sdiv = Function('evm_bvsdiv', BitVecSort(256), BitVecSort(256), BitVecSort(256))
f_smod = Function('evm_bvsrem', BitVecSort(256), BitVecSort(256), BitVecSort(256))
f_exp  = Function('evm_exp' , BitVecSort(256), BitVecSort(256), BitVecSort(256))

Then they run it, and see if it's OK. If not, they strip away the abstraction and run it on a new Z3 instance, now fully interpreted:

 if is_unknown(res, model) and args.solver_subprocess:
        [...]
        query = ex.solver.to_smt2()
        # replace uninterpreted abstraction with actual symbols for assertion solving
        query = re.sub(r'(\(\s*)evm_(bv[a-z]+)(_[0-9]+)?\b', r'\1\2', query) # TODO: replace `(evm_bvudiv x y)` with `(ite (= y (_ bv0 256)) (_ bv0 256) (bvudiv x y))` as bvudiv is undefined when y = 0; also similarly for evm_bvurem
        with open(fname, 'w') as f:
            f.write('(set-logic QF_AUFBV)\n')
            f.write(query)
        res_str = subprocess.run(['z3', '-model', fname], capture_output=True, text=True).stdout.strip()

Notice that the regexp simply strips away the evm_ which now becomes the fully interpreted arithmetic.

Where the helper functions are:

def is_unknown(result: CheckSatResult, model: Model) -> bool:
    return result == unknown or (result == sat and not is_valid_model(model))

def is_valid_model(model) -> bool:
    for decl in model:
        if str(decl).startswith('evm_'):
            return False
    return True

Notice that they create a whole new Z3 executable, hence not retaining any state between abstract and concrete interpretations.

--

We should do something similar first, but the real deal would be to: (1) refine only the parts that don't make sense in terms of the model, thereby making a multi-stage refinement, and (2) retain state by using the the SMT solver through the API.

[msooseth]

Notes to self:

• Turns out they do only PARTIAL abstraction refinement. For mod/mul/div/etc they abstract, but for e.g. XOR they don't. This makes sense, because binary operations are cheap and easy.