model-checking / kani Goto Github PK
View Code? Open in Web Editor NEWKani Rust Verifier
Home Page: https://model-checking.github.io/kani
License: Apache License 2.0
Kani Rust Verifier
Home Page: https://model-checking.github.io/kani
License: Apache License 2.0
Dynamic trait inside a box. Test implemented: gotoc-dynamic-trait-box but currently failing/not parsing through rustc.
Summarize current SSA interface, how we might use it, what might need to be fixed.
According to @danielsn:
volatile
has two meanings: one is just that we can't reorder or drop the access, which CBMC never does.
It might also mean that reads should return nondet
, which we don't currently model.
The code for this would be in intrinsics.rs
use std::io::{sink, Write};
fn main() {
let mut log : Box<dyn Write + Send> = Box::new(sink());
let dest : Box<dyn Write + Send> = Box::new(log.as_mut());
}
Fails with an unhandled pointer cast exception.
Relevant comment in intrinsics.rs
// Codegens a simple intrinsic: ie. one which maps directly to a matching goto construct
// We need to use this macro form because of a known limitation in rust
// `codegen_simple_intrinsic!(self.get_sqrt(), Type::float())` gives the error message:
// error[E0499]: cannot borrow `*self` as mutable more than once at a time
// --> src/librustc_codegen_llvm/gotoc/intrinsic.rs:76:63
// |
// 76 | codegen_simple_intrinsic!(self.get_sqrt(), Type::double())
// | ---- ------------------------ ^^^^ second mutable borrow occurs here
// | | |
// | | first borrow later used by call
// | first mutable borrow occurs here
// To solve this, we need to store the `self.get_sqrt()` into a temporary variable.
// Using the macro form allows us to keep the call as a oneliner, while still making rust happy.
GitHub actions for regression testing and PR blocking
The intended semantics of the function codegen_alloc_in_memory
are difficult to infer from the code and the documentation. The semantics of the Allocation type is hard to understand, so the codegen of the Allocation data is hard to trust. The definition of codegen_alloc_in_memory
allows the function to be called with an Allocation and a String name, but the name may or may not be present in the symbol table. It is hard to understand why any invocation would call with the name already in the symbol table. Consider rewriting this function to do nothing but create a new symbol in the table with the bit pattern type and a bit pattern value. Consider another function that transmutes the value to the type of a symbol already in the symbol table.
#![feature(layout_for_ptr)]
use std::mem;
use std::sync::Arc;
use std::sync::Mutex;
pub trait Subscriber {
fn process(&mut self);
fn interest_list(&self);
}
struct DummySubscriber {
}
impl DummySubscriber {
fn new() -> Self {
DummySubscriber {}
}
}
impl Subscriber for DummySubscriber {
fn process(&mut self) {}
fn interest_list(&self) {}
}
fn main() {
let v = unsafe { mem::size_of_val_raw(&5i32) };
assert!(v == 4);
let x : [u8;13] = [0; 13];
let y: &[u8] = &x;
let v = unsafe { mem::size_of_val_raw(y) };
assert!(v == 13);
let s : Arc<Mutex<dyn Subscriber>> = Arc::new(Mutex::new(DummySubscriber::new()));
}
This test requires an additional check in struct_type()
of cbmc/goto_program/typ.rs
to ensure that the struct's components are unique. In this case, the vtable contains two foo
fn pointers.
trait A {
fn foo(&self) -> i32;
}
trait B {
fn foo(&self) -> i32;
}
trait T : A + B {
}
struct S {
x : i32,
y : i32,
}
impl S {
fn new(a:i32, b:i32) -> S {
S {x:a, y:b}
}
fn new_box(a:i32, b:i32) -> Box<dyn T> {
Box::new(S::new(a,b))
}
}
impl A for S {
fn foo(&self) -> i32{
self.x
}
}
impl B for S {
fn foo(&self) -> i32{
self.y
}
}
impl T for S {
}
fn main() {
let t = S::new_box(1,2);
let a = <dyn T as A>::foo(&*t);
assert!(a == 1);
let b = <dyn T as B>::foo(&*t);
assert!(b == 2);
}
For the Electrolysis-style dashboard.
const SIZE1: usize = 1;
const SIZE2: usize = 2;
pub static TABLE1: [(u64, u64); SIZE1] = [
(0, 0),
];
pub static TABLE2: [(u64, u64); SIZE2] = [
(0, 0),
(0, 0),
];
fn main() {
assert!(TABLE1[0].0 == 0);
}
Fails with:
thread 'rustc' panicked at 'assertion failed: `(left == right)`
left: `256`,
right: `128`', compiler/rustc_codegen_llvm/src/gotoc/cbmc/goto_program/expr.rs:686
use std::path::Path;
fn main() {
let path = Path::new("./foo/bar.txt");
}
Fails with a can't cast exception
Can we track the name of variables so we get
main::square::vol
instead of main::Shape[0]::vtable main$$Shape[0]$$vtable_impl_for_&main$$Rectangle[0]
?
Grep for it, and see if there is a span we can use instead
Instead of taking a c in gen_function_local_variable, maintain a map from fname to int, and generate fresh variables that way. Actually: why is this index needed at all? It seems to be part of constructing a name, but unique names shouldn't rely on someone hand-picking the right index. Instead, a map of names should be kept, and the next available slot should be chosen.
See the comments on gotoc-assert-eq/main.rs
Rename typing contexts to be consistent with:
There are a couple of PRs that will add support for count builtins in CBMC. This will allow the count intrinsics code in RMC to be simplified and its regression tests to be enabled.
Inventory of how we're currently hooked in (what features we use)
Needed in firecracker/balloon-compact example
Source-based coverage report generation is an experimental feature of the Rust compiler that we need to explore further. A prototype implementation will allow us to discover any limitations that may influence the way we plan to structure the RMC testing suite.
Have cases that test what happens if the length is not greater than the min length
This should apply to both the main test, and the volatile atomic test.
Test: ForeignItems/fixme_main.rs
Currently unstable atomic tests use only u8
values, but we should extend them to work with all integer values supported in Kani.
Depends on source-based coverage reports. The reorganization will probably follow a chapter-like structure that follows the Rust reference.
See the comments on gotoc-assert-eq/main.rs
Given a structure and confidence scores.
Currently, we iterate through the table, which will be slow for large symbol tables
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.