Skip to content

Commit

Permalink
Merge branch 'main' into derive-invariant-2
Browse files Browse the repository at this point in the history
  • Loading branch information
@adpaco-aws
adpaco-aws committed Jul 17, 2024
2 parents f42e724 + 852fd8f commit ca962ed
Show file tree
Hide file tree
Showing 70 changed files with 1,672 additions and 385 deletions.
94 changes: 47 additions & 47 deletions Cargo.lock
View file
Original file line number Diff line number Diff line change
Expand Up @@ -140,19 +140,19 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"

[[package]]
name = "clap"
version = "4.5.8"
version = "4.5.9"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "84b3edb18336f4df585bc9aa31dd99c036dfa5dc5e9a2939a722a188f3a8970d"
checksum = "64acc1846d54c1fe936a78dc189c34e28d3f5afc348403f28ecf53660b9b8462"
dependencies = [
"clap_builder",
"clap_derive",
]

[[package]]
name = "clap_builder"
version = "4.5.8"
version = "4.5.9"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "c1c09dd5ada6c6c78075d6fd0da3f90d8080651e2d6cc8eb2f1aaa4034ced708"
checksum = "6fb8393d67ba2e7bfaf28a23458e4e2b543cc73a99595511eb207fdb8aede942"
dependencies = [
"anstream",
"anstyle",
Expand All @@ -169,7 +169,7 @@ dependencies = [
"heck",
"proc-macro2",
"quote",
"syn 2.0.68",
"syn 2.0.71",
]

[[package]]
Expand Down Expand Up @@ -482,7 +482,7 @@ dependencies = [
"proc-macro-error",
"proc-macro2",
"quote",
"syn 2.0.68",
"syn 2.0.71",
]

[[package]]
Expand Down Expand Up @@ -909,29 +909,29 @@ dependencies = [

[[package]]
name = "serde"
version = "1.0.203"
version = "1.0.204"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "7253ab4de971e72fb7be983802300c30b5a7f0c2e56fab8abfc6a214307c0094"
checksum = "bc76f558e0cbb2a839d37354c575f1dc3fdc6546b5be373ba43d95f231bf7c12"
dependencies = [
"serde_derive",
]

[[package]]
name = "serde_derive"
version = "1.0.203"
version = "1.0.204"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "500cbc0ebeb6f46627f50f3f5811ccf6bf00643be300b4c3eabc0ef55dc5b5ba"
checksum = "e0cd7e117be63d3c3678776753929474f3b04a43a080c744d6b0ae2a8c28e222"
dependencies = [
"proc-macro2",
"quote",
"syn 2.0.68",
"syn 2.0.71",
]

[[package]]
name = "serde_json"
version = "1.0.119"
version = "1.0.120"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "e8eddb61f0697cc3989c5d64b452f5488e2b8a60fd7d5076a3045076ffef8cb0"
checksum = "4e0d21c9a8cae1235ad58a00c11cb40d4b1e5c784f1ef2c537876ed6ffd8b7c5"
dependencies = [
"itoa",
"ryu",
Expand Down Expand Up @@ -1030,7 +1030,7 @@ dependencies = [
"proc-macro2",
"quote",
"rustversion",
"syn 2.0.68",
"syn 2.0.71",
]

[[package]]
Expand All @@ -1045,9 +1045,9 @@ dependencies = [

[[package]]
name = "syn"
version = "2.0.68"
version = "2.0.71"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "901fa70d88b9d6c98022e23b4136f9f3e54e4662c3bc1bd1d84a42a9a0f0c1e9"
checksum = "b146dcf730474b4bcd16c311627b31ede9ab149045db4d6088b3becaea046462"
dependencies = [
"proc-macro2",
"quote",
Expand All @@ -1068,22 +1068,22 @@ dependencies = [

[[package]]
name = "thiserror"
version = "1.0.61"
version = "1.0.62"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "c546c80d6be4bc6a00c0f01730c08df82eaa7a7a61f11d656526506112cc1709"
checksum = "f2675633b1499176c2dff06b0856a27976a8f9d436737b4cf4f312d4d91d8bbb"
dependencies = [
"thiserror-impl",
]

[[package]]
name = "thiserror-impl"
version = "1.0.61"
version = "1.0.62"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "46c3384250002a6d5af4d114f2845d37b57521033f30d5c3f46c4d70e1197533"
checksum = "d20468752b09f49e909e55a5d338caa8bedf615594e9d80bc4c565d30faf798c"
dependencies = [
"proc-macro2",
"quote",
"syn 2.0.68",
"syn 2.0.71",
]

[[package]]
Expand Down Expand Up @@ -1119,9 +1119,9 @@ dependencies = [

[[package]]
name = "toml_edit"
version = "0.22.14"
version = "0.22.15"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "f21c7aaf97f1bd9ca9d4f9e73b0a6c74bd5afef56f2bc931943a6e1c37e04e38"
checksum = "d59a3a72298453f564e2b111fa896f8d07fabb36f51f06d7e875fc5e0b5a3ef1"
dependencies = [
"indexmap",
"serde",
Expand Down Expand Up @@ -1149,7 +1149,7 @@ checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7"
dependencies = [
"proc-macro2",
"quote",
"syn 2.0.68",
"syn 2.0.71",
]

[[package]]
Expand Down Expand Up @@ -1320,9 +1320,9 @@ dependencies = [

[[package]]
name = "windows-targets"
version = "0.52.5"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "6f0713a46559409d202e70e28227288446bf7841d3211583a4b53e3f6d96e7eb"
checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973"
dependencies = [
"windows_aarch64_gnullvm",
"windows_aarch64_msvc",
Expand All @@ -1336,51 +1336,51 @@ dependencies = [

[[package]]
name = "windows_aarch64_gnullvm"
version = "0.52.5"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "7088eed71e8b8dda258ecc8bac5fb1153c5cffaf2578fc8ff5d61e23578d3263"
checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3"

[[package]]
name = "windows_aarch64_msvc"
version = "0.52.5"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "9985fd1504e250c615ca5f281c3f7a6da76213ebd5ccc9561496568a2752afb6"
checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469"

[[package]]
name = "windows_i686_gnu"
version = "0.52.5"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "88ba073cf16d5372720ec942a8ccbf61626074c6d4dd2e745299726ce8b89670"
checksum = "8e9b5ad5ab802e97eb8e295ac6720e509ee4c243f69d781394014ebfe8bbfa0b"

[[package]]
name = "windows_i686_gnullvm"
version = "0.52.5"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "87f4261229030a858f36b459e748ae97545d6f1ec60e5e0d6a3d32e0dc232ee9"
checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66"

[[package]]
name = "windows_i686_msvc"
version = "0.52.5"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "db3c2bf3d13d5b658be73463284eaf12830ac9a26a90c717b7f771dfe97487bf"
checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66"

[[package]]
name = "windows_x86_64_gnu"
version = "0.52.5"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "4e4246f76bdeff09eb48875a0fd3e2af6aada79d409d33011886d3e1581517d9"
checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78"

[[package]]
name = "windows_x86_64_gnullvm"
version = "0.52.5"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "852298e482cd67c356ddd9570386e2862b5673c85bd5f88df9ab6802b334c596"
checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d"

[[package]]
name = "windows_x86_64_msvc"
version = "0.52.5"
version = "0.52.6"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "bec47e5bfd1bff0eeaf6d8b485cc1074891a197ab4225d504cb7a1ab88b02bf0"
checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec"

[[package]]
name = "winnow"
Expand All @@ -1399,20 +1399,20 @@ checksum = "d135d17ab770252ad95e9a872d365cf3090e3be864a34ab46f48555993efc904"

[[package]]
name = "zerocopy"
version = "0.7.34"
version = "0.7.35"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "ae87e3fcd617500e5d106f0380cf7b77f3c6092aae37191433159dda23cfb087"
checksum = "1b9b4fd18abc82b8136838da5d50bae7bdea537c574d8dc1a34ed098d6c166f0"
dependencies = [
"zerocopy-derive",
]

[[package]]
name = "zerocopy-derive"
version = "0.7.34"
version = "0.7.35"
source = "registry+https://github.com/rust-lang/crates.io-index"
checksum = "15e934569e47891f7d9411f1a451d947a60e000ab3bd24fbb970f000387d1b3b"
checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e"
dependencies = [
"proc-macro2",
"quote",
"syn 2.0.68",
"syn 2.0.71",
]
68 changes: 61 additions & 7 deletions kani-compiler/src/codegen_cprover_gotoc/codegen/contract.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@
use crate::codegen_cprover_gotoc::GotocCtx;
use crate::kani_middle::attributes::KaniAttributes;
use cbmc::goto_program::FunctionContract;
use cbmc::goto_program::{Lambda, Location};
use cbmc::goto_program::{Expr, Lambda, Location, Type};
use kani_metadata::AssignsContract;
use rustc_hir::def_id::DefId as InternalDefId;
use rustc_smir::rustc_internal;
Expand All @@ -12,6 +12,8 @@ use stable_mir::mir::Local;
use stable_mir::CrateDef;
use tracing::debug;

use stable_mir::ty::{RigidTy, TyKind};

impl<'tcx> GotocCtx<'tcx> {
/// Given the `proof_for_contract` target `function_under_contract` and the reachable `items`,
/// find or create the `AssignsContract` that needs to be enforced and attach it to the symbol
Expand Down Expand Up @@ -122,7 +124,7 @@ impl<'tcx> GotocCtx<'tcx> {
.tcx
.all_diagnostic_items(())
.name_to_id
.get(&rustc_span::symbol::Symbol::intern("KaniMemInitShadowMem"))
.get(&rustc_span::symbol::Symbol::intern("KaniMemoryInitializationState"))
.map(|attr_id| {
self.tcx
.symbol_name(rustc_middle::ty::Instance::mono(self.tcx, *attr_id))
Expand All @@ -142,11 +144,63 @@ impl<'tcx> GotocCtx<'tcx> {
let assigns = modified_places
.into_iter()
.map(|local| {
Lambda::as_contract_for(
&goto_annotated_fn_typ,
None,
self.codegen_place_stable(&local.into(), loc).unwrap().goto_expr.dereference(),
)
if self.is_fat_pointer_stable(self.local_ty_stable(local)) {
let unref = match self.local_ty_stable(local).kind() {
TyKind::RigidTy(RigidTy::Ref(_, ty, _)) => ty,
kind => unreachable!("{:?} is not a reference", kind),
};
let size = match unref.kind() {
TyKind::RigidTy(RigidTy::Slice(elt_type)) => {
elt_type.layout().unwrap().shape().size.bytes()
}
TyKind::RigidTy(RigidTy::Str) => 1,
// For adt, see https://rust-lang.zulipchat.com/#narrow/stream/182449-t-compiler.2Fhelp
TyKind::RigidTy(RigidTy::Adt(..)) => {
todo!("Adt fat pointers not implemented")
}
kind => unreachable!("Generating a slice fat pointer to {:?}", kind),
};
Lambda::as_contract_for(
&goto_annotated_fn_typ,
None,
Expr::symbol_expression(
"__CPROVER_object_upto",
Type::code(
vec![
Type::empty()
.to_pointer()
.as_parameter(None, Some("ptr".into())),
Type::size_t().as_parameter(None, Some("size".into())),
],
Type::empty(),
),
)
.call(vec![
self.codegen_place_stable(&local.into(), loc)
.unwrap()
.goto_expr
.member("data", &self.symbol_table)
.cast_to(Type::empty().to_pointer()),
self.codegen_place_stable(&local.into(), loc)
.unwrap()
.goto_expr
.member("len", &self.symbol_table)
.mul(Expr::size_constant(
size.try_into().unwrap(),
&self.symbol_table,
)),
]),
)
} else {
Lambda::as_contract_for(
&goto_annotated_fn_typ,
None,
self.codegen_place_stable(&local.into(), loc)
.unwrap()
.goto_expr
.dereference(),
)
}
})
.chain(shadow_memory_assign)
.collect();
Expand Down
2 changes: 1 addition & 1 deletion kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -574,7 +574,7 @@ impl<'tcx> GotocCtx<'tcx> {
ty::Ref(_, t, _) | ty::RawPtr(t, _) => self.codegen_ty_ref(*t),
ty::FnDef(def_id, args) => {
let instance =
Instance::resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, args)
Instance::try_resolve(self.tcx, ty::ParamEnv::reveal_all(), *def_id, args)
.unwrap()
.unwrap();
self.codegen_fndef_type(instance)
Expand Down
Loading

0 comments on commit ca962ed

Please sign in to comment.