Update charon

zhassan-aws · Aug 28, 2024 · c3e21ae · c3e21ae
1 parent d6a7e72
commit c3e21ae
Show file tree

Hide file tree

Showing 3 changed files with 70 additions and 13 deletions.
diff --git a/Cargo.lock b/Cargo.lock
@@ -274,7 +274,7 @@ checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd"
 
 [[package]]
 name = "charon"
-version = "0.1.30"
+version = "0.1.33"
 dependencies = [
  "anyhow",
  "assert_cmd",
@@ -523,6 +523,15 @@ dependencies = [
  "syn 1.0.109",
 ]
 
+[[package]]
+name = "deranged"
+version = "0.3.11"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "b42b6fa04a440b495c8b04d0e71b707c585f83cb9cb28cf8cd0d976c315e31b4"
+dependencies = [
+ "powerfmt",
+]
+
 [[package]]
 name = "derivative"
 version = "2.2.0"
@@ -980,6 +989,7 @@ dependencies = [
  "strum",
  "strum_macros",
  "tempfile",
+ "time",
  "toml",
  "tracing",
  "tracing-subscriber",
@@ -1206,6 +1216,12 @@ dependencies = [
  "num-traits",
 ]
 
+[[package]]
+name = "num-conv"
+version = "0.1.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "51d515d32fb182ee37cda2ccdcb92950d6a3c2893aa280e540671c2cd0f3b1d9"
+
 [[package]]
 name = "num-integer"
 version = "0.1.46"
@@ -1347,6 +1363,12 @@ version = "0.2.14"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "bda66fc9667c18cb2758a2ac84d1167245054bcf85d5d1aaa6923f45801bdd02"
 
+[[package]]
+name = "powerfmt"
+version = "0.2.0"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "439ee305def115ba05938db6eb1644ff94165c5ab5e9420d1c1bcedbba909391"
+
 [[package]]
 name = "ppv-lite86"
 version = "0.2.17"
@@ -2006,6 +2028,37 @@ dependencies = [
  "num_cpus",
 ]
 
+[[package]]
+name = "time"
+version = "0.3.36"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "5dfd88e563464686c916c7e46e623e520ddc6d79fa6641390f2e3fa86e83e885"
+dependencies = [
+ "deranged",
+ "itoa",
+ "num-conv",
+ "powerfmt",
+ "serde",
+ "time-core",
+ "time-macros",
+]
+
+[[package]]
+name = "time-core"
+version = "0.1.2"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ef927ca75afb808a4d64dd374f00a2adf8d0fcff8e7b184af886c3c87ec4a3f3"
+
+[[package]]
+name = "time-macros"
+version = "0.2.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "3f252a68540fde3a3877aeea552b832b40ab9a69e318efd078774a01ddee1ccf"
+dependencies = [
+ "num-conv",
+ "time-core",
+]
+
 [[package]]
 name = "toml"
 version = "0.8.14"

diff --git a/charon b/charon
diff --git a/kani-compiler/src/codegen_aeneas_llbc/context/mod.rs b/kani-compiler/src/codegen_aeneas_llbc/context/mod.rs
@@ -15,7 +15,7 @@ use charon_lib::ast::Rvalue as CharonRvalue;
 use charon_lib::ast::Span as CharonSpan;
 use charon_lib::ast::{make_locals_generator, AbortKind, Body as CharonBody, Var, VarId};
 use charon_lib::ast::{
-    AnyTransId, AssumedTy, BodyId, Disambiguator, FileName, FunDecl, FunSig, GenericArgs,
+    AnyTransId, Assert, BodyId, BuiltinTy, Disambiguator, FileName, FunDecl, FunSig, GenericArgs,
     GenericParams, IntegerTy, ItemKind, ItemMeta, ItemOpacity, Literal, LiteralTy, Name, Opaque,
     PathElem, RawConstantExpr, RefKind, Region, ScalarValue, TranslatedCrate, TypeId,
 };
@@ -29,7 +29,7 @@ use charon_lib::ast::{
 use charon_lib::common::Error;
 use charon_lib::errors::ErrorCtx;
 use charon_lib::ids::Vector;
-use charon_lib::transform::{TransformCtx, ctx::TransformOptions};
+use charon_lib::transform::{ctx::TransformOptions, TransformCtx};
 use charon_lib::ullbc_ast::{
     BlockData, BlockId, BodyContents, ExprBody, RawStatement, RawTerminator,
     Statement as CharonStatement, SwitchTargets as CharonSwitchTargets,
@@ -43,7 +43,8 @@ use rustc_smir::rustc_internal;
 use stable_mir::abi::PassMode;
 use stable_mir::mir::mono::Instance;
 use stable_mir::mir::{
-    BasicBlock, BinOp, Body, BorrowKind, CastKind, ConstOperand, Mutability, Operand, Place, ProjectionElem, Rvalue, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind
+    BasicBlock, BinOp, Body, BorrowKind, CastKind, ConstOperand, Mutability, Operand, Place,
+    ProjectionElem, Rvalue, Statement, StatementKind, SwitchTargets, Terminator, TerminatorKind,
 };
 use stable_mir::ty::{
     Allocation, ConstantKind, IndexedVal, IntTy, MirConst, RigidTy, Span, Ty, TyKind, UintTy,
@@ -64,9 +65,7 @@ pub struct LlbcContext<'tcx> {
 
 impl<'tcx> LlbcContext<'tcx> {
     pub fn new(tcx: TyCtxt<'tcx>, queries: QueryDb) -> Self {
-        let options = TransformOptions {
-            no_code_duplication: false,
-        };
+        let options = TransformOptions { no_code_duplication: false };
         let crate_name = tcx.crate_name(LOCAL_CRATE).as_str().into();
         let translated = TranslatedCrate { crate_name, ..TranslatedCrate::default() };
         let errors = ErrorCtx {
@@ -441,7 +440,7 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> {
             RigidTy::Uint(uit) => CharonTy::Literal(LiteralTy::Integer(translate_uint_ty(uit))),
             RigidTy::Never => CharonTy::Never,
             RigidTy::Str => CharonTy::Adt(
-                TypeId::Assumed(AssumedTy::Str),
+                TypeId::Builtin(BuiltinTy::Str),
                 GenericArgs {
                     regions: Vector::new(),
                     types: Vector::new(),
@@ -578,8 +577,7 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> {
             }
             TerminatorKind::Assert { cond, expected, msg: _, target, .. } => {
                 RawTerminator::Assert {
-                    cond: self.translate_operand(cond),
-                    expected: *expected,
+                    assert: Assert { cond: self.translate_operand(cond), expected: *expected },
                     target: BlockId::from_usize(*target),
                 }
             }
@@ -799,11 +797,17 @@ impl<'a, 'tcx> FunctionCtx<'a, 'tcx> {
         (discr, switch_targets)
     }
 
-    fn translate_projection(&mut self, projection: &Vec<ProjectionElem>) -> Vec<CharonProjectionElem> {
+    fn translate_projection(
+        &mut self,
+        projection: &Vec<ProjectionElem>,
+    ) -> Vec<CharonProjectionElem> {
         projection.iter().map(|elem| self.translate_projection_elem(elem)).collect()
     }
 
-    fn translate_projection_elem(&mut self, projection_elem: &ProjectionElem) -> CharonProjectionElem {
+    fn translate_projection_elem(
+        &mut self,
+        projection_elem: &ProjectionElem,
+    ) -> CharonProjectionElem {
         match projection_elem {
             ProjectionElem::Deref => CharonProjectionElem::Deref,
             _ => todo!(),