Add support for function contracts in cprover_bindings.

cprover_bindings/src/goto_program/contract.rs

@@ -0,0 +1,61 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+use super::{Expr, Location};
+use std::fmt::Debug;
+
+/// A `Contract` represents a code contract type.
+/// A contract describes specifications (in the form of preconditions, postconditions, and invariants) of certain expressions.
+/// Further details about the CBMC implementation can be found here -
+/// https://github.com/diffblue/cbmc/blob/develop/doc/cprover-manual/contracts.md
+
+/// Represents a contract on a function, loop, etc.
+#[derive(Clone, Debug)]
+pub enum Contract {
+    FunctionContract { ensures: Vec<Spec>, requires: Vec<Spec> },
+}
+
+/// A `Spec` is a struct for representing the `requires`, `ensures`, and `assigns` clauses in a function contract.
+/// Every expression inside a function contract clause is wrapped into a lambda expression on the CBMC side.
+/// This is because CBMC generates a new symbol for each contract and the symbol needs to be self-contained.
+/// That is, variables that may have only existed in the scope of a function declaration are
+///     treated as binding variables in the lambda expression and hence made available to the contract symbol.
+/// A list of fresh symbols (one for each binding variable in the lambda expression) is stored in `temporary_symbols`.
+/// The binding variables include the return value of the function (may be empty) and the list of function arguments.
+#[derive(Clone, Debug)]
+pub struct Spec {
+    temporary_symbols: Vec<Expr>,
+    clause: Expr,
+    location: Location,
+}
+
+/// Getters
+impl Spec {
+    pub fn temporary_symbols(&self) -> &Vec<Expr> {
+        &self.temporary_symbols
+    }
+
+    pub fn clause(&self) -> &Expr {
+        &self.clause
+    }
+
+    pub fn location(&self) -> &Location {
+        &self.location
+    }
+}
+
+/// Setters
+impl Spec {
+    pub fn with_location(mut self, loc: Location) -> Self {
+        self.location = loc;
+        self
+    }
+}
+
+/// Constructor
+impl Spec {
+    pub fn new(temporary_symbols: Vec<Expr>, clause: Expr, location: Location) -> Self {
+        assert!(temporary_symbols.iter().all(|x| x.is_symbol()), "Variables must be symbols");
+        Spec { temporary_symbols, clause, location }
+    }
+}

cprover_bindings/src/goto_program/mod.rs

@@ -8,6 +8,7 @@
 #![allow(clippy::match_like_matches_macro)]
 
 mod builtin;
+mod contract;
 mod expr;
 mod location;
 mod stmt;
@@ -17,6 +18,7 @@ pub mod symtab_transformer;
 mod typ;
 
 pub use builtin::BuiltinFn;
+pub use contract::{Contract, Spec};
 pub use expr::{
     ArithmeticOverflowResult, BinaryOperator, Expr, ExprValue, SelfOperator, UnaryOperator,
 };

cprover_bindings/src/goto_program/symbol.rs

@@ -1,7 +1,7 @@
 // Copyright Kani Contributors
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 use super::super::utils::aggr_tag;
-use super::{DatatypeComponent, Expr, Location, Parameter, Stmt, Type};
+use super::{Contract, DatatypeComponent, Expr, Location, Parameter, Stmt, Type};
 use crate::{InternStringOption, InternedString};
 
 /// Based off the CBMC symbol implementation here:
@@ -56,6 +56,7 @@ pub enum SymbolModes {
 pub enum SymbolValues {
     Expr(Expr),
     Stmt(Stmt),
+    Contract(Contract),
     None,
 }
 /// Constructors
@@ -128,6 +129,29 @@ impl Symbol {
         )
     }
 
+    pub fn contract<T: Into<InternedString>, U: Into<InternedString>>(
+        name: T,
+        base_name: U,
+        typ: Type,
+        contract: Contract,
+        loc: Location,
+    ) -> Symbol {
+        let name = name.into();
+        // Both base name and pretty name contain the name of the function that the contract is written for.
+        let base_name: InternedString = base_name.into();
+        let pretty_name = base_name;
+        Symbol::new(
+            name,
+            loc,
+            typ,
+            SymbolValues::Contract(contract),
+            Some(base_name),
+            Some(pretty_name),
+        )
+        // CBMC distinguishes between contract symbols and object or function symbols using this flag.
+        .with_is_property(true)
+    }
+
     pub fn constant(
         name: &str,
         pretty_name: &str,
@@ -283,6 +307,11 @@ impl Symbol {
         self
     }
 
+    pub fn with_is_property(mut self, v: bool) -> Symbol {
+        self.is_property = v;
+        self
+    }
+
     pub fn with_is_thread_local(mut self, v: bool) -> Symbol {
         self.is_thread_local = v;
         self
@@ -341,24 +370,31 @@ impl Symbol {
 }
 
 impl SymbolValues {
+    pub fn is_contract(&self) -> bool {
+        match self {
+            SymbolValues::Contract(_) => true,
+            SymbolValues::None | SymbolValues::Expr(_) | SymbolValues::Stmt(_) => false,
+        }
+    }
+
     pub fn is_expr(&self) -> bool {
         match self {
             SymbolValues::Expr(_) => true,
-            SymbolValues::None | SymbolValues::Stmt(_) => false,
+            SymbolValues::None | SymbolValues::Contract(_) | SymbolValues::Stmt(_) => false,
         }
     }
 
     pub fn is_none(&self) -> bool {
         match self {
             SymbolValues::None => true,
-            SymbolValues::Expr(_) | SymbolValues::Stmt(_) => false,
+            SymbolValues::Contract(_) | SymbolValues::Expr(_) | SymbolValues::Stmt(_) => false,
         }
     }
 
     pub fn is_stmt(&self) -> bool {
         match self {
             SymbolValues::Stmt(_) => true,
-            SymbolValues::Expr(_) | SymbolValues::None => false,
+            SymbolValues::Contract(_) | SymbolValues::Expr(_) | SymbolValues::None => false,
         }
     }
 }

cprover_bindings/src/goto_program/symtab_transformer/transformer.rs

@@ -2,8 +2,8 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 
 use crate::goto_program::{
-    BinaryOperator, CIntType, DatatypeComponent, Expr, ExprValue, Location, Parameter,
-    SelfOperator, Stmt, StmtBody, SwitchCase, Symbol, SymbolTable, SymbolValues, Type,
+    BinaryOperator, CIntType, Contract, DatatypeComponent, Expr, ExprValue, Location, Parameter,
+    SelfOperator, Spec, Stmt, StmtBody, SwitchCase, Symbol, SymbolTable, SymbolValues, Type,
     UnaryOperator,
 };
 use crate::InternedString;
@@ -55,6 +55,9 @@ pub trait Transformer: Sized {
             Type::IncompleteStruct { tag } => self.transform_type_incomplete_struct(*tag),
             Type::IncompleteUnion { tag } => self.transform_type_incomplete_union(*tag),
             Type::InfiniteArray { typ } => self.transform_type_infinite_array(typ),
+            Type::MathematicalFunction { domain, codomain } => {
+                self.transform_type_mathematical_function(domain, codomain)
+            }
             Type::Pointer { typ } => self.transform_type_pointer(typ),
             Type::Signedbv { width } => self.transform_type_signedbv(width),
             Type::Struct { tag, components } => self.transform_type_struct(*tag, components),
@@ -154,6 +157,15 @@ pub trait Transformer: Sized {
         transformed_typ.infinite_array_of()
     }
 
+    fn transform_type_mathematical_function(&mut self, domain: &[Type], codomain: &Type) -> Type {
+        let transformed_domain = domain.iter().map(|x| self.transform_type(x)).collect();
+        let transformed_codomain = self.transform_type(codomain);
+        Type::MathematicalFunction {
+            domain: transformed_domain,
+            codomain: Box::new(transformed_codomain),
+        }
+    }
+
     /// Transforms a pointer type (`typ*`)
     fn transform_type_pointer(&mut self, typ: &Type) -> Type {
         let transformed_typ = self.transform_type(typ);
@@ -240,6 +252,30 @@ pub trait Transformer: Sized {
         transformed_typ.to_typedef(tag)
     }
 
+    /// Transforms a contract data structure by recursively transforming its clauses.
+    fn transform_contract(&mut self, c: &Contract) -> Contract {
+        match c {
+            Contract::FunctionContract { ensures, requires } => {
+                let transformed_ensures =
+                    ensures.iter().map(|spec| self.transform_spec(spec)).collect();
+                let transformed_requires =
+                    requires.iter().map(|spec| self.transform_spec(spec)).collect();
+                Contract::FunctionContract {
+                    ensures: transformed_ensures,
+                    requires: transformed_requires,
+                }
+            }
+        }
+    }
+
+    /// Transforms a `Spec` data structure.
+    fn transform_spec(&mut self, spec: &Spec) -> Spec {
+        let transformed_symbols =
+            spec.temporary_symbols().iter().map(|s| self.transform_expr(s)).collect();
+        let transformed_clause = self.transform_expr(spec.clause());
+        Spec::new(transformed_symbols, transformed_clause, *spec.location())
+    }
+
     /// Perform recursive descent on a `Expr` data structure.
     /// Extracts the variant's field data, and passes them into
     /// the corresponding expr transformer method along with the expr type.
@@ -704,6 +740,9 @@ pub trait Transformer: Sized {
     fn transform_value(&mut self, value: &SymbolValues) -> SymbolValues {
         match value {
             SymbolValues::None => SymbolValues::None,
+            SymbolValues::Contract(contract) => {
+                SymbolValues::Contract(self.transform_contract(contract))
+            }
             SymbolValues::Expr(expr) => SymbolValues::Expr(self.transform_expr(expr)),
             SymbolValues::Stmt(stmt) => SymbolValues::Stmt(self.transform_stmt(stmt)),
         }

cprover_bindings/src/goto_program/typ.rs

@@ -48,6 +48,8 @@ pub enum Type {
     IncompleteUnion { tag: InternedString },
     /// CBMC specific. `typ x[__CPROVER_infinity()]`
     InfiniteArray { typ: Box<Type> },
+    /// Corresponds to `mathematical_function_typet` in CBMC. Used to represent type signatures.
+    MathematicalFunction { domain: Vec<Type>, codomain: Box<Type> },
     /// `typ*`
     Pointer { typ: Box<Type> },
     /// `int<width>_t`. e.g. `int32_t`
@@ -178,6 +180,7 @@ impl DatatypeComponent {
             | IncompleteStruct { .. }
             | IncompleteUnion { .. }
             | InfiniteArray { .. }
+            | MathematicalFunction { .. }
             | VariadicCode { .. } => false,
 
             TypeDef { .. } => unreachable!("typedefs should have been unwrapped"),
@@ -343,6 +346,9 @@ impl Type {
             IncompleteStruct { .. } => unreachable!("IncompleteStruct doesn't have a sizeof"),
             IncompleteUnion { .. } => unreachable!("IncompleteUnion doesn't have a sizeof"),
             InfiniteArray { .. } => unreachable!("InfiniteArray doesn't have a sizeof"),
+            MathematicalFunction { .. } => {
+                unreachable!("MathematicalFunction doesn't have a sizeof")
+            }
             Pointer { .. } => st.machine_model().pointer_width,
             Signedbv { width } => *width,
             Struct { components, .. } => {
@@ -552,6 +558,7 @@ impl Type {
             | IncompleteStruct { .. }
             | IncompleteUnion { .. }
             | InfiniteArray { .. }
+            | MathematicalFunction { .. }
             | VariadicCode { .. } => false,
 
             TypeDef { .. } => unreachable!("Expected concrete type only."),
@@ -601,6 +608,7 @@ impl Type {
             | IncompleteStruct { .. }
             | IncompleteUnion { .. }
             | InfiniteArray { .. }
+            | MathematicalFunction { .. }
             | Struct { .. }
             | StructTag(_)
             | Union { .. }
@@ -891,6 +899,7 @@ impl Type {
             | IncompleteStruct { .. }
             | IncompleteUnion { .. }
             | InfiniteArray { .. }
+            | MathematicalFunction { .. }
             | VariadicCode { .. } => false,
 
             TypeDef { .. } => unreachable!("typedefs should have been unwrapped"),
@@ -1304,6 +1313,18 @@ impl Type {
             Type::InfiniteArray { typ } => {
                 format!("infinite_array_of_{}", typ.to_identifier())
             }
+            Type::MathematicalFunction { domain, codomain } => {
+                let domain_string = domain
+                    .iter()
+                    .map(|domain| domain.to_identifier())
+                    .collect::<Vec<_>>()
+                    .join("_");
+                format!(
+                    "mathematical_functional_from_{}_to_{}",
+                    domain_string,
+                    codomain.to_identifier()
+                )
+            }
             Type::Pointer { typ } => format!("pointer_to_{}", typ.to_identifier()),
             Type::Signedbv { width } => format!("signed_bv_{}", width),
             Type::Struct { tag, .. } => format!("struct_{}", tag),

cprover_bindings/src/irep/irep.rs

@@ -2,7 +2,7 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! The actual `Irep` structure, and associated constructors, getters, and setters.
 
-use super::super::goto_program::{Location, Type};
+use super::super::goto_program::{Contract, Location, Type};
 use super::super::MachineModel;
 use super::{IrepId, ToIrep};
 use crate::cbmc_string::InternedString;
@@ -36,6 +36,20 @@ impl Irep {
 
 /// Fluent Builders
 impl Irep {
+    pub fn with_contract(self, contract: &Contract, mm: &MachineModel) -> Self {
+        match contract {
+            Contract::FunctionContract { requires, ensures } => self
+                .with_named_sub(
+                    IrepId::CSpecEnsures,
+                    Irep::just_sub(ensures.iter().map(|spec| spec.to_irep(mm)).collect()),
+                )
+                .with_named_sub(
+                    IrepId::CSpecRequires,
+                    Irep::just_sub(requires.iter().map(|spec| spec.to_irep(mm)).collect()),
+                ),
+        }
+    }
+
     pub fn with_location(self, l: &Location, mm: &MachineModel) -> Self {
         if !l.is_none() {
             self.with_named_sub(IrepId::CSourceLocation, l.to_irep(mm))