Add option to run CBMC sanity checks + set is_param for function parameters #1387
Conversation
This will ensure the gotoc model we generate is valid. Surprisingly, we fail at that in many places today.
I am not aware of any verification issue from missing this flag, but but it is expected in a well formed iRep according to the sanity checks in CBMC. This is blocking us from enable those sanity checks so I'm fixing them now.
We are still seeing issues with `memcmp` in the regression. Disable the sanity checks in the regression for now but allow them to be run manually.
| @@ -130,6 +134,16 @@ impl KaniSession { | |||
| self.call_goto_instrument(args) | |||
| } | |||
|
|
|||
| fn goto_sanity_check(&self, file: &Path) -> Result<()> { | |||
There was a problem hiding this comment.
This seems to be running it twice, when we're already doing it with the cbmc args?
There was a problem hiding this comment.
Yeah. I figured it's a cheap analysis, so we might as well run before any goto-instrument optimization and right before verification.
There was a problem hiding this comment.
that said, I totally misplaced it. Let me move it up.
| @@ -153,7 +159,8 @@ impl<'tcx> GotocCtx<'tcx> { | |||
| loc: Location, | |||
| ) -> (Expr, Stmt) { | |||
| let c = self.current_fn_mut().get_and_incr_counter(); | |||
| let var = self.gen_stack_variable(c, &self.current_fn().name(), "temp", t, loc).to_expr(); | |||
| let var = | |||
| self.gen_stack_variable(c, &self.current_fn().name(), "temp", t, loc, false).to_expr(); | |||
There was a problem hiding this comment.
could/should this use gen_function_local_variable?
There was a problem hiding this comment.
I believe so. We would just need to add is_hidden parameter to that function.
There was a problem hiding this comment.
Oh, a proliferation of boolean arguments isn't good either. Maybe ignore my comment here, or consider a "gen_hidden_local_variable" function or something like that.
There was a problem hiding this comment.
Sorry, I thought you were talking about the explicit Symbol::variable call in function.rs.
This does name variables "temp" instead of "var". I would rather not change that in this PR if that's OK for you.
| @@ -58,7 +67,8 @@ impl<'tcx> GotocCtx<'tcx> { | |||
| let loc = self.codegen_span(&ldata.source_info.span); | |||
| let sym = | |||
| Symbol::variable(name, base_name, t, self.codegen_span(&ldata.source_info.span)) | |||
| .with_is_hidden(!ldata.is_user_variable()); | |||
| .with_is_hidden(!ldata.is_user_variable()) | |||
| .with_is_parameter(idx > 0 && idx <= num_args); | |||
There was a problem hiding this comment.
I don't know why this condition is here? Definitely calls for a comment.
There was a problem hiding this comment.
yeah... that's a good point. I'll add some comments.
There was a problem hiding this comment.
What's 0? And the rest are locals I assume?
There was a problem hiding this comment.
0 is the return variable. There is a comment right below that talks about that. I added a comment to the function explaining that. I hope it helps.
| @@ -58,7 +67,8 @@ impl<'tcx> GotocCtx<'tcx> { | |||
| let loc = self.codegen_span(&ldata.source_info.span); | |||
| let sym = | |||
| Symbol::variable(name, base_name, t, self.codegen_span(&ldata.source_info.span)) | |||
| .with_is_hidden(!ldata.is_user_variable()); | |||
| .with_is_hidden(!ldata.is_user_variable()) | |||
| .with_is_parameter(idx > 0 && idx <= num_args); | |||
There was a problem hiding this comment.
What's 0? And the rest are locals I assume?
Description of changes:
kani-driverto run sanity checks that are available in CBMC to perform consistency checks on the GOTO model.is_parameterflag. We were not setting this parameter at all. CBMC expects all symbols that are function parameters to have this flag set totrue.Resolved issues:
This is related to #957
Call-outs:
We would like to enable these checks (as requested in #957), however the regression is still failing as described in #957 (comment).
Testing:
How is this change tested?
Is this a refactor change?
Checklist
By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.