Skip to content

Add a mechanism to declare that a function should be kept uninterpreted during symbolic evaluation #2674

@yav

Description

@yav

In SAW we have some prove strategies that can declare that certain functions should be kept uninterpreted when they are sent to the solver. However, in some cases this is too late, because we'd like to also keep the same functions uninterpreted during symbolic evaluation (i.e., while computing what we need to prove). Here's an example illustrating the problem:

example.c

unsigned char c_ID(unsigned char x) { return x; }
unsigned char c_FIVE(unsigned char y) { return c_ID(5)+y; }

Example.cry

module Example where

cry_ID : [8] -> [8]
cry_ID x = x

cry_FIVE : [8] -> [8]
cry_FIVE y = cry_ID 5 + y

Example.saw

m <- llvm_load_module "example.bc";

import "Example.cry";

thm_id <- llvm_verify
  m "c_ID" [] false
  do {
    X <- llvm_fresh_var "X" (llvm_int 8);
    llvm_execute_func [llvm_term X];
    llvm_return (llvm_term {{ cry_ID X }} );
  }
  rme;

thm_five <- llvm_verify
  m "c_FIVE" [thm_id] false
  do {
    Y <- llvm_fresh_var "Y" (llvm_int 8);
    llvm_execute_func [llvm_term Y];
    llvm_return (llvm_term {{ cry_FIVE Y }});
  }
  do {
    print_goal;
    w4_unint_rme ["cry_ID"];
  };

This script first proves that the function c_ID behaves like cry_ID, successfully( thm_id). Unfortunately, we fail to prove that function c_FIVE behaves like cry_FIVE, using theorem thm_id. The goal we cannot discharge is (essentially) that cry_FIVE Y = 5 + Y.
The problem is that cry_FIVE Y expands to cry_ID 5 + Y, which is not equal to 5 + Y because we specified that we'd like to keep cry_ID uninterpreted. The RHS was computed during symbolic evaluation, where we knew that c_ID behaves like cry_ID (from thm_id) and then we just reduced cry_ID 5 to just 5.

The reason we'd like to keep terms uninterpreted sometimes is that if we expand their definitions the complexity of the terms can explode, and verification fails.

To work around this problem, I propose that we add a way to declare that certain functions should be kept uninterpreted during symbolic simulation. This is similar to what we do in crux-mir-comp. This can be specified either as additional parameters to llvm_verify or as another command that can be involved in the setup parameter to llvm_verify

Metadata

Metadata

Assignees

No one assigned

    Labels

    needs testIssues for which we should add a regression testsubsystem: crucible-jvmIssues related to Java verification with crucible-jvmsubsystem: crucible-llvmIssues related to LLVM bitcode verification with crucible-llvmsubsystem: crucible-mirIssues related to Rust verification with crucible-mir and/or mir-jsonsubsystem: saw-scriptIssues related to the SAWScript language and/or its interpretation and executiontype: bugIssues reporting bugs or unexpected/unwanted behavior

    Type

    No type

    Projects

    No projects

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions