search

smackers / smack

SMACK Software Verifier and Verification Toolchain
http://smackers.github.io
Other
432 stars 82 forks source link

Portfolio solving draft #762

Closed jmcmillan1 closed 3 years ago

jmcmillan1 commented 3 years ago

Right now a command line call like: smack --verifier=portfolio ./file.c should run 4 threads of corral verification on that "file.c" each with a combination of the args (eager_threshold=100, smt.arith.solver=2)

It is likely multiple print-outs will show verification results for processes which terminate close together in time, but the first terminating result is held and described

zvonimir commented 3 years ago

Ok, so something is weird with this pull request since it is trying to update the sea-dsa submodule of SMACK. My hunch is that you did not update submodules once you switch to the develop branch, and you added you commits to the develop branch with the old submodule. Could you please take a look at this? @keram88 can probably help you out here.

jmcmillan1 commented 3 years ago

You are right, the sea-dsa submodule was not updated after bringing in develop's changes, should be updated now

shaobo-he commented 3 years ago

Is this PR ready to be reviewed? I saw that it's still a draft.

shaobo-he commented 3 years ago

One tiny suggestion: we may want the parallel runs to be configurable. Namely, the user can supply a configuration file that specifies the options for each run. Currently, they are hardcoded.

The configuration file can be, e.g., a YAML file, like the following,

- verifier: corral
  options: /bopt:proverOpt:O:smt.qi.eager_threshold=100

- verifier: boogie
  options: /proverOpt:O:smt.arith.solver=2

Our portfolio solver can read this file and run each configuration in the list in parallel.

By default, we can generate a simple file that just contains verifier boogie and corral without any options.