Skip to content

remove symbolic_memory and use symbolic_memory_concretizing in concolic#402

Closed
redianthus wants to merge 1 commit intoOCamlPro:mainfrom
redianthus:concretizing_memory_in_conc
Closed

remove symbolic_memory and use symbolic_memory_concretizing in concolic#402
redianthus wants to merge 1 commit intoOCamlPro:mainfrom
redianthus:concretizing_memory_in_conc

Conversation

@redianthus
Copy link
Member

@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?

@filipeom
Copy link
Collaborator

filipeom commented Aug 3, 2024

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.

@redianthus redianthus closed this May 15, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants