Merge branch 'master' into new_inv

TODO.txt

 Change retag semantics! Don't prove anything about this crazy monster.
 
 Things in the "logical" side of the model that could be made better:
-- The invariant for one (sub-)resource should only talk about that resource.
-  To fix CallMapInv: replace set T by `gmap loc tag` indicating which locations are protected.
-  To fix TagMapInv: kill the "value" part of LMAP.
-  To fix LocMapInv: make it a `gmap loc tag` that all just have a singleton stack with that loc.
-  Then we can also make PrivLoc handle fairly uniformly locations that are "privatized" by being protected or by being local.
-- heaplets need to map to *pairs of* scalars: left val, right val. Remove silly equality from LmapInv.
-- lmap needs to become `gmap tag (ex (gset loc))` so that we can make local locations public and know that this does not de-privatize any other location.
-  or maybe instead just make it a different state that a tag can be in? pub, uniq, local? Seems more reasonable at this point.
-- No need for (persistently) public call IDs.  Still need to be able to pass
-  ownership of *all* tag protected by a call ID though, so
-  `gmap call_id (ex (gmap tag loc))` seems reasonable, or else `gmap call_id (prod frac (gmap tag (ex loc)))`.
 - Free and Retag should be WF!
 
 More speculative:

theories/opt/ex1.v

@@ -13,6 +13,7 @@ Definition ex1_unopt : function :=
     *{int} "x" <- #[42] ;;
     Call #[ScFnPtr "g"] [] ;;
     Copy *{int} "x"
+    (* FIXME: should deallocate `x` *)
   .
 
 Definition ex1_opt : function :=
@@ -23,6 +24,7 @@ Definition ex1_opt : function :=
     *{int} "x" <- #[42] ;;
     let: "v" := Copy *{int} "x" in
     Call #[ScFnPtr "g"] [] ;;
+    (* FIXME: should deallocate `x` *)
     "v"
   .
 

theories/sim/refl.v

@@ -27,14 +27,13 @@ Fixpoint expr_wf (e: expr) : Prop :=
   | Val v => value_wf v
   | Call f args => expr_wf f ∧ Forall id (fmap expr_wf args)
   | Case e branches => expr_wf e ∧ Forall id (fmap expr_wf branches)
-  | Deref e _ | Ref e | Copy e =>
+  | Deref e _ | Ref e | Copy e | Free e | Retag e _ =>
     expr_wf e
   | Proj e1 e2 | Conc e1 e2 | BinOp _ e1 e2 | Let _ e1 e2 | Write e1 e2 =>
     expr_wf e1 ∧ expr_wf e2
   (* Forbidden cases. *)
   | InitCall e | EndCall e => False (* administrative *)
   | Place _ _ _ => False (* literal pointers *)
-  | Free _ | Retag _ _ => False (* TODO: We'd like to support deallocation and retag! *)
   end.
 Definition prog_wf (prog: fn_env) :=
   has_main prog ∧
@@ -286,8 +285,8 @@ Proof using Type*.
     split; first done.
     simpl. split; last done. constructor; last done.
     eapply arel_mono, arel_ptr; auto.
-  - (* Free: can't happen *) done.
-  - (* Retag: can't happen *) done.
+  - (* Free *) admit.
+  - (* Retag *) admit.
   - (* Let *)
     move=>[Hwf1 Hwf2] xs Hxs /=. sim_bind (subst_map _ e1) (subst_map _ e1).
     eapply sim_simple_frame_core.