Adds support for sysconf (#2557)

Signed-off-by: Felipe R. Monteiro <felisous@amazon.com>

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",
                     };

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;
+}