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

[Experimental] skeleton_globals_post and return value postconditions? #1810

Open
WeeknightMVP opened this issue Feb 3, 2023 · 1 comment
Labels
subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm type: feature request Issues requesting a new feature or capability
Milestone

Comments

@WeeknightMVP
Copy link

WeeknightMVP commented Feb 3, 2023

The following creates a "boilerplate" SAW specification from LLVM bitcode, e.g. Salsa20.bc:

enable_experimental;
MODULE <- ".../salsa20.bc";
MODULE_SKEL <- module_skeleton MODULE;
llvm_boilerplate "salsa20_boilerplate.saw" MODULE_SKEL true;
enable_experimental;
MODULE <- ".../salsa20.bc";  // non-boilerplate inserted here
MODULE_SKEL <- module_skeleton MODULE;

rotl_skel <- function_skeleton MODULE_SKEL "rotl";
let rotl_spec = do {
  skeleton_globals_pre MODULE_SKEL;
  prestate <- skeleton_prestate rotl_skel;
  skeleton_exec prestate;
  poststate <- skeleton_poststate rotl_skel prestate;
  skeleton_globals_post MODULE_SKEL;
};
rotl_override <- llvm_verify MODULE "rotl" [] false rotl_spec z3;

// ...

Attempting to verify rotl fails at this point because the C operator << (over uint_32) requires a precondition that {{ 0 < shift /\ shift < 32 }} to avoid undefined behavior...

let rotl_spec : LLVMSetup () = do {
  skeleton_globals_pre MODULE_SKEL;
  prestate <- skeleton_prestate rotl_skel;

  // non-boilerplate
  shift <- skeleton_arg prestate "shift";
  llvm_precond {{ 0 < shift /\ shift < 32 }};

  skeleton_exec prestate;

  poststate <- skeleton_poststate rotl_skel prestate;
  skeleton_globals_post MODULE_SKEL;
};

Verifying this skeleton spec succeeds, but does not reflect a postcondition that rotl returns value <<< shift:

let rotl_spec : LLVMSetup () = do {
  skeleton_globals_pre MODULE_SKEL;
  prestate <- skeleton_prestate rotl_skel;

  // non-boilerplate
  shift <- skeleton_arg prestate "shift";
  value <- skeleton_arg prestate "value";
  llvm_precond {{ 0 < shift /\ shift < 32 }};

  skeleton_exec prestate;
  poststate <- skeleton_poststate rotl_skel prestate;

  // non-boilerplate
  llvm_return (llvm_term {{ value <<< shift }});

  skeleton_globals_post MODULE_SKEL;
};
$ saw --version
0.9
$ saw salsa20_boilerplate.saw
[23:49:01.252] Loading file "salsa20_boilerplate.saw"
[23:49:01.356] FunctionSkeleton {_funSkelName = "rotl", _funSkelLoc = Nothing, _funSkelArgs = [ArgSkeleton {_argSkelName = Just "value", _argSkelLoc = Just (Location {_locationLine = 6, _locationColumn = Just 31}), _argSkelType = TypeSkeleton {_typeSkelLLVMType = PrimType (Integer 32), _typeSkelIsPointer = False, _\
typeSkelSizeGuesses = []}},ArgSkeleton {_argSkelName = Just "shift", _argSkelLoc = Just (Location {_locationLine = 6, _locationColumn = Just 42}), _argSkelType = TypeSkeleton {_typeSkelLLVMType = PrimType (Integer 32), _typeSkelIsPointer = False, _typeSkelSizeGuesses = []}}], _funSkelRet = TypeSkeleton {_typeSkelLL\
VMType = PrimType (Integer 32), _typeSkelIsPointer = False, _typeSkelSizeGuesses = []}, _funSkelCalls = fromList []}
[23:49:01.474] Stack trace:
"llvm_verify" (salsa20_boilerplate.saw:21:3-21:14):
"rotl_spec" (salsa20_boilerplate.saw:21:39-21:48):
"llvm_return" (salsa20_boilerplate.saw:14:3-14:14):
crucible_return: duplicate return value specification

Per #668, adding a postcondition on function arguments is straightforward, but can one specify a return value alongside skeleton_globals_post?

@chameco
Copy link
Contributor

chameco commented Feb 9, 2023

I don't believe there's a way to specify the return value currently, but I suspect it would be straightforward to add. Do you have a particular use-case in mind where the boilerplate generation feature would be helpful? I don't think we've used it very much at Galois (maybe once or twice), and I suspect some elements of the design aren't very well-considered.

@sauclovian-g sauclovian-g added subsystem: crucible-llvm Issues related to LLVM bitcode verification with crucible-llvm type: feature request Issues requesting a new feature or capability labels Nov 5, 2024
@sauclovian-g sauclovian-g added this to the Someday milestone Nov 5, 2024
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 type: feature request Issues requesting a new feature or capability
Projects
None yet
Development

No branches or pull requests

3 participants