facebookexperimental / mirai Goto Github PK
View Code? Open in Web Editor NEWRust mid-level IR Abstract Interpreter
License: MIT License
Rust mid-level IR Abstract Interpreter
License: MIT License
The str::is_empty
contract relies on the builtin str::len
function and compares the result of calling that function to 0
. When the string is actually empty, this condition is not sufficient for some reason.
pub mod foreign_contracts {
pub mod core {
pub mod str {
pub mod implement_str {
pub fn is_empty(_self: &str) -> bool {
_self.len() == 0
}
}
}
}
}
pub fn main() {
let s = "";
verify!(s.is_empty());
}
No error.
warning: possible false verification condition
|
20 | verify!(s.is_empty());
| ^^^^^^^^^^^^^^^^^^^^^^
|
Rust version (rustc --version): rustc 1.37.0-nightly (8ebd67e4e 2019-06-27)
The condition in assume
doesn't seem to be modifying the path condition as expected.
Test case:
#[macro_use]
extern crate mirai_annotations;
pub struct Block {
round: u64,
}
pub fn round(bl: Block) -> u64{
assume!(bl.round < std::u64::MAX - 1);
bl.round
}
pub fn foo(bl: Block) {
let ret = round(bl);
verify!(ret < std::u64::MAX - 1);
}
The verify
condition is expected to be true.
thread 'rustc' panicked at 'Unexpected error: possible false verification condition
Rust version (rustc --version): rustc 1.37.0-nightly (0beb2ba16 2019-07-02)
The upper bound of a value is not recognized in a postcondition.
pub fn checked_add(_self: usize, value: usize) -> Option<usize> {
let res = _self.checked_add(value);
postcondition!(res.is_none() || _self <= usize::max_value() - value);
res
}
No warning message.
MIRAI warns that there is a possible attempt to subtract with overflow in usize::max_value() - value
. This warning goes away if the following assumption is added: assume!(value <= usize::max_value());
.
Rust version (rustc --version): rustc 1.37.0-nightly (0beb2ba16 2019-07-02)
Defining a constant's max_value()
with the MAX
constant defined in the foreign contracts crate does not work.
pub mod implement_usize {
use crate::foreign_contracts::core;
pub fn max_value() -> usize {
if cfg!(any(
target_arch = "x86",
tagret_arch = "mips",
tagret_arch = "powerpc",
tagret_arch = "arm"
)) {
usize::MAX
} else if cfg!(any(
target_arch = "x86_64",
tagret_arch = "powerpc64",
tagret_arch = "aarch64"
)) {
usize::MAX
} else {
panic!("Unsupported architecture");
}
}
}
All tests should pass.
Some tests that use usize::max_value()
fail with Possible unsatisfied precondition
when they didn't before.
Rust version (rustc --version): rustc 1.37.0-nightly (0beb2ba16 2019-07-02)
Constants used in annotations are not always recognized to mean literal value.
Please see: https://our.internmc.facebook.com/intern/diff/D15950558/
If a MIRAI annotation contains a constant, the constant should be recognized and its value should be used in the annotation.
If the value of the constant is substituted into the annotation, then it behaves as expected. If the constant is used, the annotation does not have the desired effect.
Rust version (rustc --version): rustc 1.37.0-nightly (b25ee6449 2019-06-17)
The automatically derived serializer/deserializer cannot deal with references, which makes it hard to define AbstractValue and related types in such a way that they can be cheaply shared.
As a first step to making AbstractValues serializable, just write explicit implications of the serializer methods for Summary and all types reachable from it.
AbstractDomain::implies and AbstracDomain:implies_not use algebraic rules to attempt to figure out at compile time what the values of x => y and x => !y are. The rule is that false is also the way to say "I don't know". These implications are used to eliminate paths and to simplify conditional expressions.
Only a few rules are currently used. Here are some more rules that I've previously used in another project. Better check them with theorem prover, for there may transcription errors.
Note that the rules are recursive and may have exponential complexity unless depth limited.
x => x
(x || y) => z if (x => z && y => z)
(x && y) => z if (x => z || y => z)
!!x => y if x => y
(c ? true : false) => c
(c ? false : y) => (false != z) if y => z, since (c ? false: y) is false unless y is true z is true if y is true
(c ? false : y) => (z != false) if y => z, since (c ? false: y) is false unless y is true z is true if y is true
(c ? x : false) => (false != z) if x => z, since (c ? x : false) is false unless x is true and z is true if x is true
(c ? x : false) => (z != false) if x => z, since (c ? x : false) is false unless x is true and z is true if x is true
(c ? x : false) => z if c => z || x => z
(false != x) => x
(x != false) => x
(0 != x) => x // not type correct but might happen
(x != 0) => x // not type correct but might happen
!x => !x
(x || y) => !z if (x => !z && y => !z)
(x && y) => !z if (x => !z || y => !z)
!!x => !y if x => !y
x => !y if y => !x
!x => !y if y => x since if y is false x can be any value and if y is true then x must be true
(c ? false : true) => !c
(c ? false : y) => !(z == false) if y => z, since !(z == false) is true if y is true
(c ? false : y) => !(false == z) if y => z, since !(false == z) is true if y is true
(c ? x : false) => !(z == false) if x => z, since !(z == false) is true if x is true
(c ? x : false) => !(false == z) if x => z, since !(false == z) is true if x is true
(c ? x : false) => !z if c => !z || x => !z
(x === y && y !== z) => !(x === z)
(x === y && x !== z => !(y === z)
If you like compilers and related tools, you are a meta-programmer, so you should like meta issues as well. This issue is a task to create tasks.
Since you are new here, please keep track of all of the surprises you've encountered and the things you had to find out the hard way. Then make an issue to get the fixed.
Ideally, follow that up with PR in which you fix it. Many thanks for doing that!
Read the developer documentation and try to fix an issue.
You got going with no problems and everything is crystal clear.
You muttered WTF on several occasions.
Trace output can be overwhelming so I often want to turn that off. On the other hand, since debugging support for Rust is pretty much non existent, I often need to insert some kind of print statement in the code while debugging. This is covered by the distinction between trace! and debug!, but unfortunately the code I looked at early on only ever used debug! and I just followed that.
Some functions from the standard libraries (and from mirai-annotations) are well known to MIRAI and calls to them have semantics that cannot be expressed in summaries.
Currently there is an elaborate and not very scalable scheme for checking if a function is well known. Basically, it boils down to checking if the summary cache key is well known. Since this is an expensive check it needs to be cached.
Currently that is done in ConstantValueCache, but many expensive checks may happen before caching succeeds. While it is conceivable that the total number of such checks will be smaller than the total number of function values created during the lifetime of ConstantValueCache, the current scheme does not guarantee a bound to the number of checks.
An alternative scheme is to set aside a field in each function object that is an enum that lists all of the well known functions (and has an "other" value for non well known functions). This field must then be initialized (via the expensive summary cache key check) when a function is constructed.
Code sites that want to check if a function is a particular well known function, will then just have to check the value of this enum.
It says to do rustup override set nightly
but as of 02/23 this results in cargo build
failing with a compile error. I eventually realized that the Travis build was pinned to the 01/07 nightly. Maybe the guide could contain a pointer to the .travis.yml
file?
FWIW, before realizing that, I had cobbled together a fix to make things compile here: int3@f4a45d2.
Edit: The "fix" errors out at runtime, never mind... just going to work off the older nightly version for now.
Some parts of the MIRAI code base are not covered by integration tests. You task here is to find such bits of code and to create an issue for each of them. Ideally follow up with a PR that contains a test case that covers that bit of code.
As you read through the code base to get to know it, click on the coverage button so see code coverage. The code coverage tools is not quite perfect, so you might see lines that are marked as not covered when they obviously are, but there will be some cases that are not obviously covered. You can verify that a line of code is not covered by setting a break point on it and running the integration tests from the debugger.
If you are going to follow up with a PR to fix this omission, the next step would be to set some breakpoints in the surrounding covered code to find the test cases that reach then and then try to mutate one or more of those test cases to instead or also reach the uncovered code.
Every executable source line should be reached by an integration test case.
Some code lines are not so covered.
We need more issues. Create some meta issues to spur the creation of more issues.
Look at the issues tab.
There should be more issues and meta issues.
Not enough issues.
Implement the code to extract a suitable summary from the state constructed by the visitor for a function body.
This is a tracking item for work related to this road map item.
Rather than manually inspecting the .travis.yml to determine the current supported nightly version, and then manually installing it with rustup, you can just create a rust-toolchain
file with the nightly version in it. This will cause cargo
to automatically download and use that toolchain without needing user interaction.
Follow build steps.
Automatic selection of toolchain.
Manual install and configuration of toolchain.
Linux (but pretty sure it applies to all)
Running MIRAI over an entire crate every time it the crate is rebuilt is somewhat painful since every function body is re-analyzed at least once.
An alternative way to is to run MIRAI as part of the linter (see https://doc.rust-lang.org/unstable-book/language-features/plugin.html#lint-plugins and https://github.com/rust-lang/rust-clippy/blob/61aa5c957c219abe1fb2d1b5e51db8b365b4f565/clippy_lints/src/missing_const_for_fn.rs#L105).
It seems that the linter will only call the MIRAI plugin when a function has changed, so the it should be sufficient to invoke the checker in the same way as will be done by #113.
Currently one cannot write a contract for a Rust primitive such as str
.
The format of a contract on a function has to be such that MIRAI recognizes it as the same as the mangled name of the actual function. If the function is for a primitive type, i.e. str::as_bytes
, then one will need a model of str
. However, Rust only allows one definition of language builtins.
Attempt to use the following contract:
pub mod str {
impl str {
pub fn len(&self) -> usize {
self.as_bytes().len()
}
}
}
One should be able to define an alternate name for language builtins that MIRAI recognizes. For example, impl rust_builtin_str
. The rust_builtin
prefix would be stripped by MIRAI.
Rust does not allow the above contract to be written; it gives the error:
error[E0390]: only a single inherent implementation marked with '#[lang = "str"]' is allowed for the
str primitive
Rust version (rustc --version): rustc 1.37.0-nightly (2fe7b3383 2019-06-19)
Create an abstract domain for tracking intervals such as [0, ..., n] and so on.
Precondition fails for contract with new name mangling scheme.
#![feature(type_alias_enum_variants)]
#[macro_use]
extern crate mirai_annotations;
pub mod foreign_contracts {
pub mod core {
pub mod num {
pub mod implement_u32 {
pub fn max_value() -> u32 {
u32::max_value()
}
}
}
}
}
pub fn test1(size: u32) -> u32 {
precondition!(size <= u32::max_value());
size
}
pub fn test() {
test1(100);
}
fn main() {
test();
}
No warnings should be issued.
warning: possible unsatisfied precondition
--> examples/test5.rs:23:5
|
23 | test1(100);
| ^^^^^^^^^^
|
note: related location
--> examples/test5.rs:18:5
|
18 | precondition!(size <= u32::max_value());
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Rust version (rustc --version): rustc 1.37.0-nightly (2fe7b3383 2019-06-19)
Running MIRAI on selection sort which iterates over a range of integers causes "fixed point loop divergence".
Test case:
fn selection_sort(array: &mut [i32]) {
let mut min;
for i in 0..array.len() {
min = i;
for j in (i + 1)..array.len() {
if array[j] < array[min] {
min = j;
}
}
let tmp = array[i];
array[i] = array[min];
array[min] = tmp;
}
}
fn main() {
let mut array = [9, 4, 8, 3, -5, 2, 1, 6];
println!("The initial array is {:?}", array);
selection_sort(&mut array);
println!(" The sorted array is {:?}", array);
}
Cargo command:
RUSTC_WRAPPER=mirai MIRAI_LOG=info cargo check
Analysis should reach fixed point without divergence in the loop.
[2019-06-26T22:33:39Z INFO mirai::callbacks] Processing input file: examples/selection_sort/src/main.rs
[2019-06-26T22:33:39Z INFO mirai::callbacks] storing summaries for examples/selection_sort/src/main.rs at /Users/rashmimudduluru/MIRAI/target/debug/deps/.summary_store.sled
[2019-06-26T22:33:39Z INFO mirai::callbacks] outer fixed point iteration 1
[2019-06-26T22:33:39Z INFO mirai::callbacks] analyzing("selection_sort.selection_sort")
[2019-06-26T22:33:39Z INFO mirai::summaries] Summary store has no entry for core.slice.implement.len__i32
[2019-06-26T22:33:39Z WARN mirai::visitors] fixed point loop diverged in body of selection_sort.selection_sort
[2019-06-26T22:33:39Z WARN mirai::visitors] Fixed point loop took 51 iterations for selection_sort.selection_sort.
[2019-06-26T22:33:40Z INFO mirai::callbacks] analyzing("selection_sort.main")
[2019-06-26T22:33:42Z INFO mirai::callbacks]
[2019-06-26T22:33:42Z INFO mirai::callbacks] outer fixed point iteration 2
[2019-06-26T22:33:42Z INFO mirai::callbacks] reanalyzing("selection_sort.selection_sort")
[2019-06-26T22:33:42Z INFO mirai::summaries] Summary store has no entry for core.slice.implement.len__i32
[2019-06-26T22:33:42Z WARN mirai::visitors] fixed point loop diverged in body of selection_sort.selection_sort
[2019-06-26T22:33:42Z WARN mirai::visitors] Fixed point loop took 51 iterations for selection_sort.selection_sort.
[2019-06-26T22:33:42Z INFO mirai::callbacks] reanalyzing("selection_sort.main")
Rust version (rustc --version): rustc 1.37.0-nightly (2fe7b3383 2019-06-19)
MIRAI issues a false warning when a provably true condition is specified with verify!
Test case:
use mirai_annotations::{verify};
use std::{
sync::Arc,
};
pub type Round = u64;
pub struct Block
{
round: Round,
}
impl Block
{
pub fn round(& self) -> Round {
let result = self.round;
result
}
pub fn voting_rule(
&mut self,
proposed_block: Arc<Block>,
) {
if proposed_block.round() <= self.round() {
return;
}
verify!(proposed_block.round() > self.round());
}
}
No MIRAI warning.
warning: possible false verification condition
--> src/lib.rs:27:9
|
27 | verify!(proposed_block.round() > self.round());
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
= note: this warning originates in a macro outside of the current crate (in Nightly builds, run with -Z external-macro-backtrace for more info)
Rust version (rustc --version): rustc 1.38.0-nightly (6e310f2ab 2019-07-07)
I think we need an abstract model of heap. What is on your mind? @hermanventer
Another question to clarify is how to abstract heap pointer values, a.k.a. Box<T>
. Is there another wrapper of heap-allocated object in Rust?
I checked the source and there is only pub environment: &'a mut HashTrieMap<Path, AbstractValue>
.
Talk to potential users of Mirai and determine if there is any need for Mirai specific build options.
Also determine if Mirai should automatically add options to the list it passes to the Rust compiler, for example in order to make the compilation produce additional information that will help static analysis.
Write a rudimentary simplifier that will simplify an expression domain instance using Algebra rules and pattern matching. This will complement using a fully featured solver like Z3. The latter will be invoked mainly when a potential issue has been identified in a path that has conditions that have not been solved by the simplifier.
The place where this is to be implemented is the implementation of AbstractDomain. Most of the methods there are factories that construct AbstractDomain values from arguments for particular operations. If you look there you will already see that most methods start with a match statement that checks if the arguments are constants and then does constant folding.
In many cases, further algebraic simplifications can be done. For example, instead of constructing a multiply expression for x * 0, the factory can just return the constant 0. There is no need to be concerned about side effects since those are all factored out into assignment statements that are not expressions. Even functional calls are not expressions.
Here are a list of algebraic simplifications that were useful in another project I've worked on before MIRAI. They are in no particular order and there may be many others that are equally useful. They also assume recursive simplification (subject to recursive depth limitation).
x + 0 = x
x * 1 = x
x * 0 = 0
x | 0 = x
x & 0 = 0
!!x <=> x
true && y <=> y
true || y <=> true
false || y <=> y
x && true <=> x
x || true <=> true
x && false <=> false
x || false <=> x
x || x || y <=> x || y
!x0 || y0 || x0 <=> true
(x && y) && x <=> x && y
(x && y) && y <=> x && y
!x && x <=> false
x && (x && y) <=> x && y
y && (x && y) <=> x && y
x && (x && y || x && z) <=> x && (y || z)
c ? x : x <=> x
x ? x : y <=> x || y
y ? x : y <=> y && x
c ? (c ? xx : xy) : y <=> c ? xx : y
c ? x : (c ? y : z) : z <=> c ? x : z
c ? true : false <=> c
c ? false : true <=> !c
((c ? xx : xy) === y) && xx === y && xy !== y <=> c
((!c ? xx : xy) === y) && xx !== y && xy === y <=> !c
(x === (c ? yx : yy) === y) && x === yx && x !== yy <=> c
(x === (!c ? yx : yy) === y) && x !== yx && x === yy <=> !c
!(x == y) <=> x != y
!(x != y) <=> x == y
!(x < y) <=> x >= y
!(x <= y) <=> x > y
!(x > y) <=> x <= y
!(x >= y) <=> x < y
!(x && y) <=> !x || !y
!(x || y) <=> !x && !y
Promoted constants are compile time constant values that are promoted to runtime memory locations so that they may be referred to via references.
Since these constants can be complex, the MIR representation helpfully provides a function body that will compute the constant.
Before starting the analysis proper, find the promoted constants, analyze their bodies and store the Mirai abstract value from their summaries in a table that can be used by the analysis proper.
Give some though to how the code for constant A may refer to another constant B.
An abstract value that is serialized into to the persistent summary cache for use by another
compilation, does not take its provenance with it since syntax_pos::Span is only meaningful inside the current compilation.
This means that if a function foo in crate A violates a precondition when calling function bar in crate B, the diagnostic will not be able to point out the source location of that precondition, which can be irksome if the precondition is not documented.
For such cases it would be nice to precompute a source location string from the span and save it in the summary alongside the abstract value that is the precondition.
Doing so only when the precondition is not otherwise documented is a bit of stretch goal. One way to think about this is that the string stored in the summary is the documentation and that precomputed source location is just default documentation. One might also consider using the actual source of the precondition as the default documentation, rather than just pointing to it, although in the latter case the actual location should probably be there as well.
We can't do Algebraic simplifications such as (x == 0) || !(x == 0) => true if we get (Top == 0) || !(Top == 0) because the value of x is unknown.
Hi everyone! I've just heard about MIRAI. The project is very exciting and I hope it will eventually become a part of IntelliJ Rust and RLS code analysis! However, while reading the documentation I was surprised to see that CLion doesn't support debugging MIRAI ([1] and [2]).
I've just tried it out and seems like it works fine:
All I have to do is to provide the DYLD_LIBRARY_PATH
as specified:
Also [3],
debugging support for Rust is pretty much non existent
I'm sorry to hear that. I'm working on new lldb formatters for Rust; in CLion, they are enabled by default and configurable via Preferences | Build, Execution, Deployment | Debugger | Data Views | Rust
. I hope debugging support gets better, though there is no Evaluate expression
for Rust yet. So I really want to know if something related to debugging frontend doesn't work properly or if you have some ideas to improve it (at frontend level, like formatters, watches, remote debugging and so on). If so, you can open an issue here.
Currently a set of constants in checker/src/k_limits.rs provides limits on how much computation MIRAI will do in various places. With these limits in place, largish crates can be analyzed in a somewhat reasonable time frame. The limits do, however, impact on precision and may lead to false negatives. By making these into variables that can be set via command line options, it will become possible to schedule longer runs that may find more issues than more limited runs. The greater precision allowed by such runs can also be used to weed out false positives.
The recommended way to complete this task is to turn the constants in k_limits into the fields of a struct and to provide a constructor that sets the fields to default values, along with a command line processor that updates the values from options in the command line.
The limits struct should then be made part of the visitor state (checker/src/visitor.rs).
Ideally, there should also be a way to set these options to non default values for integration test cases. See also #52.
The default debug formatter for ExpressionDomain results in very verbose hard to read output. Write a proper formatter that uses operator symbols and precedence rules to compact the output into something much more like a source language expression.
MIRAI incorrectly issues a warning for a provably correct verification condition.
use mirai_annotations::{verify};
use std::{
sync::Arc,
};
pub type Round = u64;
pub struct Block
{
round: Round,
}
impl Block
{
pub fn round(& self) -> Round {
let result = self.round;
result
}
pub fn voting_rule(
&mut self,
proposed_block: Arc<Block>,
) {
if proposed_block.round() <= self.round() {
return;
}
verify!(proposed_block.round() > self.round());
}
}
MIRAI should verify the program without any warnings.
warning: possible false verification condition
--> src/lib.rs:27:9
|
27 | verify!(proposed_block.round() > self.round());
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Rust version (rustc --version): rustc 1.37.0-nightly (0beb2ba16 2019-07-02)
Provide a way to write code that provides a contract for a function without a body (e.g. a trait method or a foreign function). Get Mirai to find and analyze this code and put the results in the summary cache.
assumed_postcondition
doesn't add the postcondition to the function summary in the presence of an unsatisfiable precondition.
use mirai_annotations::{checked_precondition, assumed_postcondition, verify};
pub struct Block {
round: u64,
}
pub fn round(bl: Block) -> u64 {
checked_precondition!(bl.round < std::u64::MAX - 1);
let result = bl.round;
assumed_postcondition!(result < std::u64::MAX - 1);
result
}
pub fn foo(bl: Block) {
let ret = round(bl);
verify!(ret < std::u64::MAX - 1);
}
assumed_precondition
should behave the same both in the presence of checked_precondition
and without it.
Running MIRAI on the above example results in the following output:
warning: possible unsatisfied precondition
--> src/lib.rs:15:15
|
15 | let ret = round(bl);
| ^^^^^^^^^
|
note: related location
--> src/lib.rs:8:5
|
8 | checked_precondition!(bl.round < std::u64::MAX - 1);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
= note: this warning originates in a macro outside of the current crate (in Nightly builds, run with -Z external-macro-backtrace for more info)
warning: possible false verification condition
--> src/lib.rs:16:5
|
16 | verify!(ret < std::u64::MAX - 1);
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
|
= note: this warning originates in a macro outside of the current crate (in Nightly builds, run with -Z external-macro-backtrace for more info)
Removing the checked_precondition
causes MIRAI to not report any error.
Rust version (rustc --version): rustc 1.38.0-nightly (4b65a86eb 2019-07-15)
When debugging MIRAI in a context where a small repro is not readily available, it is helpful to be able to run MIRAI in a mode where it will only analyze a specified method.
Typically, the summary cache from a full run will still be available, so analysis of a function body in this way can be done with much more context than is convenient to provide in a small test case.
To implement this feature, add a command line option (see also #112) and then add a check to the after_analysis function in checker/src/callbacks.rs that filters out any function that is not the one specified by the command line option.
An assumed_postcondition
on a vec![]
does not seem to work. If the assumption (assume!(t.v.is_empty())
is placed after the initialization call then it does work.
#[macro_use]
extern crate mirai_annotations;
struct Test {
v: Vec<u8>,
}
impl Test {
fn new() -> Self {
let res = Self {
v: vec![],
};
assumed_postcondition!(res.v.is_empty());
res
}
}
pub fn main() {
let t = Test::new();
verify!(t.v.is_empty());
}
No errors or warnings.
possible false verification condition
Rust version: rustc 1.38.0-nightly (6e310f2ab 2019-07-07)
In some cases MIRAI fails to recognize a condition on an implicit loop iteration variable. This can lead MIRAI to not be able to bound the size of variables within the loop whose values depend on the number of iterations.
Please see: https://our.internmc.facebook.com/intern/diff/D15950558/
MIRAI should recognize that the loop breaks before the shift
variable becomes greater than 14; MIRAI should therefore not give a spurious warning about a potential overflow when the shfit
variable is used for a left shift.
MIRAI gives the following spurious warning:
warning: possible attempt to shift left with overflow
|
209 | value |= u16::from(val) << shift;
| ^^^^^^^^^^^^^^^^^^^^^^^
Rust version (rustc --version): rustc 1.37.0-nightly (b25ee6449 2019-06-17)
Adding an unverifiable postcondition to a function prevents reporting incorrect verify
conditions at its call site.
#[macro_use]
extern crate mirai_annotations;
pub struct Block {
round: u64,
}
impl Block
{
pub fn round(&self) -> u64 {
postcondition!(self.round < std::u64::MAX - 2);
self.round
}
}
pub fn voting_rule(
proposed_block: Block,
) -> () {
let _ret = proposed_block.round();
verify!(_ret < std::u64::MAX);
}
MIRAI should report both the unsatisfiability of the postcondition
and that the verify
condition could be false.
error: possible unsatisfied postcondition
Doesn't report a possibly false verify
condition.
Rust version (rustc --version): rustc 1.38.0-nightly (4b65a86eb 2019-07-15)
Mirai computes a summary for each method and function it analyzes. These summaries should be stored persistently so that they can be retrieved during incremental compilation.
Decide on a way to do this and initialize a cache for summaries when processing the input used by the compilation.
We can expect to accumulate a large collection of small program snippets, each of which exercises some small part of Mirai. It is not convenient to have to write a new entry in tests/integration_tests.rs for each snippet and to have to recompile the ever growing tests/integration_tests.rs every time we add a snippet.
So, instead, let's write a dedicated test runner that will invoke mirai independently on each snippet found in a dedicated directory (e.g. tests/snippets). There should be a mode that can run a designated snippet for debugging purposes (BTW. I can't figure out how to debug a test run via cargo test with VSCode. Please comment if you know how.)
Preferably a default run should use all of the cores of the machine it is running on and should produce minimal console spew for successful runs. When one or more tests fail, the console output should be no more than is needed to run any of the failing tests as an individual run inside a debugger.
Compiler options can influence the MIR that gets generated. For example, the Rvalue::Len
expression may be turned into a constant for -Z mir-opt-level=n
where n > 0
. Since the default level is 1, cargo test
will not run in a mode where the code path that handles Rvalue::Len
gets reached.
In order to test this case using cargo test
, the code integration_test.rs needs to be enhanced to look for comments that specify which compiler options should be used to compile the test case.
Add an info level log statement to the code that handles Rvalue::Len
and observe that MIRAI_LOG=info cargo test
produces no output from this log statement.
When this issue is fixed, you can add the compiler option -Z mir-opt-level=0
to the test case array_literal.rs and you should observe a log entry from your added log statement.
What you expected to happen. For example the error message you expected to see.
No test coverage for Rvalue::Len
when running cargo test
.
Add the function summaries for the following functions to standard contracts:
core.fmt.implement_core_fmt_Formatter.debug_tuple_
core.fmt.builders.implement_core_fmt_builders_DebugTuple.field_
core.fmt.builders.implement_core_fmt_builders_DebugTuple.finish_
serde.de.Deserializer.deserialize_struct____D_consensus_model_chained_bft_consensus_types_block__IMPL_DESERIALIZE_FOR_Block_{{impl}}_deserialize___Visitor_T
core.fmt.implement_core_fmt_Formatter.write_str_
serde.de.Error.invalid_value____E
core.cmp.PartialEq.eq__str_str
serde.de.Deserializer.deserialize_identifier____D_consensus_model_chained_bft_consensus_types_block__IMPL_DESERIALIZE_FOR_Block_{{impl}}_deserialize___FieldVisitor
serde.de.SeqAccess.next_element____A_crypto_hash_HashValue
serde.de.Error.invalid_length____A_as_serde_de_SeqAccess_Error
serde.de.MapAccess.next_key____A_consensus_model_chained_bft_consensus_types_block__IMPL_DESERIALIZE_FOR_Block_{{impl}}_deserialize___Field
serde.de.MapAccess.next_value____A_serde_de_ignored_any_IgnoredAny
serde.de.Error.duplicate_field____A_as_serde_de_MapAccess_Error
serde.private.de.missing_field__crypto_hash_HashValue___A_as_serde_de_MapAccess_Error
serde.ser.Serializer.serialize_struct____S
serde.ser.SerializeStruct.serialize_field____S_as_serde_ser_Serializer_SerializeStruct_crypto_hash_HashValue
serde.ser.SerializeStruct.end____S_as_serde_ser_Serializer_SerializeStruct
core.clone.Clone.clone__crypto_hash_HashValue
core.fmt.implement_core_fmt_Formatter.debug_struct_
core.fmt.builders.implement_core_fmt_builders_DebugStruct.field_
core.fmt.builders.implement_core_fmt_builders_DebugStruct.finish_
core.cmp.PartialEq.ne__crypto_hash_HashValue_crypto_hash_HashValue
core.fmt.implement_core_fmt_Arguments.new_v1_formatted_
core.fmt.implement_core_fmt_Formatter.write_fmt_
crypto.hash.CryptoHash.hash__consensus_model_chained_bft_consensus_types_block_BlockSerializer_T
core.result.implement_core_result_Result_T_E.expect__nextgen_crypto_ed25519_Ed25519Signature_failure_error_Error
std.panicking.begin_panic_fmt_
core.result.implement.map_err__tuple_0_types_validator_verifier_VerifyError_consensus_model_chained_bft_consensus_types_block_BlockVerificationError_closure_consensus_model_chained_bft_consensus_types_block_{{impl}}_1_verify_{{closure}}_T_i32_FnPtr
core.ops.try.Try.into_result__core_result_Result_tuple_0_consensus_model_chained_bft_consensus_types_block_BlockVerificationError
core.convert.From.from__consensus_model_chained_bft_consensus_types_block_BlockVerificationError_consensus_model_chained_bft_consensus_types_block_BlockVerificationError
core.ops.try.Try.from_error__core_result_Result_tuple_0_consensus_model_chained_bft_consensus_types_block_BlockVerificationError
core.ops.deref.Deref.deref__crypto_hash_GENESIS_BLOCK_ID
canonical_serialization.implement_canonical_serialization_SimpleSerializer_W.serialize__alloc_vec_Vec_u8_consensus_model_chained_bft_consensus_types_block_BlockSerializer_T
core.default.Default.default__crypto_hash_BlockHasher
core.convert.AsRef.as_ref__alloc_vec_Vec_u8_slice_u8
crypto.hash.CryptoHasher.write__crypto_hash_BlockHasher
crypto.hash.CryptoHasher.finish__crypto_hash_BlockHasher
canonical_serialization.CanonicalSerializer.encode_u64__impl
canonical_serialization.CanonicalSerializer.encode_struct__impl
canonical_serialization.CanonicalSerializer.encode_raw_bytes__impl
core.convert.Into.into__crypto_hash_HashValue_bytes_bytes_Bytes
rmp_serde.encode.to_vec_named__T
proto_conv.IntoProto.into_proto__consensus_model_chained_bft_consensus_types_quorum_cert_QuorumCert
rmp_serde.decode.from_slice__T
proto_conv.FromProto.from_proto__consensus_model_chained_bft_consensus_types_quorum_cert_QuorumCert
core.convert.TryFrom.try_from__types_account_address_AccountAddress_bytes_bytes_Bytes
core.intrinsics._1.discriminant_value__consensus_model_chained_bft_liveness_pacemaker_NewRoundReason
std.sync.mutex.implement_std_sync_mutex_Mutex_T.lock__u64
core.result.implement_core_result_Result_T_E.unwrap__std_sync_mutex_MutexGuard_u64_std_sys_common_poison_PoisonError_std_sync_mutex_MutexGuard_u64
core.ops.deref.DerefMut.deref_mut__std_sync_mutex_MutexGuard_u64
core.slice.implement.iter__alloc_sync_Arc_consensus_model_chained_bft_consensus_types_block_Block_T
core.iter.traits.iterator.Iterator.map__core_slice_Iter_alloc_sync_Arc_consensus_model_chained_bft_consensus_types_block_Block_T_ref_T_closure_consensus_model_chained_bft_liveness_proposal_generator_{{impl}}_generate_proposal_{{closure}}_{{closure}}_T_i16_FnPtr
core.iter.traits.iterator.Iterator.collect__core_iter_adapters_Map_core_slice_Iter_alloc_sync_Arc_consensus_model_chained_bft_consensus_types_block_Block_T_closure_consensus_model_chained_bft_liveness_proposal_generator_{{impl}}_generate_proposal_{{closure}}_{{closure}}_T_i16_FnPtr
core.time.implement.from_micros_
core.pin.implement_core_pin_Pin_P.new_unchecked__ref_mut_impl_consensus_model_util_time_service_wait_if_possible_{{opaque}}
std.future.poll_with_tls_context__impl_consensus_model_util_time_service_wait_if_possible_{{opaque}}
slog_scope.with_logger__closure_consensus_model_chained_bft_liveness_proposal_generator_{{impl}}_generate_proposal_{{closure}}_{{closure}}_1_T_i32_FnPtr
core.time.implement.as_millis_
prometheus.histogram.implement_prometheus_histogram_Histogram.observe_
prometheus.counter.implement_prometheus_counter_GenericCounter_P.inc__prometheus_atomic64_fallback_RwlockAtomic_i64
core.time.implement.as_micros_
std.future.from_generator__default
core.iter.traits.iterator.Iterator.enumerate__core_slice_Iter_consensus_model_chained_bft_liveness_timeout_msg_PacemakerTimeout
core.iter.traits.collect.IntoIterator.into_iter__core_iter_adapters_Enumerate_core_slice_Iter_consensus_model_chained_bft_liveness_timeout_msg_PacemakerTimeout
core.iter.traits.iterator.Iterator.next__core_iter_adapters_Enumerate_core_slice_Iter_consensus_model_chained_bft_liveness_timeout_msg_PacemakerTimeout
std.collections.hash.set.implement.new__types_account_address_AccountAddress
std.collections.hash.set.implement_std_collections_hash_set_HashSet_T_S.len__types_account_address_AccountAddress_std_collections_hash_map_RandomState
std.collections.hash.set.implement_std_collections_hash_set_HashSet_T_S.insert__types_account_address_AccountAddress_std_collections_hash_map_RandomState
core.option.implement.map_or__u64_u64_closure_consensus_model_chained_bft_liveness_timeout_msg_{{impl}}_11_verify_{{closure}}_i32_FnPtr
core.option.implement.unwrap_or__u64
core.cmp.Ord.min__u64
core.iter.traits.collect.FromIterator.from_iter__protobuf_repeated_RepeatedField_network_proto_consensus_PacemakerTimeout_network_proto_consensus_PacemakerTimeout_core_iter_adapters_Map_alloc_vec_IntoIter_consensus_model_chained_bft_liveness_timeout_msg_PacemakerTimeout_fn_proto_conv_IntoProto_into_proto_consensus_model_chained_bft_liveness_timeout_msg_PacemakerTimeout
protobuf.repeated.implement_protobuf_repeated_RepeatedField_T.into_iter__network_proto_consensus_PacemakerTimeout
core.intrinsics._1.unreachable_
prometheus.gauge.implement_prometheus_gauge_GenericGauge_P.set__prometheus_atomic64_fallback_RwlockAtomic_i64
core.option.implement.expect__alloc_sync_Arc_consensus_model_chained_bft_consensus_types_block_Block_T
alloc.string.ToString.to_string__network_protocols_rpc_error_RpcError
std.collections.hash.map.implement_std_collections_hash_map_HashMap_K_V_S.get__crypto_hash_HashValue_consensus_model_chained_bft_consensus_types_quorum_cert_QuorumCert_std_collections_hash_map_RandomState_crypto_hash_HashValue
core.iter.traits.iterator.Iterator.for_each__std_collections_hash_map_IntoIter_crypto_hash_HashValue_consensus_model_chained_bft_consensus_types_quorum_cert_QuorumCert_closure_consensus_model_chained_bft_block_storage_block_store_{{impl}}_build_block_tree_{{closure}}_{{closure}}_1_T_i16_FnPtr
std.sync.rwlock.implement_std_sync_rwlock_RwLock_T.read__consensus_model_chained_bft_block_storage_block_tree_BlockTree_T
std.sync.rwlock.implement_std_sync_rwlock_RwLock_T.write__consensus_model_chained_bft_block_storage_block_tree_BlockTree_T
logger.security.security_log_
logger.security.implement.error__ref_consensus_model_chained_bft_block_storage_InsertError
logger.security.implement.data__ref_consensus_model_chained_bft_consensus_types_block_Block_T
logger.security.implement.log_
alloc.alloc.box_free__array_consensus_model_chained_bft_consensus_types_block_Block_T
alloc.slice.implement.into_vec__consensus_model_chained_bft_consensus_types_block_Block_T
core.option.implement.ok_or_else__consensus_model_state_replication_ExecutedState_consensus_model_chained_bft_block_storage_InsertError_closure_consensus_model_chained_bft_block_storage_block_store_{{impl}}_insert_single_quorum_cert_{{closure}}_{{closure}}_T_i32_FnPtr
alloc.sync.implement_alloc_sync_Arc_T.new__consensus_model_chained_bft_consensus_types_block_Block_T
std.collections.hash.map.implement.new__crypto_hash_HashValue_alloc_sync_Arc_consensus_model_chained_bft_consensus_types_block_Block_T
std.collections.hash.map.implement_std_collections_hash_map_HashMap_K_V_S.insert__crypto_hash_HashValue_alloc_sync_Arc_consensus_model_chained_bft_consensus_types_block_Block_T_std_collections_hash_map_RandomState
alloc.collections.vec_deque.implement_alloc_collections_vec_deque_VecDeque_T.with_capacity__crypto_hash_HashValue
std.collections.hash.map.implement_std_collections_hash_map_HashMap_K_V_S.remove__crypto_hash_HashValue_alloc_vec_Vec_alloc_sync_Arc_consensus_model_chained_bft_consensus_types_block_Block_T_std_collections_hash_map_RandomState_crypto_hash_HashValue
std.collections.hash.map.implement_std_collections_hash_map_HashMap_K_V_S.contains_key__crypto_hash_HashValue_alloc_sync_Arc_consensus_model_chained_bft_consensus_types_block_Block_T_std_collections_hash_map_RandomState_crypto_hash_HashValue
core.option.implement_core_option_Option_ref_T.cloned__alloc_sync_Arc_consensus_model_chained_bft_consensus_types_block_Block_T
core.option.implement.ok_or__ref_alloc_sync_Arc_consensus_model_chained_bft_consensus_types_block_Block_T_consensus_model_chained_bft_block_storage_BlockTreeError
std.collections.hash.map.implement_std_collections_hash_map_HashMap_K_V_S.entry__crypto_hash_HashValue_alloc_vec_Vec_alloc_sync_Arc_consensus_model_chained_bft_consensus_types_block_Block_T_std_collections_hash_map_RandomState
std.collections.hash.map.implement_std_collections_hash_map_VacantEntry_K_V.insert__crypto_hash_HashValue_alloc_vec_Vec_alloc_sync_Arc_consensus_model_chained_bft_consensus_types_block_Block_T
std.collections.hash.map.implement_std_collections_hash_map_OccupiedEntry_K_V.into_mut__crypto_hash_HashValue_alloc_vec_Vec_alloc_sync_Arc_consensus_model_chained_bft_consensus_types_block_Block_T
prometheus.gauge.implement_prometheus_gauge_GenericGauge_P.inc__prometheus_atomic64_fallback_RwlockAtomic_i64
std.collections.hash.map.implement_std_collections_hash_map_Entry_K_V.or_insert_with__crypto_hash_HashValue_alloc_sync_Arc_consensus_model_chained_bft_consensus_types_quorum_cert_QuorumCert_closure_consensus_model_chained_bft_block_storage_block_tree_{{impl}}_insert_quorum_cert_{{closure}}_T_i32_FnPtr
std.collections.hash.map.implement_std_collections_hash_map_HashMap_K_V_S.len__types_account_address_AccountAddress_crypto_signing_Signature_std_collections_hash_map_RandomState
core.time.implement.checked_sub_
alloc.collections.vec_deque.implement_alloc_collections_vec_deque_VecDeque_T.new__crypto_hash_HashValue
alloc.collections.vec_deque.implement_alloc_collections_vec_deque_VecDeque_T.push_back__crypto_hash_HashValue
alloc.collections.vec_deque.implement_alloc_collections_vec_deque_VecDeque_T.len__crypto_hash_HashValue
prometheus.gauge.implement_prometheus_gauge_GenericGauge_P.sub__prometheus_atomic64_fallback_RwlockAtomic_i64
alloc.collections.vec_deque.implement_alloc_collections_vec_deque_VecDeque_T.append__crypto_hash_HashValue
alloc.collections.vec_deque.implement_alloc_collections_vec_deque_VecDeque_T.pop_front__crypto_hash_HashValue
std.collections.hash.map.implement_std_collections_hash_map_HashMap_K_V_S.keys__crypto_hash_HashValue_alloc_sync_Arc_consensus_model_chained_bft_consensus_types_block_Block_T_std_collections_hash_map_RandomState
core.iter.traits.iterator.Iterator.cloned__std_collections_hash_map_Keys_crypto_hash_HashValue_alloc_sync_Arc_consensus_model_chained_bft_consensus_types_block_Block_T_crypto_hash_HashValue
std.collections.hash.map.implement_std_collections_hash_map_HashMap_K_V_S.values__crypto_hash_HashValue_alloc_sync_Arc_consensus_model_chained_bft_consensus_types_block_Block_T_std_collections_hash_map_RandomState
core.time.implement.from_millis_
futures_locks.rwlock.implement_futures_locks_rwlock_RwLock_T.read__consensus_model_chained_bft_event_processor_EventProcessor_T_P
futures_util.compat.compat01as03.Future01CompatExt.compat__futures_locks_rwlock_RwLockReadFut_consensus_model_chained_bft_event_processor_EventProcessor_T_P
futures_util.stream.StreamExt.next__channel_WithGauge_futures_channel_mpsc_Receiver_consensus_model_chained_bft_liveness_pacemaker_NewRoundEvent
futures_util.future.FutureExt.boxed__impl_consensus_model_chained_bft_chained_bft_smr_{{impl}}_1_fetch_and_process_proposal_{{opaque}}_T_P
futures_util.future.FutureExt.unit_error__core_pin_Pin_alloc_boxed_Box_dyn_dyn
futures_util.try_future.TryFutureExt.compat__futures_util_future_unit_error_UnitError_core_pin_Pin_alloc_boxed_Box_dyn_dyn
tokio.runtime.threadpool.task_executor.implement.spawn__futures_util_compat_compat03as01_Compat_futures_util_future_unit_error_UnitError_core_pin_Pin_alloc_boxed_Box_dyn_dyn
futures_locks.rwlock.implement_futures_locks_rwlock_RwLock_T.write__consensus_model_chained_bft_event_processor_EventProcessor_T_P
core.option.implement.as_ref__consensus_model_chained_bft_liveness_timeout_msg_PacemakerTimeoutCertificate
core.option.implement.unwrap_or_else__alloc_vec_Vec_alloc_sync_Arc_consensus_model_chained_bft_consensus_types_block_Block_T_fn_alloc_vec_{{impl}}_new_alloc_sync_Arc_consensus_model_chained_bft_consensus_types_block_Block_T
futures_channel.oneshot.implement_futures_channel_oneshot_Sender_T.send__consensus_model_chained_bft_network_BlockRetrievalResponse_T
alloc.fmt.format_
failure.error_message.err_msg__alloc_string_String
prometheus.counter.implement_prometheus_counter_GenericCounter_P.inc_by__prometheus_atomic64_fallback_RwlockAtomic_i64
std.time.implement.now_
core.result.implement.is_err__tuple_0_consensus_model_chained_bft_consensus_types_block_BlockVerificationError
std.time.implement.elapsed_
futures_util.sink.SinkExt.send__channel_WithGauge_futures_channel_mpsc_Sender_core_result_Result_network_validator_network_Event_network_proto_consensus_ConsensusMsg_failure_error_Error_core_result_Result_network_validator_network_Event_network_proto_consensus_ConsensusMsg_failure_error_Error
alloc.vec.implement.remove__consensus_model_chained_bft_consensus_types_block_Block_T
core.slice.implement.last__consensus_model_chained_bft_consensus_types_block_Block_T
core.ops.index.Index.index__alloc_vec_Vec_consensus_model_chained_bft_consensus_types_block_Block_T_usize
core.slice.implement.reverse__consensus_model_chained_bft_consensus_types_block_Block_T
rand.rngs.thread.thread_rng_
rand.Rng.gen_range__rand_rngs_thread_ThreadRng_usize_usize_usize
core.time.implement.from_secs_
core.num.implement_u32.pow_
core.ops.arith.Mul.mul__core_time_Duration_u32
core.cmp.PartialOrd.ge__std_time_Instant_std_time_Instant
std.time.implement.duration_since_
core.option.implement.map__core_time_Duration_core_time_Duration_closure_consensus_model_chained_bft_sync_manager_retrieval_timeout_{{closure}}_i32_FnPtr
futures_locks.mutex.implement_futures_locks_mutex_Mutex_T.lock__tuple_0
futures_locks.mutex.implement_futures_locks_mutex_Mutex_T.new__tuple_0
futures_locks.mutex.implement_futures_locks_mutex_Mutex_T.try_unwrap__tuple_0
std.time.implement_std_time_SystemTime.now_
std.time.implement_std_time_SystemTime.duration_since_
core.cmp.PartialOrd.le__std_time_Instant_std_time_Instant
core.ops.arith.Sub.sub__core_time_Duration_core_time_Duration
core.cmp.PartialOrd.lt__core_time_Duration_core_time_Duration
core.ops.arith.Add.add__core_time_Duration_core_time_Duration
core.cmp.PartialOrd.gt__core_time_Duration_core_time_Duration
grpcio.env.implement.new_
grpcio.env.implement.name_prefix__ref_str
grpcio.env.implement.build_
grpcio.channel.implement.new_
grpcio.channel.implement.connect_
slog.implement_slog_Level.as_usize_
slog.__slog_static_max_level_
slog.implement_slog_FilterLevel.as_usize_
slog.implement_slog_Record.new_
slog.implement.log__alloc_sync_Arc_dyn_dyn
metrics.op_counters.implement.new_and_registered__ref_str
metrics.op_counters.implement.gauge_
metrics.op_counters.implement.counter_
metrics.op_counters.implement.histogram_
lazy_static.lazy.implement.get__metrics_op_counters_OpMetrics_fn_consensus_model_counters_{{impl}}_deref___static_ref_initialize
core.cmp.PartialEq.eq__crypto_hash_HashValue_crypto_hash_HashValue
core.ops.try.Try.into_result__core_result_Result_tuple_0_core_fmt_Error
core.convert.From.from__core_fmt_Error_core_fmt_Error
core.ops.try.Try.from_error__core_result_Result_tuple_0_core_fmt_Error
core.ops.deref.Deref.deref__alloc_vec_Vec_consensus_model_chained_bft_liveness_timeout_msg_PacemakerTimeout
core.slice.implement.iter__consensus_model_chained_bft_liveness_timeout_msg_PacemakerTimeout
core.clone.Clone.clone__alloc_sync_Arc_consensus_model_chained_bft_consensus_types_block_Block_T
core.iter.traits.iterator.Iterator.map__alloc_vec_IntoIter_consensus_model_chained_bft_consensus_types_quorum_cert_QuorumCert_tuple_2_crypto_hash_HashValue_consensus_model_chained_bft_consensus_types_quorum_cert_QuorumCert_closure_consensus_model_chained_bft_block_storage_block_store_{{impl}}_build_block_tree_{{closure}}_{{closure}}_T_i16_FnPtr
core.iter.traits.iterator.Iterator.collect__core_iter_adapters_Map_alloc_vec_IntoIter_consensus_model_chained_bft_consensus_types_quorum_cert_QuorumCert_closure_consensus_model_chained_bft_block_storage_block_store_{{impl}}_build_block_tree_{{closure}}_{{closure}}_T_i16_FnPtr
core.pin.implement_core_pin_Pin_P.new_unchecked__ref_mut_core_pin_Pin_alloc_boxed_Box_dyn_dyn
std.future.poll_with_tls_context__core_pin_Pin_alloc_boxed_Box_dyn_dyn
core.result.implement_core_result_Result_T_E.expect__consensus_model_state_replication_StateComputeResult_failure_error_Error
core.result.implement_core_result_Result_T_E.unwrap__std_sync_rwlock_RwLockReadGuard_consensus_model_chained_bft_block_storage_block_tree_BlockTree_T_std_sys_common_poison_PoisonError_std_sync_rwlock_RwLockReadGuard_consensus_model_chained_bft_block_storage_block_tree_BlockTree_T
core.result.implement.map_err__consensus_model_state_replication_StateComputeResult_failure_error_Error_consensus_model_chained_bft_block_storage_InsertError_closure_consensus_model_chained_bft_block_storage_block_store_{{impl}}_execute_and_insert_block_{{closure}}_{{closure}}_T_i32_FnPtr
core.ops.deref.DerefMut.deref_mut__std_sync_rwlock_RwLockWriteGuard_consensus_model_chained_bft_block_storage_block_tree_BlockTree_T
slog_scope.with_logger__closure_consensus_model_chained_bft_block_storage_block_store_{{impl}}_prune_tree_{{closure}}_{{closure}}_T_i32_FnPtr
crypto.hash.CryptoHash.hash__consensus_model_chained_bft_consensus_types_block_Block_T
core.convert.AsRef.as_ref__alloc_sync_Arc_consensus_model_chained_bft_consensus_types_quorum_cert_QuorumCert_consensus_model_chained_bft_consensus_types_quorum_cert_QuorumCert
protobuf.repeated.implement_protobuf_repeated_RepeatedField_T.into_iter__network_proto_consensus_Block
proto_conv.FromProto.from_proto__consensus_model_chained_bft_consensus_types_block_Block_T
core.option.implement.ok_or_else__crypto_hash_HashValue_failure_error_Error_closure_consensus_model_chained_bft_sync_manager_{{impl}}_process_highest_ledger_info_{{closure}}_{{closure}}_T_i32_FnPtr
std.collections.hash.map.implement_std_collections_hash_map_HashMap_K_V_S.keys__types_account_address_AccountAddress_crypto_signing_Signature_std_collections_hash_map_RandomState
core.cmp.Ord.min__u32
core.iter.traits.collect.IntoIterator.into_iter__alloc_vec_Vec_consensus_model_chained_bft_consensus_types_quorum_cert_QuorumCert
core.ops.deref.Deref.deref__alloc_sync_Arc_dyn_dyn
core.option.implement.expect__consensus_model_state_replication_ExecutedState
core.cmp.PartialEq.eq__consensus_model_state_replication_ExecutedState_consensus_model_state_replication_ExecutedState
core.iter.traits.iterator.Iterator.next__alloc_vec_IntoIter_consensus_model_chained_bft_consensus_types_block_Block_T
core.ops.try.Try.into_result__core_result_Result_consensus_model_state_replication_StateComputeResult_consensus_model_chained_bft_block_storage_InsertError
core.convert.From.from__consensus_model_chained_bft_block_storage_InsertError_consensus_model_chained_bft_block_storage_InsertError
core.ops.try.Try.from_error__core_result_Result_alloc_sync_Arc_consensus_model_chained_bft_consensus_types_block_Block_T_consensus_model_chained_bft_block_storage_InsertError
core.clone.Clone.clone__consensus_model_chained_bft_consensus_types_block_Block_T
core.cmp.PartialEq.ne__network_proto_consensus_BlockRetrievalStatus_network_proto_consensus_BlockRetrievalStatus
Rust version (rustc --version): rustc 1.37.0-nightly (0beb2ba16 2019-07-02)
MIRAI seems to treat all expressions like !e
as logical negation, while Rust does support bitwise negation operation. This makes Z3 crash due to typing errors.
Run MIRAI for the utf8-range crate (v1.0.3) reproduces the crash. More specifically, the crash is triggered when analyzing the function Utf8Sequences::next
.
The analysis should terminate without errors.
An error message from Z3 before crash: Error: Sort mismatch at argument #1 for function (declare-fun not (Bool) Bool) supplied sort is Int
Rust version 1.37.0-nightly (5f3656ce9 2019-06-11)
Write the code to
a) find every function/method body in the crate being compiled and
b) load MIR for the body and then traverse the body, visiting every MIR instruction for abstract interpretation.
If Vec::new()
is used then MIRAI knows that the vector's length is initially zero. It vec![]
is used in place of Vec::new()
then MIRAI does not know that the vector is initially empty.
#[macro_use]
extern crate mirai_annotations;
pub fn main() {
let v: Vec<i32> = vec![];
verify!(v.len() == 0);
}
No errors or warnings.
possible false verification condition
Rust version: rustc 1.38.0-nightly (6e310f2ab 2019-07-07)
Flesh out abstract_domains.rs, abstract_value.rs, constant_value.rs, etc, by:
Create a separate logger for Mirai and emit a log message to capture how Mirai is being run.
In some cases, the mangled function name that MIRAI produces does not include a type when it should.
#![feature(type_alias_enum_variants)]
#[macro_use]
extern crate mirai_annotations;
pub fn test1(size: u32) -> u32 {
precondition!(size <= u32::max_value());
size
}
pub fn test2(string: &str) -> &str {
precondition!(string.as_bytes().len() <= 100);
string
}
fn main() {
println!("Result1: {}", test1(100));
println!("Result2: {}", test2("test"));
}
MIRAI should mangle the name of u32::max_value()
to include u32
.
MIRAI should mangle the name of string.as_bytes()
to include str
.
The name of u32::max_value()
is mangled as core.num.implement_14.max_value_
.
The name of string.as_bytes
is mangled as core.str.implement_32.as_bytes_
.
Rust version (rustc --version): rustc 1.37.0-nightly (2fe7b3383 2019-06-19)
Name mangling fails when given a function bound with a generic parameter T
via the syntax ::<>
.
Ex: size_of::<u32>
MIRAI will mangle the name of this function to be size_of_
.
Test case:
#![feature(type_alias_enum_variants)]
#[macro_use]
extern crate mirai_annotations;
pub mod foreign_contracts;
use std::{ mem::{size_of} };
enum ConstantTest {}
impl ConstantTest { pub const OVERFLOW_U32: u32 = size_of::<u32>() as u32 * 2 + 1; }
fn main() { let _a = ConstantTest::OVERFLOW_U32; }
Log output should be [INFO mirai::summaries] Summary store has no entry for core.mem.size_of_u32_usize
Log output is: [INFO mirai::summaries] Summary store has no entry for core.mem.size_of_
Rust version (rustc --version): rustc 1.37.0-nightly (7cdaffd79 2019-06-05)
Building the standard library is somewhat special. Here are instructions from the Miri project:
rustup component add --toolchain nightly rust-src
cargo +nightly install xargo
rustup run nightly xargo/build.sh
One of the first things to figure out is how to run Mirai over the standard library code and to output summaries that can be used in the same way as summaries for any other crate.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
๐ Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. ๐๐๐
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google โค๏ธ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.