Introduce native kani / cargo-kani #738

tedinski · 2022-01-08T01:44:31Z

Description of changes:

This is a port of our python/bash scripts to native Rust implementations.

There are two entry points to the binary: kani and cargo-kani.
Argument parsing is in arg.rs
We set up a KaniSession from session.rs to serve as the ambient background data/state for an execution.
All calls out to other binaries are organized around call_*.rs files.

Major TODOs:

I need to double check the behavior for cargo-kani --visualize
I need to audit the old code to be sure I know everything that's been dropped that major.

Currently known to be missing:

--gen-c-runnable (producing --symbol-table-passes)
"unwind tip" (we should do this over using the new output parsing code instead of what we did previously, possibly create an issue to track this)
Checking for dependencies in PATH (we should install them instead)

Resolved issues:

some progress should be entered into the major tracking issue cargo-rmc tracking issue #701
I believe this fixes cargo-rmc tests fail if we do not add $(pwd) to --build-base #755. I'm not sure how to interpret that issue, but I think we switch to changing the directory that cargo gets called in, which maybe resolves that issue?

Call-outs:

Testing:

How is this change tested? existing regressions
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.

…g#722 yet)

celinval

I took a quick look. It's a nice start! Thanks for doing this. Here are a few suggestions:

I think it would be cleaner if we create two modules, one that does the external calls and one that does the parsing. You might as well split the objects too.
Can you also add a bit more documentation to the files and functions?

celinval · 2022-01-21T18:34:08Z

src/cargo-kani/src/call_cargo.rs

+
+use crate::context::KaniContext;
+
+impl KaniContext {


Does this need to be inside KaniContext?

Yep, it's using self a lot. (Was even back when you asked, but perhaps only once then. Much more obvious now we have all the flags.)

This is a general comment and I think we should address in a separate PR, but I would prefer breaking some of this logic down into more than one struct. I think it would be cleaner if we had smaller structs. We are using self a lot, and that could possible be broken down by calling other objects.

celinval · 2022-01-21T20:49:39Z

src/cargo-kani/src/call_goto_cc.rs

+    /// Given a `file` (a .symtab.json), produce `{file}.out` by calling symtab2gb
+    pub fn link_c_lib(&self, inputs: &[PathBuf], output: &Path, function: &str) -> Result<()> {
+        {
+            let mut temps = self.temporaries.borrow_mut();


Why borrow_mut? Shouldn't self be mutable? Or can we manage temporaries outside of KaniContext?

I'm making use of RefCell to let us pass around just a &self (not mut, so we don't need exclusivity), but then still update the list of temporaries.

celinval · 2022-01-21T21:24:55Z

src/cargo-kani/src/context.rs

+
+    pub fn kani_rustc(&self) -> Result<PathBuf> {
+        match self {
+            Self::DevRepo(repo) => {


Can you create a utility function? This seemed to be repeated in the functions bellow.

(same as earlier comment: I'll fix it once we have another install type?)

src/cargo-kani/src/context.rs

celinval · 2022-01-21T21:27:21Z

src/cargo-kani/src/context.rs

+}
+
+/// Represents where we detected Kani, with helper methods for using that information to find critical paths
+enum InstallType {


Why do we need this? Can we use a build.rs instead?

This is the code to dynamic detect where all our dependencies are located at runtime. It looks weird right now because I'm not trying to support anything except "checked out repo, globally installed deps" except I was trying to still support a better structure later...

I'll refactor it later if you think we can tolerate it for now. As soon at we actually have another install type this should either become clear or get fixed...

src/cargo-kani/src/context.rs

src/cargo-kani/src/call_single_file.rs

src/cargo-kani/src/call_goto_instrument.rs

celinval · 2022-02-09T07:30:03Z

src/cargo-kani/src/args.rs

+
+#[derive(Debug, StructOpt)]
+pub struct CheckArgs {
+    // Rust argument parsers (/clap) don't have the convenient '--flag' and '--no-flag' boolean pairs, so approximate


Do we need them?

We currently have two "modes": --default-checks where you write --no-blah-checks for specific categories. Or --no-default-checks where you write --blah-checks for specific categories. I'm supporting that for now. We could revisit eventually?

I am in favor of revisiting. This seems to be adding unnecessary complexity and it doesn't seem to be a common practice in rust anyway.

tedinski · 2022-02-15T20:52:33Z

src/cargo-kani/src/args.rs

+
+#[derive(Debug, StructOpt)]
+pub struct CheckArgs {
+    // Rust argument parsers (/clap) don't have the convenient '--flag' and '--no-flag' boolean pairs, so approximate


We currently have two "modes": --default-checks where you write --no-blah-checks for specific categories. Or --no-default-checks where you write --blah-checks for specific categories. I'm supporting that for now. We could revisit eventually?

tedinski · 2022-02-15T20:53:36Z

src/cargo-kani/src/call_cargo.rs

+
+use crate::context::KaniContext;
+
+impl KaniContext {


Yep, it's using self a lot. (Was even back when you asked, but perhaps only once then. Much more obvious now we have all the flags.)

tedinski · 2022-02-15T20:57:29Z

src/cargo-kani/src/call_goto_cc.rs

+    /// Given a `file` (a .symtab.json), produce `{file}.out` by calling symtab2gb
+    pub fn link_c_lib(&self, inputs: &[PathBuf], output: &Path, function: &str) -> Result<()> {
+        {
+            let mut temps = self.temporaries.borrow_mut();


I'm making use of RefCell to let us pass around just a &self (not mut, so we don't need exclusivity), but then still update the list of temporaries.

tedinski · 2022-02-15T20:59:49Z

src/cargo-kani/src/context.rs

+}
+
+/// Represents where we detected Kani, with helper methods for using that information to find critical paths
+enum InstallType {


This is the code to dynamic detect where all our dependencies are located at runtime. It looks weird right now because I'm not trying to support anything except "checked out repo, globally installed deps" except I was trying to still support a better structure later...

I'll refactor it later if you think we can tolerate it for now. As soon at we actually have another install type this should either become clear or get fixed...

tedinski · 2022-02-15T21:02:06Z

src/cargo-kani/src/context.rs

+
+    pub fn kani_rustc(&self) -> Result<PathBuf> {
+        match self {
+            Self::DevRepo(repo) => {


(same as earlier comment: I'll fix it once we have another install type?)

tedinski · 2022-02-15T21:03:44Z

tests/cargo-kani/simple-config-toml/Cargo.toml

-[kani.flags.loudness]
-quiet = false
-
-[kani.flags.artifacts.extra.suffixes]


Just a note for anyone reviewing: these things under kani.flags were pointless and I'm not sure why they were ever there. So I removed these "sections" that shouldn't be there.

Also, I removed --no-quiet and --no-visualize and mangler as options, so I removed those here too.

tedinski · 2022-02-15T21:04:53Z

tools/compiletest/src/runtest.rs

-            .arg(&parent_dir);
+            .current_dir(&parent_dir);


I removed the --crate flag in favor of just changing directories here.

tedinski · 2022-02-15T21:05:15Z

tools/compiletest/src/runtest.rs

-        kani.args(&self.props.kani_flags)
-            .arg("--input")
-            .arg(&self.testpaths.file)
+        kani.arg(&self.testpaths.file)


I removed the --input flag in favor of just passing the argument here.

…checks

celinval

A few more comments. I'm OK leaving the comments related to polishing the code to a separate PR.

celinval · 2022-02-18T22:45:06Z

src/cargo-kani/src/args_toml.rs

+/// Produces a set of arguments to pass to "self" (cargo-kani) from a Cargo.toml project file
+pub fn config_toml_to_args() -> Result<Vec<OsString>> {
+    // TODO: `cargo locate-project` maybe?
+    let file = std::fs::read_to_string("Cargo.toml");


Don't we need to handle --config-toml option?

Nothing is using that flag, so I dropped it.

src/cargo-kani/src/main.rs

src/cargo-kani/src/call_cargo.rs

celinval · 2022-02-18T23:24:30Z

src/cargo-kani/src/main.rs

+    ctx.run_goto_instrument(&linked_obj)?;
+
+    if ctx.args.visualize {
+        ctx.run_visualize(&linked_obj, "target/report")?;


Can you please use PathBuf?

celinval · 2022-02-18T23:26:57Z

src/cargo-kani/src/args.rs

+    // TODO: currently only cargo-kani pays attention to this.
+    /// Directory for all generated artifacts
+    #[structopt(long, parse(from_os_str))]
+    pub target_dir: Option<PathBuf>,


Is it possible to set a default value here to avoid hard coding the default value in other places?

No: the default is different for standalone/cargo. The "hard coding in other places" is just the two different defaults.

I agree there's a design problem there, but it's not an obvious one to fix. I've deliberately avoided letting a KaniSession know if it's cargo-kani or kani because it's just supposed to represent the flags, but here's an area where it matters, and it gets a little annoying.

src/cargo-kani/src/args.rs

celinval · 2022-02-18T23:33:21Z

src/cargo-kani/src/args.rs

+// Common arguments for invoking Kani. This gets put into KaniContext, whereas
+// anything above is "local" to "main"'s control flow.
+#[derive(Debug, StructOpt)]
+pub struct KaniArgs {


What is the output for kani --help after this change?

Right now a big jumbled mess:

$ cargo-kani --help cargo-kani 0.1.0 Verify a Rust crate. For more information, see https://github.com/model-checking/kani USAGE: cargo-kani [FLAGS] [OPTIONS] FLAGS: --allow-cbmc-verification-failure Do not produce error return code on CBMC verification failure --assertion-reach-checks Turn on assertion reachability checks --auto-unwind Turn on automatic loop unwinding --debug Produce full debug information --default-checks Turn on all default checks --dry-run Print commands instead of running them --gen-c Generate C file equivalent to inputted program -h, --help Prints help information --keep-temps Keep temporary files generated throughout Kani process --memory-safety-checks Turn on default memory safety checks --no-default-checks Turn off all default checks --no-memory-safety-checks Turn off default memory safety checks --no-overflow-checks Turn off default overflow checks --no-restrict-vtable Disable restricting the targets of virtual table function pointer calls --no-undefined-function-checks Turn off undefined function checks --no-unwinding-checks Turn off default unwinding checks --only-codegen Kani will only compile the crate --overflow-checks Turn on default overflow checks -q, --quiet Produces no output, just an exit code and requested artifacts; overrides --verbose --restrict-vtable Restrict the targets of virtual table function pointer calls --tests Enable test function verification. Only use this option when the entry point is a test function --undefined-function-checks Turn on undefined function checks --unwinding-checks Turn on default unwinding checks --use-abs Use abstractions for the standard library -V, --version Prints version information -v, --verbose Output processing stages and commands, along with minor debug information --visualize Generate visualizer report to <target-dir>/report/html/index.html OPTIONS: --abs-type <abs-type> Choose abstraction for modules of standard library if available [default: std] [possible values: std, kani, c-ffi, no-back] --c-lib <c-lib>... Link external C files referenced by Rust code --cbmc-args <cbmc-args>... Pass through directly to CBMC; must be the last flag --function <function> Entry point for verification [default: main] --object-bits <object-bits> Specify the number of bits used for representing object IDs in CBMC [default: 16] --output-format <output-format> Toggle between different styles of output [default: regular] [possible values: Regular, Terse, Old] --target-dir <target-dir> Directory for all generated artifacts --unwind <unwind> Specify the value used for loop unwinding in CBMC

IMO, cleaning it up is another PR.

Interesting. It uses the doc comments to generate the help information. It is clean but a bit error prone.

This is a topic for the next PR though. Thanks

celinval · 2022-02-18T23:39:01Z

src/cargo-kani/src/call_single_file.rs

+            let mut temps = self.temporaries.borrow_mut();
+            temps.push(output_filename.clone());
+            temps.push(alter_extension(file, "type_map.json"));
+            temps.push(alter_extension(file, "kani-metadata.json"));


Can we create a little utility class to generate these extensions for us? Another alternative is to create a constant for each type of extension. I noticed that they are hard-coded in different places.

While they're hardcoded, they each appear exactly once (except "restrictions.json" which is a design flaw I might try to correct now...)

Ok. Maybe once you merge this I can add a little utility module that can be used by kani / cargo-kani and the kani-compiler.

celinval

I think I am OK signing off this PR the way it is since it is a clear improvement to what we have today. Thanks for that.

What's your plan to address the issues that we are leaving for follow up PRs though?

Some things like improving the --help output I think is high priority but I also see a lot of TODO statements that don't have any issue attached to them. There are also a lot of comments here that are going to be pushed to follow up PRs.

celinval · 2022-02-22T21:23:55Z

src/cargo-kani/src/args.rs

+// Common arguments for invoking Kani. This gets put into KaniContext, whereas
+// anything above is "local" to "main"'s control flow.
+#[derive(Debug, StructOpt)]
+pub struct KaniArgs {


Interesting. It uses the doc comments to generate the help information. It is clean but a bit error prone.

This is a topic for the next PR though. Thanks

src/cargo-kani/src/args_toml.rs

celinval · 2022-02-22T21:42:23Z

src/cargo-kani/src/args_toml.rs

+}
+
+/// Translates one toml entry into arguments and inserts it into args
+fn insert_arg_from_toml(flag: &str, value: &Value, args: &mut Vec<OsString>) -> Result<()> {


I have a question, what will happen if the user invokes cargo-kani with an argument in the command line that is also included in the Cargo.toml?

It should be the same thing as happens on the command line so:

$ cargo-kani --verbose --verbose error: The argument '--verbose' was provided more than once, but cannot be used multiple times USAGE: cargo-kani --abs-type <abs-type> --function <function> --object-bits <object-bits> --output-format <output-format> --verbose For more information try --help

The command line argument should take precedence over the cargo configuration though. Like it does today. I believe this works today because the python implementation allows you to use an argument more than once.

On clap you can set the following setting AllArgsOverrideSelf to enable that behavior.

src/cargo-kani/src/args_toml.rs

celinval · 2022-02-22T21:53:17Z

scripts/cbmc_json_parser.py

        print("Json File Input Missing")
        sys.exit(1)

+    if len(sys.argv) == 3:


Maybe @jaisnan can improve this logic a bit once you merge. I believe he only created the main in order to run some sanity checks.

tedinski · 2022-02-24T19:37:18Z

I combed the PR and updated #701 with all follow up issues we've mentioned.

celinval

Can you please add to your TODO list that command line arguments should take precedence over flags on Cargo.toml?

Thanks

…nal error message

celinval

Good catch

celinval · 2022-02-24T21:31:04Z

src/cargo-kani/src/main.rs

    } else {
-        ctx.run_cbmc(&linked_obj)?;
+        let result = ctx.run_cbmc(&linked_obj)?;
+        if result == VerificationStatus::Failure {


Nit: next time you can use if let

Introduce native rmc / cargo-rmc

98a27df

adpaco-aws mentioned this pull request Jan 11, 2022

Intrinsics Audit #727

Closed

tedinski added 4 commits January 18, 2022 22:26

merge origin/main

aac1f63

rename to cargo-kani (not yet working, must account for model-checkin…

2dfa3d2

…g#722 yet)

adapt to new kani-compiler

eb1f190

Merge remote-tracking branch 'origin/main' into native-rmc

4744016

celinval reviewed Jan 21, 2022

View reviewed changes

tedinski added 12 commits January 28, 2022 22:09

merge origin/main

095e8ce

add support for various output modifier flags

fe77718

add enable/disable flags for cbmc checks

7573df5

implement more flags

023ecfa

add cbmc arguments

f1654f9

Merge remote-tracking branch 'origin/main' into native-rmc

7fa5510

add gen-c

1cb4295

add output-format

54ab877

support use-abs and abs-type

4e13da7

merge origin/main

a7c3e9d

update debug flag mechanism

044478d

add vtable restrictions code

03afcc6

celinval reviewed Feb 9, 2022

View reviewed changes

tedinski added 7 commits February 9, 2022 21:45

Merge remote-tracking branch 'origin/main' into native-rmc

8cb97de

Switch to native, delete the python

a05a163

Merge remote-tracking branch 'origin/main' into native-rmc

a934769

Merge remote-tracking branch 'origin/main' into native-rmc

2767f4a

add symbol mangling, stratify arguments

912dfdf

use python3

c2b7ddb

use correct build triple

2b672ae

tedinski commented Feb 15, 2022

View reviewed changes

tedinski added 2 commits February 15, 2022 21:18

clean up some comments

636e4c7

Rename KaniContext -> KaniSession

c69c2ff

tedinski mentioned this pull request Feb 18, 2022

Unwind tip (+ unsupported tip?) #839

Closed

5 tasks

tedinski added 2 commits February 18, 2022 20:49

fail based on 'formatter' result alone. Accomodates the reachability …

15f4aa4

…checks

move toml code to its own file, it didn't belong where it was

79c1e0c

celinval reviewed Feb 18, 2022

View reviewed changes

jaisnan mentioned this pull request Feb 21, 2022

Add a parameter (default off) to run_cmd to control whether to run the CBMC output parser #849

Merged

4 tasks

tedinski added 5 commits February 21, 2022 23:01

merge origin/main

1704c54

pathbuf and error checks

bd7de7b

introduce aggregate return type for kani outputs

5acf2e4

introduce aggregate return type for cargo-kani outputs

8e3ea09

Merge remote-tracking branch 'origin/main' into native-rmc

bd73faf

celinval reviewed Feb 22, 2022

View reviewed changes

tedinski added 2 commits February 24, 2022 18:52

rename descend to get_table

42491ef

Merge remote-tracking branch 'origin/main' into native-rmc

931e804

tedinski mentioned this pull request Feb 24, 2022

cargo-rmc tracking issue #701

Closed

30 tasks

celinval approved these changes Feb 24, 2022

View reviewed changes

tedinski added 2 commits February 24, 2022 20:02

allow repeated arguments

b00eb42

Detect verification failure and exit appropriately without an additio…

526a666

…nal error message

celinval reviewed Feb 24, 2022

View reviewed changes

Merge branch 'main' into native-rmc

cc01c3f

tedinski merged commit 2840208 into model-checking:main Feb 24, 2022

tedinski deleted the native-rmc branch February 24, 2022 21:56

tedinski mentioned this pull request Feb 24, 2022

--visualize and --output-format don't play well together #820

Closed

This was referenced Feb 24, 2022

Running --visualize still includes unnecessary CBMC checks in coverage run #368

Closed

Add unwind tip to CBMC result parser script #866

Merged

adpaco-aws mentioned this pull request Mar 1, 2022

All bookrunner examples show verification failures #876

Closed

tedinski added a commit to tedinski/rmc that referenced this pull request Apr 26, 2022

Introduce native kani / cargo-kani (model-checking#738)

2419294

tedinski added a commit that referenced this pull request Apr 27, 2022

Introduce native kani / cargo-kani (#738)

63935f6

Introduce native kani / cargo-kani #738

Introduce native kani / cargo-kani #738

Uh oh!

Conversation

tedinski commented Jan 8, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Description of changes:

Resolved issues:

Call-outs:

Testing:

Checklist

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!

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!

Uh oh!

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!

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!

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!

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!

Uh oh!

Uh oh!

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!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

tedinski commented Jan 8, 2022 •

edited

Loading