How do you tell Frama-C and Eva that an entry point's parameters are assumed valid?

Question

Take the following C code example.

struct foo_t {
    int bar;
};

int my_entry_point(const struct foo_t *foo) {
    return foo->bar;
}

In our case, my_entry_point will be called from assembly, and *foo here must be assumed to always be correct.

Running with the command line...

frama-c -eva -report -report-classify -report-unclassified-warning ERROR -c11 -main my_entry_point /tmp/test.c

... results in ...

[report] Monitoring events
[kernel] Parsing /tmp/override.c (with preprocessing)
[eva] Analyzing a complete application starting at my_entry_point
[eva] Computing initial state
[eva] Initial state computed
[eva:initial-state] Values of globals at initialization

[eva:alarm] /tmp/override.c:6: Warning:
  out of bounds read. assert \valid_read(&foo->bar);
[eva] done for function my_entry_point
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function my_entry_point:
  __retres ∈ [--..--]
[eva:summary] ====== ANALYSIS SUMMARY ======
  ----------------------------------------------------------------------------
  1 function analyzed (out of 1): 100% coverage.
  In this function, 2 statements reached (out of 2): 100% coverage.
  ----------------------------------------------------------------------------
  No errors or warnings raised during the analysis.
  ----------------------------------------------------------------------------
  1 alarm generated by the analysis:
       1 invalid memory access
  ----------------------------------------------------------------------------
  No logical properties have been reached by the analysis.
  ----------------------------------------------------------------------------
[report] Classification
[ERROR:eva.unclassified.warning] Unclassified Warning (Plugin 'eva')
[REVIEW:unclassified.unknown] my_entry_point_assert_Eva_mem_access
[report] Reviews     :    1
[report] Errors      :    1
[report] Unclassified:    2
[report] User Error: Classified errors found
[kernel] Plug-in report aborted: invalid user input.

Of course, we can always add a base-case NULL check, which satisfies the checker (this is probably how we'll solve this for now, anyway).

if (!foo) return 0;

But I'm more curious (for learning purposes) about how this might be done with e.g. ACSL annotations telling the checker "hey, we understand this is pointer could, in theory, be invalid - however, please assume that, since it's the entry point, it is indeed valid".

Is this something that ACSL supports, or can the behavior be altered via command line arguments to frama-c? I can see why the standards committee might be hesitant on adding such a mechanism to ACSL since it could be abused, but seeing as how I'm just learning ACSL I was curious to know what the common approach might be here.

Answer 1

ACSL has no intrinsic notion of "analysis' initial state", or "entry point". Each analysis, modular or not, has its own notion of initial context. For instance, WP is modular, so its initial state are the preconditions of the function currently being analyzed. In Eva, the whole-program analysis has an initial state closer to C11's "5.1.2.1. Freestanding environment" than to "5.1.2.2. Hosted environment", in the sense that, while the default initial function is called main, the user may override it with another function name, and initial parameters are defined by Eva's notion of context, with related options (-eva-context-depth, -eva-context-width, -eva-context-valid-pointers).

So, in your case, setting -eva-context-valid-pointers will work. Note that this option affects all pointers created for the initial state, so it can be a problem if there are multiple pointer arguments.

Another solution is to write a precondition such as /*@ requires \valid_read(foo); */. It will not be proven by Eva (it will remain as Unknown), but it will be taken into account during the analysis, thus preventing the alarm from being emitted. Future versions of Frama-C might include an admit (or similar keyword) to be able to state such properties and consider them as valid.

Finally, for more complex situations, a more sophisticated initial context may be required, and there are plug-ins to do so, but not in the open-source distribution. What is often done in such cases is to manually write a stub function to create the initial state before calling the function. Some Frama-C built-in functions such as Frama_C_interval can be used to help create this state. An example of an initial state, where argv may have up to 5 arbitrary strings, each up to 256 characters long, is available here. This stub-based approach offers more precision, e.g. if you have a complex struct containing several pointer fields as initial context, but it requires more effort.

Answer 2

The requires (here, something like \valid(foo) clause means exactly that: from the point of view of the callee, it is something it can assume, since it is up to the caller (or in the particular case of the main entry point, the outside world) to guarantee that the execution of the function will start in a state that respects the pre-condition.

However, in your particular case, there's a catch: for technical reasons, Eva does create an initial context first, and then reduce it according to the pre-condition. Hence, you'll get a warning that the requires is unknown.

Generally speaking, the usual way to let Eva start in a specific context is to write a small wrapper function, potentially using the built-ins mentioned in section 9.2.1 of the Eva manual. There are also a few options (described in section 6.3 of the manual) that control the way the initial state is computed. If you don't need too precise information about the initial state, they might be sufficient (e.g. too just ensure that foo and any other pointer is valid, use -eva-context-valid-pointers)

Finally, there have been experiments on generating a wrapper function from ACSL requires clause (see this paper), but as far as I know the corresponding plug-in is not freely available.