owi icon indicating copy to clipboard operation
owi copied to clipboard

remove symbolic_memory and use symbolic_memory_concretizing in concolic

Open redianthus opened this issue 1 year ago • 1 comments

@filipeom, I tried to do this but it does not typecheck and I'm not sure to understand what's going on for now... What do you think about this change?

redianthus avatar Aug 02 '24 22:08 redianthus

I think it would be interesting if we could do this. However, I think it's a little hard, and that's why I didn't do it in #371.

From #371, Symbolic_memory_make creates symbolic memories that internally use Symbolic_choice_without_memory. For example, the function:

val load_32 : t -> Symbolic_value.int32 -> Symbolic_value.int32

is now:

val load_32 : t -> Symbolic_value.int32 -> Symbolic_value.int32 Symbolic_choice_without_memory.t

So, in the concolic engine, we would need a function to lift 'a Symbolic_choice_without_memory.t into 'a Concolic_choice.t or another mechanism to unwrap the branching that might have taken place in the symbolic memory.

filipeom avatar Aug 03 '24 07:08 filipeom