Commit f9ff4e02 authored by Andrei Paskevich's avatar Andrei Paskevich

Expr: execute abstract blocks and whiteboxes with unfiltered effect

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.
parent 516cfd3a
use import int.Int
use import ref.Ref
exception Exit
let funny () =
exception FixRegion (ref int) in
let fixed_ref (i : int) : unit
ensures { false }
raises { FixRegion r -> !r = i }
= raise FixRegion (ref i) in
let r1 = try fixed_ref 42; absurd with FixRegion r -> r end in
try begin ensures { false }
let r2 = try fixed_ref 17; absurd with FixRegion r -> r end in
r2 := !r2 + 1;
raise Exit
end with Exit -> () end;
assert { !r1 = 18 }
use import int.Int
use import ref.Ref
let funny () =
exception FixRegion (ref int) in
let fixed_ref (i : int) : unit
ensures { false }
raises { FixRegion r -> !r = i }
= raise FixRegion (ref i) in
let r1 = try fixed_ref 42; absurd with FixRegion r -> r end in
begin
let r2 = try fixed_ref 17; absurd with FixRegion r -> r end in
r2 := !r2 + 1
end ensures { true };
assert { !r1 = 18 }
......@@ -734,7 +734,26 @@ let e_let ld e =
let e_exec c =
let cty = cty_exec (c_cty_enrich false RKnone c) in
mk_expr (Eexec (c, cty)) cty.cty_result cty.cty_mask cty.cty_effect
(* abstract blocks and white-box blocks can escape into the outer
VC context. Therefore we should assume the full effect of the
underlying expression rather than the filtered effect of c,
as produced by create_cty. However, we still want to remove
the exceptions whose post-condition is False: this is handy,
and we can handle it correctly in VC. We can safely ignore
the function-to-mapping conversions, as they cannot appear
as white-box blocks, and abstract blocks can only escape
via exceptions, which functions-as-mappings do not raise. *)
let eff = match c.c_cty.cty_args, c.c_node with
| [], Cfun e ->
let x_lost = Sxs.diff e.e_effect.eff_raises
cty.cty_effect.eff_raises in
let eff = Sxs.fold (fun xs eff ->
eff_catch eff xs) x_lost e.e_effect in
let eff = if cty.cty_effect.eff_ghost then
try_effect [e] eff_ghostify true eff else eff in
eff_union_par cty.cty_effect eff
| _ -> cty.cty_effect in
mk_expr (Eexec (c, cty)) cty.cty_result cty.cty_mask eff
let c_any c = mk_cexp Cany c
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment