Allow user to specify CBMC's solver #2088

zhassan-aws · 2023-01-06T18:30:46Z

Description of changes:

Adds two methods that allow the user to select the solver to use with CBMC:

A new command-line --solver option
A kani::solver attribute

The kani::solver attribute allows selecting a different solver for each harness, e.g.

#[kani::proof]
#[kani::solver(kissat)]
fn check() { ... }

If the command-line --solver option is specified, it overrides the solver specified in the attribute (if any).

Valid values are kissat and minisat. Passing a custom SAT solver binary can be done with:

#[kani::solver(custom = "my_sat_solver")]

This case gets passed to CBMC's --external-sat-solver option directly.

Resolved issues:

Resolves #1656

Related RFC:

Optional #ISSUE-NUMBER.

Call-outs:

Testing:

How is this change tested? Added several tests
Is this a refactor change? No

Checklist

Each commit message has a non-empty body, explaining why the change was made
Methods or procedures are documented
Regression or unit tests are included, or existing tests cover the modified code
My PR is restricted to a single feature or bugfix

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

celinval · 2023-01-06T21:44:00Z

I would prefer if the attribute is based on an ID, not a path. I don't think it's a good practice to hardcode paths in the code, since it is hard to ensure that the path works for every developer and the CI.

To make this extensible for users that want to try something new that doesn't ship with Kani, I would prefer adding installation instructions, command line or a utility that configures a new engine via its path into a format / path that Kani expects.

zhassan-aws · 2023-01-07T00:00:53Z

I would prefer if the attribute is based on an ID, not a path. I don't think it's a good practice to hardcode paths in the code, since it is hard to ensure that the path works for every developer and the CI.

Point taken. A kani::solver attribute should be ID-based to support future plans of integrating multiple backends.

For the purposes of allowing the user to control CBMC's SAT solver specifically (which this PR is targeting), I can think of two options:

Introduce a CBMC-specific annotation, e.g. kani::cbmc_solver or even kani::cbmc_sat_solver where the argument would be kissat, cadical, etc.
Use kani::solver, and prefix each SAT solver option with cbmc (as we discussed offline), e.g. cbmc_kissat, cbmc_cadical, etc.

The advantage of option 1 is that it would keep the more valuable/more generic kani::solver attribute free, allowing us some time to design it based on future plans for integrating more backends.

The advantage of option 2 is that the user only needs to learn about one attribute for specifying the solver (i.e. fewer control knobs) which makes the usage simpler.

Thoughts?

rahulku · 2023-01-07T00:17:04Z

Option 2 sounds better.

celinval · 2023-01-07T00:49:37Z

Just a nit... maybe use "::" as a convention, it is also less likely that "::" will be in the same of a binary.

I was thinking, since we only have cbmc today, we could consider that things that an id that doesn't have "::" uses cbmc. I.e.: kani::solver("minisat") is the same as kani::solver("cbmc::minisat").

Another option would be to start with what you have, and once we add more options, we use key / value for the attribute. And we support the previous mode as legacy purpose. I.e.:
kani::solver("minisat") == kani::solver(engine="cbmc", sat_solver="minisat")

adpaco-aws · 2023-01-10T15:49:22Z

Thanks for pushing on this, @zhassan-aws !

Why are we adding a new attribute? We could just make engine and solver optional arguments in kani::proof, your example would look like this:

#[kani::proof(solver = kissat)]
fn check() { ... }

This idea comes from @fzaiser in #1656, and in my opinion is much cleaner than the other options considered here. It'd work in a similar way to @celinval 's last suggestion, assuming engine = cbmc and solver = minisat at the moment.

I don't think engines and solvers should be coupled in any of these options neither (i.e., things like cbmc_kissat or cbmc::kissat). Is there a technical reason for us to keep them that way? Even if newer backends only work with certain solvers, we can always limit these choices from Kani, but in principle we should aim for maximum flexibility.

zhassan-aws · 2023-01-11T23:44:08Z

Why are we adding a new attribute? We could just make engine and solver optional arguments in kani::proof:

I fully agree with making attributes arguments to kani::proof, and have proposed it in #1217.

jaisnan · 2023-01-31T17:53:49Z

Are we going in the direction of adding a new attribute vs attribute arguments?

zhassan-aws · 2023-01-31T17:55:33Z

Are we going in the direction of adding a new attribute vs attribute arguments?

We agreed that we will support both approaches.

celinval · 2023-01-31T18:26:15Z

I have a few comments regarding the UX from the PR description:

We should also accept minisat as a value.
We should create a --list-sovers that prints all the solvers known to Kani.
I was wondering if we should consider adding a --default-solver similar to the --default-unwind option.

zhassan-aws · 2023-01-31T18:30:25Z

We should also accept minisat as a value.

Make sense.

We should create a --list-sovers that prints all the solvers known to Kani.

Good idea.

I was wondering if we should consider adding a --default-solver similar to the --default-unwind option.

TBH, I don't like --default-unwind, and I haven't seen it being used much. The behavior that makes sense to me is that command-line options should override attributes.

celinval · 2023-01-31T18:40:06Z

We should also accept minisat as a value.

Make sense.

We should create a --list-sovers that prints all the solvers known to Kani.

Good idea.

I was wondering if we should consider adding a --default-solver similar to the --default-unwind option.

TBH, I don't like --default-unwind, and I haven't seen it being used much. The behavior that makes sense to me is that command-line options should override attributes.

Sounds good to me.

zhassan-aws · 2023-01-31T22:15:06Z

Added minisat in e426f79.

For --list-solvers, I just recalled that the help already displays the options:

$ kani --help
...
      --solver <SOLVER>
          Specify the CBMC solver to use. Overrides the harness `solver` attribute
          [possible values: "SAT solver binary", kissat, minisat]
...

Is this sufficient?

…o solver-attr

zhassan-aws · 2023-02-06T22:38:03Z

I don't think the arguments to the annotation should be strings.

I updated the PR to not use strings, e.g. #[kani::solver(kissat)]. Custom solver binaries can be specified using #[kani::solver(custom = "my_solver_binary")].

zhassan-aws · 2023-02-06T22:43:30Z

I do wonder if we should make a distinction between a builtin solver and a custom one. So:

Done. This only works for the attribute though, but not the command-line option :( It seems that to support passing --solver custom="solver_binary", we would need to parse the argument ourselves. In this case, we would lose the automatic listing of variants in the help message that strum provides.

adpaco-aws · 2023-02-06T23:07:58Z

I updated the PR to not use strings, e.g. #[kani::solver(kissat)]. Custom solver binaries can be specified using #[kani::solver(custom = "my_solver_binary")].

Thanks, @zhassan-aws !

One question: How would the user specify the solver in #[kani::proof(solver = ...)] if he wants to use a custom solver? I don't know if there's a syntax that'd support this case, since custom receives a string now, right?

zhassan-aws · 2023-02-06T23:10:46Z

How would the user specify the solver in #[kani::proof(solver = ...)] if he wants to use a custom solver?

I'm not sure :) We could perhaps do kani::proof(solver = custom("solver-binary")).

celinval

It looks good to me. Just some minor tweaks of the error messages.

celinval · 2023-02-07T18:30:51Z

kani-driver/src/call_cbmc.rs

+            CbmcSolver::Custom(custom_solver) => {
+                // Check if the specified binary exists in path
+                if which::which(custom_solver).is_err() {
+                    eprintln!(


I was wondering if we should merge this eprintln!() and the bail() statements. If you do want to keep them separate, can you please use util::error instead to print this message so we keep our formatting consistent?

I think we are using stdout there but you can change it if you prefer.

Removed the eprintln and moved its message to bail.

celinval · 2023-02-07T18:35:42Z

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

+                Some(CbmcSolver::Custom(lit.token_lit.symbol.to_string()))
+            }
+            _ => {
+                invalid_arg_err(attr);


Can you make this message more specific to the custom option?

This message is not specific to custom. It is emitted when the argument received is neither a MetaItemKind::Word or MetaItemKind::NameValue.

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

celinval · 2023-02-07T18:40:31Z

kani-driver/src/call_cbmc.rs

+                    eprintln!(
+                        "Error: The specified solver \"{custom_solver}\" was not found in path"
+                    );
+                    bail!("cbmc solver argument handling failed")


If you want to keep this separate from the error print, can you please make this more user friendly. Something like, "Custom solver resolution failed".

celinval · 2023-02-07T18:41:31Z

tests/ui/solver-attribute/no-arg/expected

+error: The `#[kani::solver]` attribute expects a single argument. Got 0 arguments.
+test.rs:5:1
+  |
+5 | #[kani::solver]


nit: remove the line number from the expected files and add "" to the end of each line.

…o solver-attr

adpaco-aws

Just a few comments about error messages.

I'd like us to iterate on the best option to pass the path for custom solvers. In my opinion, there shouldn't be any differences between the CLI and the annotation, which AFAIK is not true at the moment. But I don't want this to block the contribution since it's a special, non-required case for me.

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

adpaco-aws · 2023-02-07T20:09:52Z

kani_metadata/src/cbmc_solver.rs

+    Deserialize
+)]
+#[strum(serialize_all = "snake_case")]
+pub enum CbmcSolver {


What's the reason for this to be CbmcSolver and not just Solver?

Since the solver is currently specific for CBMC, and we're not yet clear on future plans, and whether this solver will apply to other engines as well, I added CBMC to its name.

I tend to agree with @adpaco-aws here, but this is an implementation detail that is internal to our code, so we can easily rename this later.

zhassan-aws · 2023-02-08T01:15:47Z

In my opinion, there shouldn't be any differences between the CLI and the annotation, which AFAIK is not true at the moment.

I implemented a clap parser for the --solver option, so that we allow --solver kissat, --solver minisat, or --solver custom=<any-binary>. I added a couple of tests for it.

@celinval this is something that you have requested as well.

adpaco-aws

Thanks, @zhassan-aws ! Looks great overall, just a few suggestions 😄

kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

kani-driver/src/args.rs

kani-driver/src/call_cbmc.rs

kani_metadata/src/cbmc_solver.rs

library/kani_macros/src/lib.rs

tests/perf/btreeset/insert_same/src/main.rs

Co-authored-by: Adrian Palacios <[email protected]>

celinval

It looks good. Just please remove the remaining line numbers from the expected tests.

celinval · 2023-02-08T18:12:24Z

tests/ui/solver-attribute/invalid/expected

+  |\
+5 | #[kani::solver(123)]\
+  | ^^^^^^^^^^^^^^^^^^^^


Removing the line number:

Suggested change

|\

5 | #[kani::solver(123)]\

| ^^^^^^^^^^^^^^^^^^^^

|\

| #[kani::solver(123)]\

| ^^^^^^^^^^^^^^^^^^^^

celinval · 2023-02-08T18:13:12Z

tests/ui/solver-attribute/multiple-args/expected

+  |\
+5 | #[kani::solver(kissat, minisat)]\
+  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^


Suggested change

|\

5 | #[kani::solver(kissat, minisat)]\

| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

|\

| #[kani::solver(kissat, minisat)]\

| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

celinval · 2023-02-08T18:14:38Z

tests/ui/solver-attribute/multiple-attrs/expected

+  |\
+5 | #[kani::solver(kissat)]\
+  | ^^^^^^^^^^^^^^^^^^^^^^^


Suggested change

|\

5 | #[kani::solver(kissat)]\

| ^^^^^^^^^^^^^^^^^^^^^^^

|\

| #[kani::solver(kissat)]\

| ^^^^^^^^^^^^^^^^^^^^^^^

celinval · 2023-02-08T18:15:05Z

tests/ui/solver-attribute/no-arg/expected

+  |\
+5 | #[kani::solver]\
+  | ^^^^^^^^^^^^^^^


Suggested change

|\

5 | #[kani::solver]\

| ^^^^^^^^^^^^^^^

|\

| #[kani::solver]\

| ^^^^^^^^^^^^^^^

celinval · 2023-02-08T18:15:29Z

tests/ui/solver-attribute/unknown/expected

+  |\
+5 | #[kani::solver(foo)]\
+  | ^^^^^^^^^^^^^^^^^^^^


Suggested change

|\

5 | #[kani::solver(foo)]\

| ^^^^^^^^^^^^^^^^^^^^

|\

| #[kani::solver(foo)]\

| ^^^^^^^^^^^^^^^^^^^^

zhassan-aws force-pushed the solver-attr branch 2 times, most recently from 84adc14 to 97b40f8 Compare January 6, 2023 18:37

zhassan-aws mentioned this pull request Jan 7, 2023

Include Kissat in the Kani bundle #2087

Merged

4 tasks

zhassan-aws added 2 commits January 26, 2023 18:51

Add a kani::solver attribute to allow specifying a SAT solver

38d0292

Add a list of registered CBMC solvers that Kani knows how to handle

1d3738c

zhassan-aws force-pushed the solver-attr branch from 97b40f8 to 1d3738c Compare January 27, 2023 19:48

zhassan-aws changed the title ~~Add a kani::solver attribute to allow specifying a SAT solver~~ Allow specifying the CBMC SAT solver Jan 27, 2023

zhassan-aws changed the title ~~Allow specifying the CBMC SAT solver~~ Allow user to specify CBMC's solver Jan 27, 2023

Format

f8720c2

zhassan-aws marked this pull request as ready for review January 27, 2023 19:59

zhassan-aws requested a review from a team as a code owner January 27, 2023 19:59

zhassan-aws added 3 commits January 31, 2023 14:11

Add minisat to the list of solvers

e426f79

Merge branch 'main' into solver-attr

73cdf49

Merge branch 'main' into solver-attr

da917fb

zhassan-aws requested a review from adpaco-aws February 1, 2023 00:05

zhassan-aws added 3 commits January 31, 2023 22:50

Merge branch 'main' into solver-attr

a2635c7

Clarify solver help message

d86882c

Merge branch 'solver-attr' of https://github.com/zhassan-aws/kani int…

11af24b

…o solver-attr

Clippy fix

cd8ecbb

zhassan-aws added 2 commits February 6, 2023 14:49

Fix format

8b9992f

Fix argument

0dde227

Merge branch 'main' into solver-attr

640500b

celinval reviewed Feb 7, 2023

View reviewed changes

zhassan-aws added 2 commits February 7, 2023 11:30

Address PR comments

51d98d0

Merge branch 'solver-attr' of https://github.com/zhassan-aws/kani int…

f5e34b7

…o solver-attr

adpaco-aws reviewed Feb 7, 2023

View reviewed changes

zhassan-aws added 3 commits February 7, 2023 14:16

Start error messages with lowercase

fb9bab7

Implement a clap parser for CbmcSolver

f5e3e5a

Merge branch 'main' into solver-attr

e05bd9b

Clippy fix

7210132

adpaco-aws approved these changes Feb 8, 2023

View reviewed changes

zhassan-aws and others added 6 commits February 8, 2023 07:53

Apply suggestions from code review

947da6d

Co-authored-by: Adrian Palacios <[email protected]>

Apply suggestions from code review

3b0915f

Co-authored-by: Adrian Palacios <[email protected]>

Update kani-compiler/src/codegen_cprover_gotoc/codegen/function.rs

077d94e

Co-authored-by: Adrian Palacios <[email protected]>

Update test

da808d5

Merge branch 'main' into solver-attr

841134c

Merge branch 'main' into solver-attr

74cc438

danielsn merged commit 4dfff36 into model-checking:main Feb 8, 2023

celinval reviewed Feb 8, 2023

View reviewed changes

zhassan-aws added a commit to zhassan-aws/kani that referenced this pull request Feb 8, 2023

Address missed comments from model-checking#2088

04d41d4

zhassan-aws mentioned this pull request Feb 8, 2023

Address missed comments from #2088 #2200

Merged

3 tasks

zhassan-aws added a commit that referenced this pull request Feb 8, 2023

Address missed comments from #2088 (#2200)

d0a4d9b

zhassan-aws deleted the solver-attr branch February 8, 2023 19:32

Allow user to specify CBMC's solver #2088

Allow user to specify CBMC's solver #2088

Uh oh!

Conversation

zhassan-aws commented Jan 6, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description of changes:

Resolved issues:

Related RFC:

Call-outs:

Testing:

Checklist

Uh oh!

celinval commented Jan 6, 2023

Uh oh!

zhassan-aws commented Jan 7, 2023

Uh oh!

rahulku commented Jan 7, 2023

Uh oh!

celinval commented Jan 7, 2023

Uh oh!

adpaco-aws commented Jan 10, 2023

Uh oh!

zhassan-aws commented Jan 11, 2023

Uh oh!

jaisnan commented Jan 31, 2023

Uh oh!

zhassan-aws commented Jan 31, 2023

Uh oh!

celinval commented Jan 31, 2023

Uh oh!

zhassan-aws commented Jan 31, 2023

Uh oh!

celinval commented Jan 31, 2023

Uh oh!

zhassan-aws commented Jan 31, 2023

Uh oh!

zhassan-aws commented Feb 6, 2023

Uh oh!

zhassan-aws commented Feb 6, 2023

Uh oh!

adpaco-aws commented Feb 6, 2023

Uh oh!

zhassan-aws commented Feb 6, 2023

Uh oh!

celinval left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

adpaco-aws left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

zhassan-aws commented Feb 8, 2023

Uh oh!

adpaco-aws left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

zhassan-aws commented Jan 6, 2023 •

edited

Loading