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.

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

Add crucible_pointer_cast and deprecate crucible_points_to_untyped #930

Closed
andreistefanescu opened this issue Nov 23, 2020 · 3 comments · Fixed by #970
Closed

Add crucible_pointer_cast and deprecate crucible_points_to_untyped #930

andreistefanescu opened this issue Nov 23, 2020 · 3 comments · Fixed by #970
Assignees
Labels
subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm
Milestone

Comments

@andreistefanescu
Copy link
Contributor

Add crucible_pointer_cast : SetupValue -> LLVMType -> SetupValue and deprecate crucible_points_to_untyped. This would support the cases where crucible_points_to_untyped is needed, while still checking that the value argument of crucible_points_to has the intended user type.

@brianhuffman brianhuffman self-assigned this Nov 24, 2020
@brianhuffman brianhuffman added the subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm label Dec 3, 2020
@brianhuffman
Copy link
Contributor

Unfortunately it looks like this will require more work than I originally thought, and for a dumb reason. Basically, all I need to do is to add a new constructor to the haskell datatype that is used to represent the saw-script SetupValue type. However, the haskell SetupValue type is defined as a single generic parameterized type that is used in both the LLVM and JVM backends, so I can't simply add a constructor with an LLVM-specific argument type to it. Instead, I'll have to do a bunch of code refactoring first, to get rid of this abstraction boundary that was put in the wrong place.

@atomb atomb added this to the 0.8 milestone Dec 11, 2020
@brianhuffman
Copy link
Contributor

Another approach that would require much less work to implement would be to replace crucible_points_to_untyped with this:

crucible_points_to_at_type : SetupValue -> LLVMType -> SetupValue -> CrucibleSetup ()

Basically, crucible_points_to_at_type ptr ty val would be like crucible_points_to (crucible_pointer_cast ptr ty) val (if we had crucible_pointer_cast). Granted, crucible_points_to_at_type is slightly less flexible than crucible_pointer_cast, because you can't have a cast nested inside a pointer expression; but maybe that's not a big deal. Due to the way the code is organized, adding a new kind of points-to relation can be done with a much smaller change to the code than adding a new kind of SetupValue.

@andreistefanescu
Copy link
Contributor Author

@brianhuffman I like your idea! Let's add crucible_points_to_at_type/crucible_conditional_points_to_at_type for now.

brianhuffman pushed a commit that referenced this issue Dec 12, 2020
Also `crucible_conditional_points_to_at_type`.

Fixes #930.
brianhuffman pushed a commit that referenced this issue Jan 13, 2021
Also `crucible_conditional_points_to_at_type`.

Fixes #930.
brianhuffman pushed a commit that referenced this issue Jan 14, 2021
Also `crucible_conditional_points_to_at_type`.

Fixes #930.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm
Projects
None yet
Development

Successfully merging a pull request may close this issue.

3 participants