LLVMFunctionContract.md

For common LLVM function contracts it may be useful for SAW users to simply specity the function's signature and pre/postconditions and let the low-level SAW boilerplate (e.g., the Python equivalents to crucible_fresh_var, crucible_alloc, etc) be done automatically since they're fairly predictable.

E.g., The abstract function contract class might look as follows:

class LLVMFunctionContract(metaclass=ABCMeta):
    def parameter_types(self) -> List[LLVMParamType]:
        """The parameter types for the function."""
        pass

    def return_type(self) -> LLVMReturnType:
        """The return type for the function."""
        pass

    def preconditions(self, *params : SetupVal) -> None:
        """Makes any necessary precondition assertions.
        
        N.B., this function will be called with ``len(self.parameter_types())`` positional arguments, 
        i.e., one representing each argument the function has been declared to have via the
        ``parameter_types`` function."""
        pass

    def postconditions(self, *params : SetupVal) -> None:
        """Makes any necessary postcondition assertions.
        
        N.B., this function will be called with ``len(self.parameter_types()) + 1`` positional arguments, 
        i.e., one for each argument the function has been declared to have via the ``param_types`` function and."""
        pass

    def _call_pre(self):
        if self.param_types() is None:
            raise ValueError("param_types was not set!")
        # arguments would be initialized appropriately here automatically,
        # saved so they can also be passed later to the post condition
        # function
        # and then passed to the preconditions function
        self.preconditions(*self.param_types())

    def _call_post(self):
        if self.param_types() is None:
            raise ValueError("param_types was not set!")
        self.postconditions(*self.param_types())

Users are expected to then implement the parameter_types and return_type methods. The values returned by those two functions could then be used to automatically generate all fresh vars, allocated pointers, etc, and pass them to the users' implementations of preconditions and postconditions, which could then simply focus on stating the intended correctness properties about those values (e.g., asserting what they equal, what they point to, etc).

Here is a simple example of such a contract for a function plus that adds two i32s:

class PlusContract(LLVMFunctionContract):
    def param_types(self):
        return [llvm.i32, llvm.i32]

    def return_type(self):
        return llvm.i32

    def preconditions(self, x, y):
        pass # There are no assertions to make about `x` and `y`

    def postconditions(self, x, y, result):
        self.proclaim(result == x + y)

Behind the scenes (if you will) the parent class LLVMFunctionContract would be calling fresh_var for the two parameters and for the return value, and it simply passes those values to preconditions and postconditions where assertions can be made.

To make this work well, we'd probably need to come up with some intuitive types for parameters and return types that are both straightforward and unambiguously tell the parent class how to properly instantiate them. E.g., we wouldn't want to just say a parameter was a llvm.ptr(llvm.i32), we would need to at least have the possibility to say a little more, such as whether or not it is allocated, etc, perhaps that can be achieved conveniently via some simple/intuitive keyword arguments (e.g., llvm.ptr(llvm.i32, allocated=True)) or via multiple clearly-named constructors.