Address some PR comments

Cargo.lock

@@ -108,6 +108,9 @@ checksum = "630be753d4e58660abd17930c71b647fe46c27ea6b63cc59e1e3851406972e42"
 [[package]]
 name = "boogie_ast"
 version = "0.30.0"
+dependencies = [
+ "num-bigint",
+]
 
 [[package]]
 name = "bookrunner"

boogie_ast/Cargo.toml

@@ -11,3 +11,4 @@ publish = false
 # See more keys and their definitions at https://doc.rust-lang.org/cargo/reference/manifest.html
 
 [dependencies]
+num-bigint = "0.4.3"

boogie_ast/src/boogie_program/mod.rs

@@ -1,8 +1,13 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
+//! A module that defines the AST of a Boogie program and provides methods for
+//! creating nodes of the AST.
+
 mod writer;
 
+use num_bigint::{BigInt, BigUint};
+
 struct TypeDeclaration {}
 struct ConstDeclaration {}
 struct VarDeclaration {}
@@ -35,13 +40,10 @@ pub enum Literal {
     Bool(bool),
 
     /// Bit-vector values, e.g. `5bv8`
-    Bv {
-        width: usize,
-        value: String, // TODO: use bigint
-    },
+    Bv { width: usize, value: BigUint },
 
-    /// Unbounded integer values, e.g. `1000`
-    Int(String), // TODO: use bigint
+    /// Unbounded integer values, e.g. `1000` or `-456789`
+    Int(BigInt),
 }
 
 /// Unary operators
@@ -149,7 +151,7 @@ pub enum Stmt {
     While { condition: Expr, body: Box<Stmt> },
 }
 
-/// Procedure specification
+/// Contract specification
 pub struct Contract {
     /// Pre-conditions
     requires: Vec<Expr>,
@@ -161,6 +163,8 @@ pub struct Contract {
 }
 
 /// Procedure definition
+/// A procedure is a function that has a contract specification and that can
+/// have side effects
 pub struct Procedure {
     name: String,
     parameters: Vec<Parameter>,
@@ -182,6 +186,7 @@ impl Procedure {
 }
 
 /// Function definition
+/// A function in Boogie is a mathematical function
 struct Function {}
 
 /// A boogie program
@@ -236,24 +241,24 @@ impl BoogieProgram {
                         Stmt::Decl { name: "y".to_string(), typ: Type::Int },
                         Stmt::Assignment {
                             target: "x".to_string(),
-                            value: Expr::Literal(Literal::Int("1".to_string())),
+                            value: Expr::Literal(Literal::Int(1.into())),
                         },
                         Stmt::Assignment {
                             target: "y".to_string(),
-                            value: Expr::Literal(Literal::Int("2".to_string())),
+                            value: Expr::Literal(Literal::Int(2.into())),
                         },
                         Stmt::Assert {
                             condition: Expr::BinaryOp {
                                 op: BinaryOp::Eq,
                                 left: Box::new(Expr::Symbol { name: "x".to_string() }),
-                                right: Box::new(Expr::Literal(Literal::Int("1".to_string()))),
+                                right: Box::new(Expr::Literal(Literal::Int(1.into()))),
                             },
                         },
                         Stmt::Assert {
                             condition: Expr::BinaryOp {
                                 op: BinaryOp::Eq,
                                 left: Box::new(Expr::Symbol { name: "y".to_string() }),
-                                right: Box::new(Expr::Literal(Literal::Int("2".to_string()))),
+                                right: Box::new(Expr::Literal(Literal::Int(2.into()))),
                             },
                         },
                         Stmt::If {

boogie_ast/src/boogie_program/writer.rs

@@ -2,7 +2,50 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 //! A writer for Boogie programs.
-
+//! Generates a text Boogie program with the following format:
+//! ```
+//! // Type declarations:
+//! <Type declaration 1>
+//! <Type declaration 2>
+//! ...
+//!
+//! // Constant declarations:
+//! <Const declaration 1>
+//! <Const declaration 2>
+//! ...
+//!
+//! // Variable declarations:
+//! var <var-name1>: <type1>;
+//! var <var-name2>: <type2>;
+//! ...
+//!
+//! // Axioms
+//! axiom <expr1>;
+//! axiom <expr2>;
+//! ...
+//!
+//! // Functions:
+//! function <function1-name>(<arg1>: <type1>, ...) returns (return-var-name: <return-type>)
+//! {
+//!   <body>
+//! }
+//! ...
+//!
+//! // Procedures:
+//! procedure <procedure1-name>(<arg1>: <type1>, ...) returns (return-var-name: <return-type>)
+//! requires <pre-condition1>;
+//! requires <pre-condition2>;
+//! ...
+//! ensures <post-condition1>;
+//! ensures <post-condition2>;
+//! ...
+//! modifies <var1>, <var2>, ...;
+//! {
+//!   <body>
+//! }
+//! ...
+//!
+///! ```
 use crate::boogie_program::*;
 
 use std::io::Write;
@@ -55,13 +98,41 @@ impl BoogieProgram {
 
 impl Writable for BoogieProgram {
     fn write_to<T: Write>(&self, writer: &mut Writer<T>) -> std::io::Result<()> {
-        for _td in &self.type_declarations {}
-        for _const_decl in &self.const_declarations {}
-        for _var_decl in &self.var_declarations {}
-        for _a in &self.axioms {}
-        for _f in &self.functions {}
-        for p in &self.procedures {
-            writer.write(p)?;
+        if !self.type_declarations.is_empty() {
+            writeln!(writer.writer, "// Type declarations:")?;
+            for _td in &self.type_declarations {
+                todo!()
+            }
+        }
+        if !self.const_declarations.is_empty() {
+            writeln!(writer.writer, "// Constant declarations:")?;
+            for _const_decl in &self.const_declarations {
+                todo!()
+            }
+        }
+        if !self.var_declarations.is_empty() {
+            writeln!(writer.writer, "// Variable declarations:")?;
+            for _var_decl in &self.var_declarations {
+                todo!()
+            }
+        }
+        if !self.axioms.is_empty() {
+            writeln!(writer.writer, "// Axioms:")?;
+            for _a in &self.axioms {
+                todo!()
+            }
+        }
+        if !self.functions.is_empty() {
+            writeln!(writer.writer, "// Functions:")?;
+            for _f in &self.functions {
+                todo!()
+            }
+        }
+        if !self.procedures.is_empty() {
+            writeln!(writer.writer, "// Procedures:")?;
+            for p in &self.procedures {
+                writer.write(p)?;
+            }
         }
         Ok(())
     }

kani-compiler/src/codegen_boogie/context/boogie_ctx.rs

@@ -16,7 +16,7 @@ use rustc_middle::span_bug;
 use rustc_middle::ty::layout::{
     HasParamEnv, HasTyCtxt, LayoutError, LayoutOf, LayoutOfHelpers, TyAndLayout,
 };
-use rustc_middle::ty::{self, Instance, Ty, TyCtxt};
+use rustc_middle::ty::{self, Instance, IntTy, Ty, TyCtxt, UintTy};
 use rustc_span::Span;
 use rustc_target::abi::{HasDataLayout, TargetDataLayout};
 use tracing::{debug, debug_span, trace};
@@ -281,8 +281,26 @@ impl<'tcx> BoogieCtx<'tcx> {
     pub fn codegen_scalar(&self, s: Scalar, ty: Ty<'tcx>) -> Expr {
         match (s, ty.kind()) {
             (Scalar::Int(_), ty::Bool) => Expr::Literal(Literal::Bool(s.to_bool().unwrap())),
-            (Scalar::Int(i), ty::Int(_)) => Expr::Literal(Literal::Int(i.to_string())),
-            (Scalar::Int(i), ty::Uint(_)) => Expr::Literal(Literal::Int(i.to_string())),
+            (Scalar::Int(_), ty::Int(it)) => match it {
+                IntTy::I8 => Expr::Literal(Literal::Int(s.to_i8().unwrap().into())),
+                IntTy::I16 => Expr::Literal(Literal::Int(s.to_i16().unwrap().into())),
+                IntTy::I32 => Expr::Literal(Literal::Int(s.to_i32().unwrap().into())),
+                IntTy::I64 => Expr::Literal(Literal::Int(s.to_i64().unwrap().into())),
+                IntTy::I128 => Expr::Literal(Literal::Int(s.to_i128().unwrap().into())),
+                IntTy::Isize => {
+                    Expr::Literal(Literal::Int(s.to_target_isize(self).unwrap().into()))
+                }
+            },
+            (Scalar::Int(_), ty::Uint(it)) => match it {
+                UintTy::U8 => Expr::Literal(Literal::Int(s.to_u8().unwrap().into())),
+                UintTy::U16 => Expr::Literal(Literal::Int(s.to_u16().unwrap().into())),
+                UintTy::U32 => Expr::Literal(Literal::Int(s.to_u32().unwrap().into())),
+                UintTy::U64 => Expr::Literal(Literal::Int(s.to_u64().unwrap().into())),
+                UintTy::U128 => Expr::Literal(Literal::Int(s.to_u128().unwrap().into())),
+                UintTy::Usize => {
+                    Expr::Literal(Literal::Int(s.to_target_isize(self).unwrap().into()))
+                }
+            },
             _ => todo!(),
         }
     }

kani-compiler/src/codegen_boogie/overrides/hooks.rs

@@ -5,8 +5,6 @@
 //!
 //! E.g.: Functions in the Kani library that generate assumptions or symbolic variables.
 //!
-//! It would be too nasty if we spread around these sort of undocumented hooks in place, so
-//! this module addresses this issue.
 
 use crate::codegen_boogie::BoogieCtx;
 use boogie_ast::boogie_program::{Expr, Stmt};