The effects now must satisfy the following invariants:

1. Every region in eff_writes, eff_taints, and eff_covers
   must occur in the type of some variable in eff_reads.

2. Both eff_taints and eff_covers are subsets of eff_writes.

3. eff_covers and eff_resets are disjoint.

4. Every region in eff_writes is either in eff_covers or
   is stale (according to Ity.reg_r_stale) and forbidden
   for the later use.

Also, this commit rewrites Ity.eff_assign and Ity.eff_strong
(renamed now to eff_reset_overwritten) to handle correctly
parallel assignments.