Open NVThufv opened 2 months ago
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
?
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
).
Here is a code snippet that checks the value of memory using a symbolic index.
The result of
self.ctx.isSat
isFalse
. However, the corresponding SMT formula isBy replacing
ref!19
toand 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 forliftToSMT
. 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.