Merge branch 'Add-coverage-prototype' of https://github.com/jaisnan/kani

 into Add-coverage-prototype

cprover_bindings/src/goto_program/builtin.rs

@@ -61,6 +61,7 @@ pub enum BuiltinFn {
     Sinf,
     Sqrt,
     Sqrtf,
+    Sysconf,
     Trunc,
     Truncf,
     Unlink,
@@ -124,6 +125,7 @@ impl ToString for BuiltinFn {
             Sinf => "sinf",
             Sqrt => "sqrt",
             Sqrtf => "sqrtf",
+            Sysconf => "sysconf",
             Trunc => "trunc",
             Truncf => "truncf",
             Unlink => "unlink",
@@ -188,6 +190,7 @@ impl BuiltinFn {
             Sinf => vec![Type::float()],
             Sqrt => vec![Type::double()],
             Sqrtf => vec![Type::float()],
+            Sysconf => vec![Type::c_int()],
             Trunc => vec![Type::double()],
             Truncf => vec![Type::float()],
             Unlink => vec![Type::c_char().to_pointer()],
@@ -251,6 +254,7 @@ impl BuiltinFn {
             Sinf => Type::float(),
             Sqrt => Type::double(),
             Sqrtf => Type::float(),
+            Sysconf => Type::c_long_int(),
             Trunc => Type::double(),
             Truncf => Type::float(),
             Unlink => Type::c_int(),
@@ -314,6 +318,7 @@ impl BuiltinFn {
             Sinf,
             Sqrt,
             Sqrtf,
+            Sysconf,
             Trunc,
             Truncf,
             Unlink,

cprover_bindings/src/goto_program/typ.rs

@@ -27,7 +27,7 @@ pub enum Type {
     Bool,
     /// `typ x : width`. e.g. `unsigned int x: 3`.
     CBitField { typ: Box<Type>, width: u64 },
-    /// Machine dependent integers: `bool`, `char`, `int`, `size_t`, etc.
+    /// Machine dependent integers: `bool`, `char`, `int`, `long int`, `size_t`, etc.
     CInteger(CIntType),
     /// `return_type x(parameters)`
     Code { parameters: Vec<Parameter>, return_type: Box<Type> },
@@ -83,6 +83,8 @@ pub enum CIntType {
     Char,
     /// `int`
     Int,
+    /// `long int`
+    LongInt,
     /// `size_t`
     SizeT,
     /// `ssize_t`
@@ -232,6 +234,7 @@ impl CIntType {
             CIntType::Bool => st.machine_model().bool_width,
             CIntType::Char => st.machine_model().char_width,
             CIntType::Int => st.machine_model().int_width,
+            CIntType::LongInt => st.machine_model().long_int_width,
             CIntType::SizeT => st.machine_model().pointer_width,
             CIntType::SSizeT => st.machine_model().pointer_width,
         }
@@ -287,6 +290,7 @@ impl Type {
             CInteger(CIntType::Bool) => Some(mm.bool_width),
             CInteger(CIntType::Char) => Some(mm.char_width),
             CInteger(CIntType::Int) => Some(mm.int_width),
+            CInteger(CIntType::LongInt) => Some(mm.long_int_width),
             Signedbv { width } | Unsignedbv { width } => Some(*width),
             _ => None,
         }
@@ -450,6 +454,14 @@ impl Type {
         }
     }
 
+    pub fn is_long_int(&self) -> bool {
+        let concrete = self.unwrap_typedef();
+        match concrete {
+            Type::CInteger(CIntType::LongInt) => true,
+            _ => false,
+        }
+    }
+
     pub fn is_c_size_t(&self) -> bool {
         let concrete = self.unwrap_typedef();
         match concrete {
@@ -637,7 +649,10 @@ impl Type {
     pub fn is_signed(&self, mm: &MachineModel) -> bool {
         let concrete = self.unwrap_typedef();
         match concrete {
-            CInteger(CIntType::Int) | CInteger(CIntType::SSizeT) | Signedbv { .. } => true,
+            CInteger(CIntType::Int)
+            | CInteger(CIntType::LongInt)
+            | CInteger(CIntType::SSizeT)
+            | Signedbv { .. } => true,
             CInteger(CIntType::Char) => !mm.char_is_unsigned,
             _ => false,
         }
@@ -963,6 +978,10 @@ impl Type {
         CInteger(CIntType::Int)
     }
 
+    pub fn c_long_int() -> Self {
+        CInteger(CIntType::LongInt)
+    }
+
     pub fn c_size_t() -> Self {
         CInteger(CIntType::SizeT)
     }
@@ -1471,6 +1490,7 @@ mod type_tests {
         assert_eq!(type_def.is_empty(), src_type.is_empty());
         assert_eq!(type_def.is_double(), src_type.is_double());
         assert_eq!(type_def.is_bool(), src_type.is_bool());
+        assert_eq!(type_def.is_long_int(), src_type.is_long_int());
         assert_eq!(type_def.is_array(), src_type.is_array());
         assert_eq!(type_def.is_array_like(), src_type.is_array_like());
         assert_eq!(type_def.is_union(), src_type.is_union());

cprover_bindings/src/irep/to_irep.rs

@@ -589,6 +589,11 @@ impl ToIrep for Type {
                 sub: vec![],
                 named_sub: linear_map![(IrepId::Width, Irep::just_int_id(mm.int_width),)],
             },
+            Type::CInteger(CIntType::LongInt) => Irep {
+                id: IrepId::Signedbv,
+                sub: vec![],
+                named_sub: linear_map![(IrepId::Width, Irep::just_int_id(mm.long_int_width),)],
+            },
             Type::CInteger(CIntType::SizeT) => Irep {
                 id: IrepId::Unsignedbv,
                 sub: vec![],

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

@@ -157,6 +157,7 @@ impl<'tcx> GotocCtx<'tcx> {
                         cbmc::goto_program::CIntType::Bool => "bool",
                         cbmc::goto_program::CIntType::Char => "char",
                         cbmc::goto_program::CIntType::Int => "int",
+                        cbmc::goto_program::CIntType::LongInt => "long int",
                         cbmc::goto_program::CIntType::SizeT => "size_t",
                         cbmc::goto_program::CIntType::SSizeT => "ssize_t",
                     };

kani-compiler/src/kani_compiler.rs

@@ -33,6 +33,7 @@ use rustc_hir::definitions::DefPathHash;
 use rustc_interface::Config;
 use rustc_middle::ty::TyCtxt;
 use rustc_session::config::{ErrorOutputType, OutputType};
+use rustc_session::EarlyErrorHandler;
 use rustc_span::ErrorGuaranteed;
 use std::collections::{BTreeMap, HashMap};
 use std::fs::File;
@@ -372,6 +373,7 @@ impl Callbacks for KaniCompiler {
     /// During the initialization state, we collect the crate harnesses and prepare for codegen.
     fn after_analysis<'tcx>(
         &mut self,
+        _handler: &EarlyErrorHandler,
         _compiler: &rustc_interface::interface::Compiler,
         rustc_queries: &'tcx rustc_interface::Queries<'tcx>,
     ) -> Compilation {

kani-compiler/src/session.rs

@@ -9,6 +9,8 @@ use rustc_errors::{
     emitter::Emitter, emitter::HumanReadableErrorType, fallback_fluent_bundle, json::JsonEmitter,
     ColorConfig, Diagnostic, TerminalUrl,
 };
+use rustc_session::config::ErrorOutputType;
+use rustc_session::EarlyErrorHandler;
 use std::io::IsTerminal;
 use std::panic;
 use std::str::FromStr;
@@ -71,7 +73,8 @@ pub fn init_session(args: &ArgMatches, json_hook: bool) {
     // Initialize the rustc logger using value from RUSTC_LOG. We keep the log control separate
     // because we cannot control the RUSTC log format unless if we match the exact tracing
     // version used by RUSTC.
-    rustc_driver::init_rustc_env_logger();
+    let handler = EarlyErrorHandler::new(ErrorOutputType::default());
+    rustc_driver::init_rustc_env_logger(&handler);
 
     // Install Kani panic hook.
     if json_hook {

kani-dependencies

@@ -1,4 +1,4 @@
-CBMC_VERSION="5.87.0"
+CBMC_VERSION="5.88.1"
 # If you update this version number, remember to bump it in `src/setup.rs` too
 CBMC_VIEWER_VERSION="3.8"
 KISSAT_VERSION="3.0.0"

kani-driver/Cargo.toml

@@ -26,7 +26,7 @@ regex = "1.6"
 rustc-demangle = "0.1.21"
 pathdiff = "0.2.1"
 rayon = "1.5.3"
-comfy-table = "6.0.0"
+comfy-table = "7.0.1"
 strum = {version = "0.24.0"}
 strum_macros = {version = "0.24.0"}
 tracing = {version = "0.1", features = ["max_level_trace", "release_max_level_debug"]}

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2023-06-24"
+channel = "nightly-2023-07-01"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]

scripts/kani-regression.sh

@@ -19,7 +19,7 @@ KANI_DIR=$SCRIPT_DIR/..
 export KANI_FAIL_ON_UNEXPECTED_DESCRIPTION="true"
 
 # Required dependencies
-check-cbmc-version.py --major 5 --minor 86
+check-cbmc-version.py --major 5 --minor 88
 check-cbmc-viewer-version.py --major 3 --minor 8
 check_kissat_version.sh
 

tests/kani/LibC/sysconf.rs

@@ -0,0 +1,12 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//
+//! Check support for `sysconf`.
+
+#![feature(rustc_private)]
+extern crate libc;
+
+#[kani::proof]
+fn main() {
+    let page_size = unsafe { libc::sysconf(libc::_SC_PAGESIZE) } as usize;
+}