autofocus for array resource

[MorelElian]

Autofocus

Principle

We want to be able to type-check function calls that require only a subset of array resources:

Basic Example:

void simple_focus(float *y, int n) {
  __modifies(" &y[MINDEX1(n,2)] ~> Cell");

}

void simple_focus_caller(float *x, int m, int n) {
  __modifies("for i1 in 0..n -> &x[MINDEX1(n,i1)] ~> Cell");
  simple_focus(x, n);
}

Will be transformed into

void simple_focus(float* y, int n) {
   __modifies("&y[MINDEX1(n, 2)] ~> Cell");
   __admitted();
}

void simple_focus_caller(float* x, int m, int n) {
  __ghost(focus,
   __modifies("x ~> Matrix1(n)");
   __consumes("x ~> Matrix1(n)");
   __produces("&x[MINDEX1(n, 2)] ~> Cell");
   __admitted();
   __with("justif := focus");");
  simple_focus(x, n);
   __ghost(unfocus,"
   __consumes("&x[MINDEX1(n, 2)] ~> Cell");
   __produces("x ~> Matrix1(n)");
   __admitted();
   __with("justif := focus");");
 
}

Global flow

Whenever a contract needs to be type-checked, each required resource is processed in two steps.
In the first pass, typing is performed without inference or autofocus. If no available resource can satisfy the requirement, inference and autofocus are then enabled.
Among the available resources, we attempt to determine a sequence of simple ghost focuses that can produce the resource expected by the callee.
A focus corresponds to the instantiation of the iterator variable associated with a resource group.
If the resource has multiple dimensions, each focus represents the instantiation of the iterator for one dimension.

A focus is feasible when it is possible to instantiate the iterator to a specific value that yields the index in the required resource.

Once this list of focuses has been determined, we annotate the function call accordingly.
During the final elaboration phase, this ghost sequence is then materialized.

What works for now

For all the cases below, we managed to : catch the need for a focus, compute the focus list, and annotate the corresponding function call

• Simple focus : one dimensional array focused on one cell
• General focus : 4-dimensional array, focused on one of the dimension
• Complex access : Multi-dimensional array, access is "n1-i1" and not only the group index. Therefore, suggest correct instantiation of group index
• Rename and focus : Handling of different names between required resource and the one focused, suggest correct substitution
• Multiple resources : Handling of different resources : suggest that we are able to correctly pick the focused resources

To be tested

Those are notes for me, maybe you see other things ?

• Multiple resources on the same call
• Multiple focus on the same resource
• Loop contract
• Avec indirection a[b[i]]

To be added

Those are notes for me, maybe you see other things ?

• Generic index instantiation : should be able to instantiate group index for index of the form "f(i,a,b..)" -> does not work for now
• RO formula : should be able to work with __reads clauses
• Celle that are modified : __modfies(... ~> UninitCell) which becomes ... ~>Cell: we cannot directly match the reverse ghost with the ghost
• Ghost to reorder the groups, when the group order in the resources does not match the indices order.
  Example :

void f(float*x, int n1, int n2) {
__modifies(for i2 in 0..n2 -> for i1 in 0..n1 -> &x[MINDEX2(n1,n2,i1,i2)] ~> Cell)) ;
__admitted();
}
void f_caller(float*x, int n1, int n2)
{
__modifies(for i1 in 0..n1-> for i2 in 0..n2 -> &x[MINDEX2(n1,n2,i1,i2)] ~> Cell)) ;
f(x,n1,n2);
}

Next steps

• Loop minimization ?
• Models ?

Files change / added

• ast.ml : Added elaborate trm in the trm context
• resource_computation.ml : Added support for autofocus algorithm : infer phase, and re-typing of the ghost sequence.
• resource_autofocus.ml : core autofocus algorithm
• specification.cpp : supported case

Issues

Issue with the ghost:

I am using the function ghost_admitted_rewrite which should produces something like:

__ghost([&]() { ... 

but here i'm only getting :

[&]() { ...}();
} 

I don't see the "ghost call"

Issue with evar_ctx with un-const int

For the following example:

 void complex_access_ok_2(float *x, int n1, int n2, int c_callee) {
  __modifies("for i2 in 0..n2 -> &x[MINDEX2(n1,n2,(c_callee + c_callee) / "
             "2,i2)] ~> Cell");
  __admitted();
}

void complex_access_ok_caller_2(float *x, int n1, int n2) {
  __modifies("for i1 in 0..n1 -> for i2 in 0..n2 -> &x[MINDEX2(n1,n2,(i1+i1) / "
             "2,i2)] ~> "
             "Cell");
  const int c = 3;
  complex_access_ok_2(x, n1, n2, c);
}

If i remove the const from const int c = 3 I am unable to correctly substitute c_callee by c in the contract resource of the complex_access_ok_2 function.
Do you know where does this issue come from ?

Issue with get

Produces a mis-placed seq

Issue with indirection

Not able to type the resource

Questions

• Elaboration is done at the end of the trm_compute_resources, should it be done in another pass / differently ?
  For modifies that transform UninitCell in Cell, which resource should we return? (a Cell + Uninit Cell for the rest of the array ?)
• Should we adapt trm_deep_copy, so that it copies the elaborate field ? (For now, it creates an empty ctx)
• Should I add any case not mentioned here ?
• Extend to other type check than contract (get / set / loop)?

[MorelElian]

To add : modifies in the candidate and a read in the formula
Un example avec des noms différents,
Rajouter un commentaire par cas
Print le ctx