search

GillianPlatform / Gillian

The Gillian Platform main repository
https://GillianPlatform.github.io
BSD 3-Clause "New" or "Revised" License
74 stars 11 forks source link

supporting symbolic object for javascript #224

Closed jackfromeast closed 1 year ago

jackfromeast commented 1 year ago

Hi!

I just try to make sure that currently Gillian-JS only support symbolic number and string in javascript right? Do you have a plan for supporting objects in the near future?

If not, what are the main complexities that come from supporting objects? Maybe I could help work on it.

giltho commented 1 year ago

Hello!

First of all, thank you for your issue, we're always happy to receive propositions of help. I'm not 100% sure I understand your question. Gillian-JS does have support for objects, since most things are objects in JS and GJS passes the test262 test suite. Could you expand on what you mean here? Thanks :)

jackfromeast commented 1 year ago

So, I read the document and I found that

Typing and Objects in Symbolic Tests Since we do not (yet) perform lazy initialization in symbolic execution, errors may occur if you attempt to reason about symbolic objects or untyped symbolic variables. Is that mean that currently, we cannot symbolically execute objects variable in JS?

My intention is to symbolically execute an object from one point to another in the program, in order to get what the object should look like to support this particular execution path. If lazy initialization is not implemented, I doubt whether can I achieve this task.

giltho commented 1 year ago

Oh god, I'm sorry for not answering earlier. Yes, sorry, GJS can't do this at the moment, if you mean doing this during a symbolic test. However, that's what bi-abduction should be able to achieve (although bi-abduction is not the most perfected part of Gillian at the moment)

NatKarmios commented 1 year ago

Yes, this is the sort of thing that bi-abduction is meant for. Looks like this discussion is done, so I'll close this issue for now :)