GitLab

Type declarations for records (incuding the private records) can
now be followed by a "witness": a set of values for the record
fields that must satisfy the type invariant (if any). The fields
must be initialized with pure terminating program expressions.
The current syntax, proposed by Martin, is

    type t 'a = { f: ty1; g: ty2 }
      invariant { J[f,g] }
      by { f = e1; g = e2 }

The generated proof obligation is the VC for

    let g = e2 in let f = e1 in assert { J[f,g] }

In absence of an explicit witness, an existential proof obligation
"exists f,g. J[f,g]" is produced.

Without an argument, break and continue refer to the innermost loop.
A label put over an expression sequence starting with a loop, can be
used as an optional argument for break and continue:

  label L in
  [ghost] ["tag"] [M.begin]
    while true do
      ...
      break L
      ...
    done;
    [...]
  [end] [: unit]

In the square brackets are listed the constructions allowed between
the label declaration and the loop expression.

eval_match should not destruct user-written quantifiers.
For this purpose it preserves all quantifiers inside annotations.
For the same purpose it now also preserves all quantifiers appearing
inside terms in let-bindings (in particular, inside lambdas).

This commit also contains a fix for a curious exploit of our type
system which was made possible by a combination of local exceptions
and a special treatment of abstract blocks and whiteboxes.

Local exceptions allow us to exploit the type inference mechanism
and to force the same regions onto unrelated expressions. This is due
to the fact that local exceptions are region-monomorphic (this may be
relaxed in future). Of course, this was always possible via the API,
and the false aliases do not threaten the soundness of the system,
thanks to the following critical invariant:

  An allocation of a new mutable value always has an associated reset
  effect which invalidates the existing variables of the same type.

So, if two variables share a region, then exactly one of three
conditions must hold:

1. They are actually aliased, and modification of one must change
   the other in the VC.

2. They are not aliased, but the newer one invalidates the other:
   this is a case of false alias made benign by the reset effect.

3. The shared region is not actually reachable from the newer one:
        let x = if true then None else Some r
   this is another false alias, without an associated reset effect,
   yet still benign since the shared region is not reachable from x.

However, the type system and the VC generator must have the exact
same view on who's who's alias. If the VCgen encounters in the
same control flow two variables with a shared region in the type,
then the type system must have ensured one of the three conditions
above. Prior to this commit, there were two cases which violated
this:

- An exception raised in an abstract block that does not have
  an exceptional postcondition for it, escapes into the main
  control flow.

- A whitebox, by its nature, is fully handled inside the main
  control flow.

The violation came from the fact that abstract blocks and whiteboxes
are stored as cexps and so their effect is filtered by Ity.create_cty
in order to hide effects on variables allocated and collected inside
the block. This is a useful and necessary feature, except when the
VC of the block escapes into the main control flow and the forced
false aliases -- unchecked by the type system -- are seen by VCgen.
The implemented fix resolves the issue by restoring the hidden
effects for abstract blocks and whiteboxes.

Check bench/programs/bad-typing/false_alias*.mlw for two concrete
examples.

Just as abstract blocks, "white-box blocks" are program expressions
with an additional contract attached to their execution place.
Contrary to abstract blocks, whiteboxes do not hide their contents
from the outer computation. In most cases, you would not need
whiteboxes at all, as the same effect can be achieved by adding
assertions. Their utility comes from their syntax: the added
contract clauses bind to the expression and do not require
additional semicolons, begin-end's, let-in's or try-with's.

Compare:

    let x = <expr> in assert { P x }; x
to  <expr> ensures { P result }
or  <expr> returns { x -> P x }

    if ... then begin let x = <expr> in assert { P x }; x end; ...
to  if ... then <expr> ensures { P result }; ...

    try <expr> with E x -> assert { P x }; raise E x; end
to  <expr> raises { E x -> P x }

Internally, whiteboxes are just abstract blocks (zero-argument
anonymous functions executed in-place) with the label "vc:white_box"
on top. The user never needs to write this label explicitly though.

There is no reason why an abstract block cannot return an alias
with some external variable or exception.

On N127-001, an optimisation of the fast WP was introduced, based on
marking states that contain variables that need to be refreshed when
merging them. However, this "marked" status was incorrectly reset to
false when merging states, even though some of those "unfresh" variables
could survive the merge. The consequence was that the WP was reusing
variables too aggressively, which would result in incorrect VCs.

We now compute the marked status of a merged state from the states to be
merged: if one of them is marked, the merged state is marked too.

mlw_wp.ml:
(merge): synthetize marked status from input states

Change-Id: Ifb02c54fca58137c31762469e48b59e7c907b995

- most important improvement : the explanation, used as first part
  of the shape was computed twice ! (at least)
- several improvements in the implementation, avoid using Format
  in particular (done also in checksum computations)
- possible further improvements:
    do not compute shapes if checksums are OK
       (they must be the same as in previous session)
    do not compute goal checksums if theory checksum is OK
       (they must be the same as in previous session)

This makes the syntax cleaner and brings us closer to OCaml.

One incompatibility with the previous grammar is that "ghost"
binds stronger than the left arrow of assignment, and thus
ghost assignments have to be written as "ghost (x.f <- v)".

This is unavoidable, because assignment has to be weaker than
the tuple comma (think "x.f, y.g <- y.g, x.f" or "a[i] <- u,v"),
and "ghost" has to be stronger than comma, for consistency with
our patterns and our return types.

The "return" construction is weaker than comma, for "return a,b".
It is also weaker than assignment, though "return x.f <- b" does
not make much sense either way.

This change does not concern type expressions, where a tuple
type must always have its clothes^Wparentheses on: (int, int).
It might be nice to write "constant pair: int, bool", but on
the other hand this would break casts like "42: int, true".

This may produce false positives in cases like

  let x, ghost y = true, 3 + 42 (* (+) is logical here *)

The use of curly braces will suppress the warning (TODO).
Otherwise, this behaves reasonably well: there were only
two warnings inside examples/, both valid.

A symbol is now considered overloadable if it satisfies
the following conditions:
  - it has at least one parameter
  - it is non-ghost and has fully visible result
  - all of its parameters are non-ghost and have the same type
  - its result is either of the same type as its parameters
    or it is a monomorphic immutable type.

An overloadable symbol can be combined with other symbols of the
same arity and overloading kind. Otherwise, the new symbol shadows
the previously defined ones.

This generalisation allows us to overload symbols such as "size"
or "length", and also symbols of arbitraty non-zero arity.

I am reluctant to generalize this any further, because then we
won't have reasonable destructible signatures for type inference.

This reverts the enforcing part of a44cccbb.

- requires a lot more testing
- support in extraction missing (exception raised)
- interaction with "syntax literal" remains to investigate

x.{f} is allowed and can be used for unary applications
M.{f} is not allowed, use {M.f} instead