Kani should make use of CBMC's internal consistency checks.

[tautschnig]

Requested feature: cbmc and also goto-instrument can be invoked with --validate-goto-model to perform consistency checks on the GOTO model. cbmc furthermore supports --validate-ssa-equation to enable consistency checks on the formula generated during symbolic execution. These bear additional runtime cost, but could help spot bugs creeping in as Kani builds expressions using a completely different code base. CBMC uses these options in its regression test suite.
Use case: Enabling those in regression tests might well be the right approach for Kani as well.
Link to relevant documentation (Rust reference, Nomicon, RFC):
Is this a breaking change? Yes, because there currently are some inconsistencies reported when manually enabling these options on Kani-generated goto binaries.

Test case: Running CBMC on the goto binary attached to diffblue/cbmc#6731:

cbmc test.out --validate-goto-model
CBMC version 5.52.0 (cbmc-5.52.0-61-g686da25177) 64-bit x86_64 linux
Reading GOTO program from file test.out
Generating GOTO Program
--- begin invariant violation report ---
Invariant check failed
File: ../src/goto-programs/goto_function.cpp:43 function: validate
Condition: identifier.empty() || ns.lookup(identifier).is_parameter
Reason: parameter should be marked 'is_parameter' in the symbol table
Backtrace:
build/bin/cbmc(print_backtrace(std::ostream&)+0x50) [0x56243462d600]
build/bin/cbmc(get_backtrace[abi:cxx11]()+0x169) [0x56243462dba9]
build/bin/cbmc(std::enable_if<std::is_base_of<invariant_failedt, invariant_failedt>::value, void>::type invariant_violated_structured<invariant_failedt, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&>(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)+0x48) [0x562433c4d618]
build/bin/cbmc(goto_functiont::validate(namespacet const&, validation_modet) const+0x103) [0x562434144543]
build/bin/cbmc(goto_functionst::validate(namespacet const&, validation_modet) const+0x634) [0x5624341485a4]
build/bin/cbmc(initialize_goto_model(std::vector<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::allocator<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > > > const&, message_handlert&, optionst const&)+0x9fe) [0x5624341726ee]
build/bin/cbmc(cbmc_parse_optionst::get_goto_program(goto_modelt&, optionst const&, cmdlinet const&, ui_message_handlert&)+0x226) [0x562433c4f4f6]
build/bin/cbmc(cbmc_parse_optionst::doit()+0x58f) [0x562433c5372f]
build/bin/cbmc(parse_options_baset::main()+0x8f) [0x562434655c4f]
build/bin/cbmc(main+0x39) [0x562433c4df19]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7f6507d770b3]
build/bin/cbmc(_start+0x2e) [0x562433c4d02e]


--- end invariant violation report ---
Aborted (core dumped)

[zhassan-aws]

It seems that the consistency checks currently fail even on very simple Rust programs, e.g.:

$ cat test.rs 
#[kani::proof]
fn check() {
    let x: i32 = kani::any();
    assert!(x != 0);
}
$ kani test.rs --cbmc-args --validate-goto-model 
<snip>
Checking harness check...
--- begin invariant violation report ---
Invariant check failed
File: ../src/goto-programs/goto_function.cpp:43 function: validate
Condition: identifier.empty() || ns.lookup(identifier).is_parameter
Reason: parameter should be marked 'is_parameter' in the symbol table
Backtrace:
cbmc(print_backtrace(std::ostream&)+0x50) [0x556460ce36e0]
cbmc(get_backtrace[abi:cxx11]()+0x169) [0x556460ce3c89]
cbmc(std::enable_if<std::is_base_of<invariant_failedt, invariant_failedt>::value, void>::type invariant_violated_structured<invariant_failedt, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&>(std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, int, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&, std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > const&)+0x48) [0x55646046cd78]
cbmc(goto_functiont::validate(namespacet const&, validation_modet) const+0x103) [0x5564608c1853]
cbmc(goto_functionst::validate(namespacet const&, validation_modet) const+0x634) [0x5564608c5534]
cbmc(initialize_goto_model(std::vector<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> >, std::allocator<std::__cxx11::basic_string<char, std::char_traits<char>, std::allocator<char> > > > const&, message_handlert&, optionst const&)+0x9fe) [0x5564608e8c1e]
cbmc(cbmc_parse_optionst::get_goto_program(goto_modelt&, optionst const&, cmdlinet const&, ui_message_handlert&)+0x226) [0x55646046eb46]
cbmc(cbmc_parse_optionst::doit()+0x58f) [0x556460472d7f]
cbmc(parse_options_baset::main()+0x8f) [0x55646046ae8f]
cbmc(main+0x39) [0x556460457099]
/lib/x86_64-linux-gnu/libc.so.6(__libc_start_main+0xf3) [0x7ff244e8e0b3]
cbmc(_start+0x2e) [0x55646046c78e]


--- end invariant violation report ---

@tautschnig, is there a way to print more information, e.g. the name of the parameter that is failing the consistency checks?

[tautschnig]

I'll work on improving the output of those checks, I've myself been caught by this lack of information more than once. That said, however: are you setting is_parameter at all? Only if so would the name really be helpful, I guess.

[zhassan-aws]

I don't see is_parameter set to true anywhere. Which symbols does CBMC expect it to be set for?

[tautschnig]

I don't see is_parameter set to true anywhere. Which symbols does CBMC expect it to be set for?

All symbols that are function parameters. Presumably there is some code that introduces symbols for function declarations, and that's where is_parameter should get set.

[celinval]

I was able to fix the is_parameter issue. I'll submit a PR soon. However, I'm running into another issue with memcmp. E.g., with this code:

#[kani::proof]
fn main() {
    assert!("Bl" == "Bl");
}

I am getting the following error:

Reading GOTO program from 'main.out.for-main'
memcmp type inconsistency
goto program type: code
symbol table type: code
Error: goto-instrument exited with status exit status: 6

@tautschnig any idea?

Here is the snippet of main.out.demangled.c where memcmp is invoked.

_Bool <[u8] as core::slice::cmp::SlicePartialEq<u8>>::equal(struct &[u8] self, struct &[u8] other)
{
  _Bool var_0;
  _Bool var_3;
  unsigned long int var_4;
  struct &[u8] var_5;
  unsigned long int var_6;
  struct &[u8] var_7;
  unsigned long int size;
  struct &[u8] val;
  int var_10;
  unsigned char *var_11;
  unsigned char *var_12;
  struct &[u8] <[u8] as core::slice::cmp::SlicePartialEq<u8>>::equal$$1$$var_13$$self;
  unsigned char *var_14;
  unsigned char *var_15;
  struct &[u8] <[u8] as core::slice::cmp::SlicePartialEq<u8>>::equal$$1$$var_16$$self;
  unsigned long int var_17;
  struct &[u8] var_18;
  struct &[u8] var_19;
  struct &[u8] var_20;

bb0:
  ;
  var_5 = self;
  var_4 = var_5.len;
  var_7 = other;
  var_6 = var_7.len;
  var_3 = var_4 != var_6;
  if(!(var_3 == 0))
  {
    goto bb1;

  bb1:
    ;
    var_0 = 0;
    goto bb4;
  }


bb2:
  ;
  val = self;
  var_18 = (struct &[u8]){ .data=val.data, .len=val.len };
  size = 1 * var_18.len;
  goto bb5;

bb3:
  ;
  var_0 = var_10 == 0;

bb4:
  ;
  return var_0;

bb5:
  ;
  <[u8] as core::slice::cmp::SlicePartialEq<u8>>::equal$$1$$var_13$$self = self;
  var_19 = (struct &[u8]){ .data=<[u8] as core::slice::cmp::SlicePartialEq<u8>>::equal$$1$$var_13$$self.data, .len=<[u8] as core::slice::cmp::SlicePartialEq<u8>>::equal$$1$$var_13$$self.len };
  var_12 = var_19.data;
  var_11 = var_12;
  <[u8] as core::slice::cmp::SlicePartialEq<u8>>::equal$$1$$var_16$$self = other;
  var_20 = (struct &[u8]){ .data=<[u8] as core::slice::cmp::SlicePartialEq<u8>>::equal$$1$$var_16$$self.data, .len=<[u8] as core::slice::cmp::SlicePartialEq<u8>>::equal$$1$$var_16$$self.len };
  var_15 = var_20.data;
  var_14 = var_15;
  var_17 = size;
  var_10=memcmp(var_11, var_14, var_17);
  goto bb3;
}

main.symtab.zip

[tautschnig]

It seems that there is an inconsistency on the parameter types. Your symbol table includes a declaration of memcmp that matches the one that C has, which has void* typed parameters. You then, however, also have function calls to memcmp, which include a type (as expected). Those calls now have parameters of type uint8_t.

[celinval]

Thanks Michael! That message was a bit cryptic for me.

[tautschnig]

Thanks Michael! That message was a bit cryptic for me.

What a euphemism :-) I locally hacked it to use the .pretty() output to get the full ireps in order to understand what was going on.

[celinval]

It looks like rust (and LLVM's) memcmp expects *const u8.

https://github.com/rust-lang/rust/blob/15a242a432c9c40a60def102209a5d40900b7b9d/library/core/src/slice/cmp.rs#L10-L18

We'll have to special case that.

[celinval]

This issue seems to be captured here: #1350

[tedinski]

@celinval What's the current status of this? (Just not clear where things left off...)

[celinval]

This issue is blocked until we fix #1350.

[celinval]

We should revisit this... I noticed the other day that enabling these checks with contracts can trigger consistency check failure.