Unify unit variables in heapster

[jpaykin]

Trying to unify all unit-typed heapster variables.

We want to be able to introduce unit-typed phantom variables with opaque permissions, which can be used at the type level to indicate permission to do something even if there is no corresponding variable.

For example (from the worf project): we will define an opaque permission watchdog_perm and then axiomatize the following types, even though the functions take no arguments (as they work by sending messages to an external server).

/* int watchdog_task_start(); */
heapster_assume_fun_rename_prim env
    "watchdog_task_start"
    "watchdog_task_start"
    "(u:unit). empty -o u:watchdog_perm<>";

/* int watchdog_reset(); */
heapster_assume_fun_rename_prim env
    "watchdog_reset"
    "watchdog_reset"
    "(u:unit). u:watchdog_perm<> -o u:watchdog_perm<>, ret:int32<>";

/* int watchdog_cancel(); */
heapster_assume_fun_rename_prim env
    "watchdog_cancel"
    "watchdog_cancel"
    "(u:unit). u:watchdog_perm<> -o ret:int32<>";

This PR goes about this in several parts:

1. [bf73229] Modifying the state monad ImplM in Implication.hs to track the first unit-typed variable we come across, and [9780c93] modifying implSetNameType to correctly add permissions equating new unit-typed variables with this global type.
2. [9780c93] Similarly for the PermCheckM monad in TypedCrucible.hs with the corresponding function setVarType.
3. [9780c93] Add a new typing rule to equate all variables of unit type.
4. [9780c93] There may be some times at which the code assumes variables have only trivial permissions, whereas some, will now have equality permissions. This will manifest as an error from popping the stack, and the solution is to replace that call to pop with a call to recombine_perm.
5. [186d12f] Instaniate unit-typed evars with the global evar.
6. [68be84f] Add a test case to heapster-saw/examples.

[jpaykin]

Regarding (5): Eddy says:

there are a few places where you could do that. One possibility is that you instantiate unit-typed evars when you create the evars, which happens in runImplM and friends as well as withExtVarsM. Another possibility is that you do it when you have a proof goal of the form u:p for evar u, which would require you to change proveExVarImpl as well as isProvablePerm (the comments on the latter mention the former)

[jpaykin]

Experiencing a bug in recombinePerm when typechecking the commit function in tasha_update.saw:

tcEmitLLVMStmt: memclear of pointer
Emit statement
Calling handleUnitVars from TypedCrucible
handleUnitVar: u1
about to call unitEqM: u1 : eq( top_u )
done with unitEqM: u1
done with handleUnitVar: u1
recombinePerm u1 eq(top_u) <- eq(())
recombinePerm u1 true <- eq(top_u)
recombinePerm top_u watchdog_perm<> <- eq(())
recombinePerm: unexpected equality permission being recombined
top_u : watchdog_perm<> <- eq(())
[23:56:02.925] recombinePerm: unexpected equality permission being recombined
CallStack (from HasCallStack):
  error, called at src/Verifier/SAW/Heapster/Implication.hs:5252:3 in heapster-saw-0.1-inplace:Verifier.SAW.Heapster.Implication
  recombinePerm', called at src/Verifier/SAW/Heapster/Implication.hs:5214:3 in heapster-saw-0.1-inplace:Verifier.SAW.Heapster.Implication
  recombinePermExpl, called at src/Verifier/SAW/Heapster/Implication.hs:5233:47 in heapster-saw-0.1-inplace:Verifier.SAW.Heapster.Implication
  recombinePerm', called at src/Verifier/SAW/Heapster/Implication.hs:5214:3 in heapster-saw-0.1-inplace:Verifier.SAW.Heapster.Implication
  recombinePermExpl, called at src/Verifier/SAW/Heapster/Implication.hs:5198:44 in heapster-saw-0.1-inplace:Verifier.SAW.Heapster.Implication
  recombinePerm, called at src/Verifier/SAW/Heapster/Implication.hs:5362:3 in heapster-saw-0.1-inplace:Verifier.SAW.Heapster.Implication
  recombinePerms, called at src/Verifier/SAW/Heapster/TypedCrucible.hs:2447:44 in heapster-saw-0.1-inplace:Verifier.SAW.Heapster.TypedCrucible
  stmtRecombinePerms, called at src/Verifier/SAW/Heapster/TypedCrucible.hs:3402:3 in heapster-saw-0.1-inplace:Verifier.SAW.Heapster.TypedCrucible
make: *** [make/llvm.mk:107: heapster/tasha_update_gen.v] Error 2

This is stemming from a call to recombinePerm where top_u has permission watchdog_perm<>, but we have separately added a type eq(()), which is not handled by recombinePerm.

This is in turn stemming from an instance of tcEmitLLMVStmt on an LLVM_MemClear statement. The documentation on this case says "Type-check a clear instruction by getting the list of field permissions returned by 'llvmFieldsOfSize' and storing word 0 to each of them". In particular, we are able to successfully prove each field perm and write 0 to it (which involves calling recombinePerm on every field, but then we aim to return a fresh unit variable. It is this call to emitStmt and stmtRecombinePerms which adds the offending constraint u1:eq(()) when u1 already has eq(top_u), which leads to the error.

We are probably in trouble if we don't allow any unit variables to have the permission u:eq(()). Would this be improved if the global unit variable top_u did not have nontrivial permissions, e.g. if there was always a fresh variable that sat in that role?

@eddywestbrook thoughts?

[eddywestbrook]

Good job tracking that down! Yes, I see that assignment of a unit value to a fresh unit variable in the translation of LLVM_MemClear.

The issue with allowing unit variables to have permissions like eq(()) is that there is no well-defined way to combine such a permission with one of these new specification-y unit permissions you are trying to add.

One idea is to add a special case to recombinePerm to just drop any eq(()) permissions when they are being recombined...? What do you think?

[jpaykin]

One idea is to add a special case to recombinePerm to just drop any eq(()) permissions when they are being recombined...? What do you think?

Is that actually sound? Is it better to add that special case to recombinePerm or just not add the eq(()) permissions in the first place? It's not clear to me why tcEmitLLMVStmt does that in the first place, especially if we're just going to drop it.

[eddywestbrook]

Please address the small revisions I suggested in my comments. These are mostly about removing extra tracing statements that are not necessary in the debug output.

Otherwise, this is great, thanks for your hard work!