Description:
- Choice was made to not add unused variables when there is no contract
and no body (no pre/(x)post, and no body).
- For postcondition variable result, we only check variables that are not
of unit type. And, we report a warning only if the variable is not present
in all the ensures.
- For result variable, with several imbricated raise, it seems possible to
have false positive with no location. Removing the no location case which
seems unhelpful anyway
The warning can be disabled by a debug flag.
The bench was changed so as to accept examples that **should** output
warning but not fail (this category did not exist, it does now) and
label_scope has been switched to it.
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.
The only recent change in master currently ignored in
this merge is renaming mach.Array.Array63.array to array63.
If we decide to give array types in mach.Array specific names,
we should do it for every size, and not only for 63 bits.
split the ppat_ghost field in program patterns into two distinct
conditions:
- ppat_ghost, indicating that the pattern starts as ghost,
meaning that all variables in it are ghost, too;
- ppat_fail, meaning that the pattern contains a refutable
ghost subpattern, which makes the match in the extracted code
impossible, which makes the whole match expression ghost.
Until now, the two conditions were disjunctively combined, making
admissible the invalid pattern matching in bench/p/b-d/ghost4.mlw.
This fixes a soundness bug in WhyML typechecking.
See bench/programs/bad-typing/alias6.mlw for an example
of illegal alias that would go uncatched until now.
- "diverges" states that the computation may not terminate (which
does not mean that is always diverges: just as any other effect
annotation, this clause states a possibility of a side effect).
- "reads {}" states that the computation does not access any variable
except those that are listed elsewhere in the specification (or the
proper function arguments, if "reads" is in a function spec).
- "writes {}" states that the computation does not modify any mutable
value.
- If a function definition or an abstract computation may diverge,
but there is no "diverges" clause in the specification, a warning
is produced. If a function definition or an abstract computation
always terminates, but there is a "diverges" clause in the spec,
an error is produced.
- If there is a "reads" or a "writes" clause in a function definition
or an abstract computation, then every modified value must be listed
in "writes" and every accessed external variable not mentioned in
the spec must be listed in "reads". (Notice that this is a stricter
requirement than before, when the presence of a "writes" clause
did not require to specify "reads".) However, one does not have to
write "reads {}" or "writes {}" if the corresponding lists are empty.
One exception to this rule is the the result type in a non-recursive
function may contain regions coming the function's arguments (though
not from the context). It is sometimes useful to write a function
around a constructor or a projection: see function [create] in
verifythis_fm2012_LRS.mlw. For recursive functions we impose
the full non-alias discipline.
This fixes one bug and several deficiencies in the previous
implementation, which was based on read effects. One caveat
about the current version is that we treat all type variables
in a polymorphic type as visible (= non-ghost) even if they
only occur in the ghost fields. For example, the following
code is rejected:
type strange 'a = { ghost contents : 'a }
let test () =
let x = { contents = ref 0 } in
x.contents := 42
Even though the field [contents] is ghost and cannot be reached
from the real-world code, the type of x is [strange (ref int)]
and the region of the reference is considered to be visible.
Thus the last assignment is seen as an illicit ghost write.
On the other hand,
type strange 'a = { ghost contents : ref 'a }
and
type strange 'a = { ghost mutable contents : 'a }
permit ghost writes into [contents] without problem.
Ghost writes into ghost variables are also okay.
this commit changes the way of tracking occurrences of regions
and type variables for the purposes of generalization, effect
filtering, and effect checks. It restricts the previous
implementation in two aspects:
- a psymbol p can be monomorphic (= non-generalizable) in an effect
only if p depends (= is defined via) a pvsymbol whose type contains
the affected region. See bench/programs/bad-typing/recfun.mlw
for an example. This restriction is required for soundness.
- an argument of a psymbol cannot contain a region shared with
another argument or an external pvsymbol. However, we do not
require (so far) that the argument's type doesn't contain the same
region twice and we allow the result type to contain known regions.
This restriction is not necessary for soundness, and is introduced
only to avoid some unintentional user errors and reduce the gap
between the types that can be implemented in a "let" and the types
that can be declared in a "val".
