wrong constraint path after the memory update

[EpureRares]

Hi,
I am trying to make symbolic execution. I want to update the memory and some registers at a certain point of execution using the following functions void setConcreteMemoryValue(integer addr, integer value) and void setConcreteRegisterValue(Register reg, integer value), but there is a problem with the constraint path. The documentation says that these functions imply a desynchronization with the symbolic state. What can I do in this case in order to restore de symbolic state?
Thank you,
Rares

[SweetVishnya]

You may compare symbolic and concrete memory states. And concertize symbolic state if they differ.

[EpureRares]

How can I compare the states? Should I compare the concrete values and the symbolic values from that address?

[JonathanSalwan]

but there is a problem with the constraint path.

What do you means? Do you means that the path constraint (from getPathPredicate() or getPathConstraints()) is wrong regarding the new concrete value injected?

You may compare symbolic and concrete memory states. And concertize symbolic state if they differ.

This is no longer relevant since now when calling setConcrete{Memory, Register}Value the symbolic state is automatically concretized (NOTE: it's true only if you use those methods from the API class).

[EpureRares]

I have the following function:

char * function(char *ptr) {
  if (ptr[0] == '0') {
    free(ptr);
  }
  printf("%s\n", ptr);
  
  if (ptr[1] == '1') {
    free(ptr);
  }
  return ptr;
}

I use Triton to make symbolic execution, but when a system or a library call occurs that call is executed by another tool. After that call, I try to restore the context by copying sections of memory to Triton. In this case, after the printf call, it seems that something goes wrong because Triton cannot identify the constraint that comes from the second if. The second constraint is not added to the constraint path. I use getPathConstraints() to get the constraints.

[JonathanSalwan]

I try to restore the context by copying sections of memory to Triton

You probably called setConcreteMemoryValue for this purpose, right? If yes, as I said, when calling setConcreteMemoryValue you will concretize your memory space (ptr[0], ptr[1], ptr[n]) and so lost your symbolic variables. By default Triton keeps in its path predicate constraints that only contain symbolic variables. That's probably why you do not have the second constraint on you path predicate. By the way, if you want to keep all constraints in your path predicate even if they are not symbolic you can disable the mode MODE.PC_TRACKING_SYMBOLIC.

The best way when restoring context from another tool is to verify if there is a desynch like @SweetVishnya said. For example, take a look to a QBDI+Triton tool. Especially the following part of the code:

# Triton callback. This callback is called when triton need to know
# the concrete value of memory cells. Synchronize memory cells between
# Triton and QBDI
def mem_read(tt, mem):
    addr = mem.getAddress()
    size = mem.getSize()

    qbdi_value   = pyqbdi.readMemory(addr, size)
    triton_value = tt.getConcreteMemoryAreaValue(addr, size)

    # If qbdi and triton mem cells are not equal, synch Triton with
    # the context of qbdi
    if qbdi_value != triton_value:
        print(F"[triton] Memory cells ({addr:x}:{size:d}) synchronization")
        tt.setConcreteMemoryAreaValue(addr, qbdi_value)

    return

[EpureRares]

I use in my implementation setConcreteMemoryValue . Thank you for your response. This solved the memory problems, but my question now is whether there is a way to keep the constraints from symbolized registers because I update the registers when I restore the context.

[JonathanSalwan]

You can do the same thing but with getConcreteRegisterValue and within a GET_CONCRETE_REGISTER_VALUE callback?