owi
owi copied to clipboard
remove symbolic_memory and use symbolic_memory_concretizing in concolic
@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?
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.