Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Implement ghost state in all language backends #1929

Closed
RyanGlScott opened this issue Sep 1, 2023 · 1 comment · Fixed by #1958
Closed

Implement ghost state in all language backends #1929

RyanGlScott opened this issue Sep 1, 2023 · 1 comment · Fixed by #1958
Labels
subsystem: crucible-jvm Issues related to Java verification with crucible-jvm subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm subsystem: crucible-mir Issues related to Rust verification with crucible-mir and/or mir-json type: feature request Issues requesting a new feature or capability

Comments

@RyanGlScott
Copy link
Contributor

SAW's has a ghost state feature that is conceptually independent of any particular language backend. At the moment, however, ghost state is only implemented on the LLVM backend via the llvm_declare_ghost_state and llvm_ghost_value commands. This issue tracks implementing support for ghost state in the JVM and MIR backends as well.

Two possible ways of going about this are:

  1. Add {jvm,mir}_declare_ghost_state and {jvm,mir}_ghost_state counterparts to the existing llvm_declare_ghost_state and llvm_ghost_value commands.
  2. Add general-purpose declare_ghost_state and ghost_value commands, and make llvm_declare_ghost_state and llvm_ghost_value deprecated aliases for them.

I'm more inclined to do (2), as nothing in the types of the llvm_declare_ghost_state or llvm_ghost_value commands is specific to LLVM.
@RyanGlScott RyanGlScott added subsystem: crucible-jvm Issues related to Java verification with crucible-jvm subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm type: feature request Issues requesting a new feature or capability subsystem: crucible-mir Issues related to Rust verification with crucible-mir and/or mir-json labels Sep 1, 2023
@RyanGlScott RyanGlScott mentioned this issue Sep 1, 2023
Closed
29 tasks
RyanGlScott added a commit that referenced this issue Sep 1, 2023
@RyanGlScott
Document that XGhostState is only defined for LLVM at the moment
5a47ded 
I've included a pointer to #1929 as well to indicate our intention to support
ghost state on other language backends.
@RyanGlScott RyanGlScott mentioned this issue Sep 1, 2023
Merged
@RyanGlScott
Copy link
Contributor Author

I'm not sure if it's straightforward to have a general-purpose ghost_value command. The current type of llvm_ghost_value is:

Ghost -> Term -> LLVMSetup ()

Presumably, a generic ghost_value command would have a type like:

Ghost -> Term -> m ()

Where m is allowed to be any of LLVMSetup, JVMSetup, or MIRSetup, but not TopLevel. I don't know how to write such a type in SAWScript, however.

In light of this, I think we should implement a combination of (1) and (2). That is, add a generic declare_ghost_state : String -> TopLevel Ghost command that works for all language backends (and deprecate llvm_declare_ghost_state), but have separate {llvm,jvm,mir}_ghost_value commands for each language backend that all do similar things.

RyanGlScott added a commit that referenced this issue Oct 13, 2023
@RyanGlScott
Add declare_ghost_state, deprecate llvm_declare_ghost_state
e2779ed 
We want to be able to declare ghost state in all SAW language backends, so we
now use a more general `declare_ghost_state` name for the command to reflect
this. The old `llvm_declare_ghost_state` command is now deprecated in favor of
`declare_ghost_state`.

This is one part of an eventual fix for #1929.
RyanGlScott added a commit that referenced this issue Oct 13, 2023
@RyanGlScott
Draft: Support ghost values in all language backends
67b4292 
Still TODO:

* Once the MIR backend supports overrides, the MIR backend needs to call the
  `executeGhost` function from `executeCond`, similarly to how the LLVM and
  JVM backends do currently.
* Add a MIR test case demonstrating that it works.

Fixes #1929.
@RyanGlScott RyanGlScott mentioned this issue Oct 13, 2023
Merged
RyanGlScott added a commit that referenced this issue Oct 16, 2023
@RyanGlScott
Add declare_ghost_state, deprecate llvm_declare_ghost_state
8abc01f 
We want to be able to declare ghost state in all SAW language backends, so we
now use a more general `declare_ghost_state` name for the command to reflect
this. The old `llvm_declare_ghost_state` command is now deprecated in favor of
`declare_ghost_state`.

This is one part of an eventual fix for #1929.
RyanGlScott added a commit that referenced this issue Oct 16, 2023
@RyanGlScott
Support ghost values in all language backends
8301b8c 
This patch:

* Factors out the machinery needed to track ghost state into
  into the `SAWScript.Crucible.Common.Override` and `SAWScript.Builtins`
  modules. Nothing about ghost state is specific to any language backend, so it
  deserves to live in a non-LLVM–specific location.
* Adds `jvm_ghost_value` and `mir_ghost_value` commands, which behave exactly
  like the LLVM backend's `llvm_ghost_value` command does, but for the JVM and
  MIR backends, respectively.
* Adds a `test_mir_ghost` test case in SAWScript and the remote API to ensure
  that everything works as expected.

Fixes #1929.
RyanGlScott added a commit that referenced this issue Oct 16, 2023
@RyanGlScott
Add declare_ghost_state, deprecate llvm_declare_ghost_state
310b39f 
We want to be able to declare ghost state in all SAW language backends, so we
now use a more general `declare_ghost_state` name for the command to reflect
this. The old `llvm_declare_ghost_state` command is now deprecated in favor of
`declare_ghost_state`.

This is one part of an eventual fix for #1929.
RyanGlScott added a commit that referenced this issue Oct 16, 2023
@RyanGlScott
Support ghost values in all language backends
c6ca304 
This patch:

* Factors out the machinery needed to track ghost state into
  into the `SAWScript.Crucible.Common.Override` and `SAWScript.Builtins`
  modules. Nothing about ghost state is specific to any language backend, so it
  deserves to live in a non-LLVM–specific location.
* Adds `jvm_ghost_value` and `mir_ghost_value` commands, which behave exactly
  like the LLVM backend's `llvm_ghost_value` command does, but for the JVM and
  MIR backends, respectively.
* Adds a `test_mir_ghost` test case in SAWScript and the remote API to ensure
  that everything works as expected.

Fixes #1929.
RyanGlScott added a commit that referenced this issue Oct 16, 2023
@RyanGlScott
Add declare_ghost_state, mark llvm_declare_ghost_state as legacy command
3ad4957 
We want to be able to declare ghost state in all SAW language backends, so we
now use a more general `declare_ghost_state` name for the command to reflect
this. The old `llvm_declare_ghost_state` command is now a legacy command whose
use is discouraged in favor of `declare_ghost_state`.

This is one part of an eventual fix for #1929.
RyanGlScott added a commit that referenced this issue Oct 16, 2023
@RyanGlScott
Support ghost values in all language backends
4232a42 
This patch:

* Factors out the machinery needed to track ghost state into
  into the `SAWScript.Crucible.Common.Override` and `SAWScript.Builtins`
  modules. Nothing about ghost state is specific to any language backend, so it
  deserves to live in a non-LLVM–specific location.
* Adds `jvm_ghost_value` and `mir_ghost_value` commands, which behave exactly
  like the LLVM backend's `llvm_ghost_value` command does, but for the JVM and
  MIR backends, respectively.
* Adds a `test_mir_ghost` test case in SAWScript and the remote API to ensure
  that everything works as expected.

Fixes #1929.
@RyanGlScott RyanGlScott mentioned this issue Nov 2, 2023
Closed
RyanGlScott added a commit that referenced this issue Nov 9, 2023
@RyanGlScott
Add declare_ghost_state, mark llvm_declare_ghost_state as legacy command
40b9966 
We want to be able to declare ghost state in all SAW language backends, so we
now use a more general `declare_ghost_state` name for the command to reflect
this. The old `llvm_declare_ghost_state` command is now a legacy command whose
use is discouraged in favor of `declare_ghost_state`.

This is one part of an eventual fix for #1929.
RyanGlScott added a commit that referenced this issue Nov 9, 2023
@RyanGlScott
Support ghost values in all language backends
0722394 
This patch:

* Factors out the machinery needed to track ghost state into
  into the `SAWScript.Crucible.Common.Override` and `SAWScript.Builtins`
  modules. Nothing about ghost state is specific to any language backend, so it
  deserves to live in a non-LLVM–specific location.
* Adds `jvm_ghost_value` and `mir_ghost_value` commands, which behave exactly
  like the LLVM backend's `llvm_ghost_value` command does, but for the JVM and
  MIR backends, respectively.
* Adds a `test_mir_ghost` test case in SAWScript and the remote API to ensure
  that everything works as expected.

Fixes #1929.
RyanGlScott added a commit that referenced this issue Nov 9, 2023
@RyanGlScott
Support ghost values in all language backends
8583a6d 
This patch:

* Factors out the machinery needed to track ghost state into
  the `SAWScript.Crucible.Common.Override` and `SAWScript.Builtins` modules.
  Nothing about ghost state is specific to any language backend, so it deserves
  to live in a non-LLVM–specific location.
* Adds `jvm_ghost_value` and `mir_ghost_value` commands, which behave exactly
  like the LLVM backend's `llvm_ghost_value` command does, but for the JVM and
  MIR backends, respectively.
* Adds a `test_mir_ghost` test case in SAWScript and the remote API to ensure
  that everything works as expected.

Fixes #1929.
RyanGlScott added a commit that referenced this issue Nov 23, 2023
@RyanGlScott
Add declare_ghost_state, mark llvm_declare_ghost_state as legacy command
7c36bef 
We want to be able to declare ghost state in all SAW language backends, so we
now use a more general `declare_ghost_state` name for the command to reflect
this. The old `llvm_declare_ghost_state` command is now a legacy command whose
use is discouraged in favor of `declare_ghost_state`.

This is one part of an eventual fix for #1929.
RyanGlScott added a commit that referenced this issue Nov 23, 2023
@RyanGlScott
Support ghost values in all language backends
7242895 
This patch:

* Factors out the machinery needed to track ghost state into
  the `SAWScript.Crucible.Common.Override` and `SAWScript.Builtins` modules.
  Nothing about ghost state is specific to any language backend, so it deserves
  to live in a non-LLVM–specific location.
* Adds `jvm_ghost_value` and `mir_ghost_value` commands, which behave exactly
  like the LLVM backend's `llvm_ghost_value` command does, but for the JVM and
  MIR backends, respectively.
* Adds a `test_mir_ghost` test case in SAWScript and the remote API to ensure
  that everything works as expected.

Fixes #1929.
@mergify mergify bot closed this as completed in #1958 Nov 28, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
subsystem: crucible-jvm Issues related to Java verification with crucible-jvm subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm subsystem: crucible-mir Issues related to Rust verification with crucible-mir and/or mir-json type: feature request Issues requesting a new feature or capability
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Support ghost values in all language backends GaloisInc/saw-script
1 participant
@RyanGlScott