OCM: ESBMC-AI helper methods

[Yiannis128]

There is an issue when comparing results in the equivalence script for certain functions. Functions that return: pointer, array, etc. There is no way to know how the results and equivalence should be checked. Moreover, there are no configurable options on how equivalence should be checked. This issue proposes the implementation of special functions that ESBMC-AI can detect that configure the verification process, these functions start with __ESBMCAI_ and are used by ESBMC-AI, so they aren't invoked by the rest of the source code.

The functions can be included in the source code for configuration reasons, but can be excluded from compilation by ignoring all functions beginning with __ESBMCAI_. The following functions are proposed:

int __ESBMCAI_EQ_X

Overrides the equality logic that ESBMC (the backend) will use. The function starts with __ESBMCAI_EQ_ indicating it is an ESBMC-AI special function for equality checking. The get_from_index names the function that this special function will act as the equality operation for. The parameters for the function should match the return data type of the function.

int __ESBMCAI_EQ_get_from_index(struct LinkedList *a, struct LinkedList *b)
{
    // Do comparison here and return bool result.
    return 0;
}

The function that __ESBMCAI_EQ_get_from_index will act as the equality operator for:

struct LinkedList *get_from_index(struct LinkedList *root, int index)

In the function equivalence script, if a valid function is detected, then the comparison will be changed from:

assert($function_assert_old == $function_assert_new);

To:

assert(__ESBMCAI_EQ_get_from_index($function_assert_old, $function_assert_new));

This allows for any type of function with any data type to be tested.

__ESBMCAI_CFG_X_

Allows for the configuration of properties of function X. Configurable properties:

• int __ESBMCAI_CFG_MINVALUE_X_Y: Configures ESBMC AI to not supply a value less than what the function returns when supplying __VERIFIER_nondet_Z to parameter Y of function X.
• int __ESBMCAI_CFG_MAXVALUE_X_Y: Configures ESBMC AI to not supply a value greater than what the function returns when supplying __VERIFIER_nondet_Z to parameter Y of function X.

Example:

// Configures ESBMC-AI __VERIFIER_nondet_int() > 10 for input parameter index in function get_from_index
int __ESBMCAI_CFG_MINVALUE_get_from_index_index() {
  return 10;
}

Z __ESBMCAI_SETVALUE_X_Y(Z Y)

When function X is being checked for partial equivalence, will call function __ESBMCAI_SETVALUE_X_Y for parameter Y. The parameter to the function will be Z Y where Z is the datatype of the parameter Y in question. The return value of __ESBMCAI_SETVALUE_X_Y will be used as a parameter.

Example, we have a function to be optimized:

struct LinkedList* get_from_index(struct LinkedList* root, int index);

We need to supply rules to that function because the index and the LinkedList provided need to coincide with each other. We can configure both values to relate like so:

Root parameter:

struct LinkedList* __ESBMCAI_SETVALUE_get_from_index_root(struct LinkedList* root) {
  // Logic for constructing a good LinkedList
  return root;
}

Index parameter:

int index __ESBMCAI_SETVALUE_get_from_index_index(int index) {
  // Logic for constructing a good index
  return index;
}

How can we ensure communication between each method? As they don't have means of communicating, this is where the built-in seed function will come into place.

int __ESBMCAI_SEED();

Returns a random seed that for each parameter of the function will be consistent. So same value when called inside __ESBMCAI_SETVALUE_get_from_index_root and __ESBMCAI_SETVALUE_get_from_index_index, this can be used to synchronize behavior.

Tasks

• Implement a method in ClangAST to get list of return statements in a function. Inputs: Function declaration.
• Implement exclusion logic for automatically excluding functions that begin with “__ESBMCAI_CFG_”.
• Implement function parsing during source code parsing phase that will build a list of configuration functions detected. Create object FunctionConfigurator that can return configuration overrides found in source code for each function.
• Implement overriding logic during function equivalence script building step.

[Yiannis128]

Please comment/propose any other properties that should be configured by OCM.

[Yiannis128]

Need to review if Lua should be used as a scripting frontend for users to correctly configure ESBMC-AI OCM.