Inconsistency between liftToSMT and isSat when MEMORY_ARRAY is enabled

[NVThufv]

Here is a code snippet that checks the value of memory using a symbolic index.

self.ctx = TritonContext(ARCH.X86_64)
self.ctx.setMode(MODE.MEMORY_ARRAY, True)
self.ctx.setMode(MODE.SYMBOLIZE_LOAD, True)
self.ctx.setMode(MODE.SYMBOLIZE_STORE, True)
code = [
	(1, b"\x48\xc7\xc0\x00\x10\x00\x00"), # mov rax, 0x1000
	(2, b"\x48\xc7\xc3\x32\x00\x00\x00"), # mov rbx, 0x32
	# (3, b"\x89\x34\x18"), # mov dword ptr [rax + rbx], esi
	(4, b"\x8b\x0c\x18"), # mov ecx, dword ptr [rax + rbx]
	(5, b"\x48\x81\xf9\xad\xde\x00\x00"), # cmp rcx, 0xdead
]

self.ctx.symbolizeRegister(self.ctx.registers.rax, 's_rax')
self.ctx.symbolizeRegister(self.ctx.registers.rbx, 's_rbx')
self.ctx.symbolizeRegister(self.ctx.registers.rcx, 's_rcx')
self.ctx.symbolizeRegister(self.ctx.registers.rsi, 's_rsi')

for _, op in code:
	self.ctx.processing(Instruction(op))
	
zf = self.ctx.getRegisterAst(self.ctx.registers.zf)
print(self.ctx.isSat(zf == 1))
print(self.ctx.liftToSMT(self.ctx.newSymbolicExpression(zf == 1)))

The result of self.ctx.isSat is False. However, the corresponding SMT formula is

(define-fun ref!4 () (_ BitVec 64) (_ bv4096 64)) ; MOV operation
(define-fun ref!6 () (_ BitVec 64) (_ bv50 64)) ; MOV operation
(declare-fun ref!8 () (Array (_ BitVec 64) (_ BitVec 8)))
(define-fun ref!9 () (_ BitVec 64) ((_ zero_extend 32) (concat (select ref!8 (bvadd (bvadd (bvadd ref!4 (bvmul ref!6 (_ bv1 64))) (_ bv0 64)) (_ bv3 64))) (select ref!8 (bvadd (bvadd (bvadd ref!4 (bvmul ref!6 (_ bv1 64))) (_ bv0 64)) (_ bv2 64))) (select ref!8 (bvadd (bvadd (bvadd ref!4 (bvmul ref!6 (_ bv1 64))) (_ bv0 64)) (_ bv1 64))) (select ref!8 (bvadd (bvadd (bvadd ref!4 (bvmul ref!6 (_ bv1 64))) (_ bv0 64)) (_ bv0 64)))))) ; MOV operation
(define-fun ref!11 () (_ BitVec 64) (bvsub ref!9 (_ bv57005 64))) ; CMP operation
(define-fun ref!17 () (_ BitVec 1) (ite (= ref!11 (_ bv0 64)) (_ bv1 1) (_ bv0 1))) ; Zero flag
(define-fun ref!19 () (_ BitVec 1) (= ref!17 (_ bv1 1)))

By replacing ref!19 to

(assert (= ref!17 (_ bv1 1)))
(check-sat)
(get-model)

and feeding the formula to Z3, the solver instead returns a satisfiable result. It appears that isSat is assuming a memory state defaults to 0 instead of having no constraint, but this is not the case for liftToSMT. And I am wondering if it is possible for triton to concisely choose no constraint for every memory state/register (that is, symbolic) instead of assuming them to be zero by default. I find this to be much more useful for certain types of analysis.

[JonathanSalwan]

Indeed, this is because we consider array as const array with a default value 0, like it's pretty much the case when you spawn a process with uninitialized memory. We chosen to define this array as const, otherwise every cell's content is consider as symbolic by the SMT solver which is problematic in several cases.

However, I understand that for some cases, you might want to have these cell's content symbolic. Maybe we can have two modes for this, like MEMORY_CONST_ARRAY and MEMORY_ARRAY ?

[NVThufv]

Yes I think the additional modes are helpful. The following snippet for tritonToZ3.cpp may help

case ARRAY_NODE: {
	auto size  = triton::ast::getInteger<triton::uint32>(node->getChildren()[0]);
	auto isort = this->context.bv_sort(size);
	if(MODE.MEMORY_CONST_ARRAY){
		auto value = this->context.bv_val(0, 8);
		return to_expr(this->context, Z3_mk_const_array(this->context, isort, value));
	} else if(MODE.MEMORY_ARRAY){
		auto vsort = this->context.bv_sort(8);
		auto arraySort = this->context.array_sort(isort, vsort);
		return this->context.constant("memory", arraySort);
	}
}

(Of course, the model collecting mechanism in z3solver.cpp and other related codes may need additional adjustment, since it will result in non-bv sort elements like memory).