Laurel: avoid quantified modifies frames when using array theory

[julesmt]

Under --use-array-theory, a modifies clause naming only individual object
references is now encoded as a single quantifier-free heap equation instead of
a ∀-quantified frame, so the solver discharges it by array rewriting instead of
instantiating a quantifier per object/field.

∀ obj, fld. obj ≠ c ⇒ readField(old,obj,fld) == readField(new,obj,fld)   -- before
data(new) == store(data(old), c, select(data(new), c))                   -- now

The ∀ frame is unchanged for set-valued/empty modifies and when array theory is
off, so default behavior is untouched.

[keyboardDrummer]

I found the term "array-theory" in this PR misleading because the PR does not directly use any SMT array theory. Instead, the PR relies on Core Map's which are not necessarily implemented using SMT array theory. In fact, I think Core is or at least was not using array theory for their maps, simply because it is or was not implemented yet.

[keyboardDrummer]

Very cool!

[keyboardDrummer]

@keyboardDrummer-bot please resolve merge conflicts

[keyboardDrummer]

How come you can't make the enumerated encoding work with procedures that have a body? Suppose I have:

composite C { var x: int }
procedure creator() returns (c: C)
  ensures c#x == 3
  ensures fresh(c)
  modifies {}
  opaque
{
  c := new C;
  c#x := 3;
}

then that would translate to something like:

procedure creator() returns (c: C)
// c#x == 3
  ensures read($heap, c, C.x) == 3 
  
// fresh(c)
  ensures c.ref >= old($heap).nextRef

// modifies {}, enumerated encoding
  ensures $heap.data == old($heap).data 

// implicit postcondition stating that every output object is allocated in the new heap
  ensures c.ref < $heap.nextRef

which has the curious implication that read(old($heap), c, C.x) == 3, so the old heap contains data for an object that did not yet exist at the time of the old heap. However, I think that might not cause any issues. What issues did you run into?

[julesmt]

Yeah, I had pretty much the same example.
data == old data fails because the body writes the fresh row, even though fresh objects shouldn't count for modifies.

The pointwise frame dodges this with the obj < nextReference($heap_in) guard, which I can't keep without a quantifier, so I this is why I wanted to restrict the enumerated frame to bodiless procedures.

However to get it for bodies too, I split the jobs: callers assume the enumerated frame, and the body is checked separately by asserting the pointwise frame at every exit.

what do you think (see next commit) ? @keyboardDrummer

[keyboardDrummer]

However to get it for bodies too, I split the jobs: callers assume the enumerated frame, and the body is checked separately by asserting the pointwise frame at every exit.
what do you think (see next commit) ? @keyboardDrummer

Brilliant!

[keyboardDrummer]

Please remove the default values in the private methods. I think the only default should be in LaurelTranslateOptions

[julesmt]

Oh yeah sorry, I thought I had modified that, will do

[keyboardDrummer]

This will have a few merge conflicts after #1352 merges. I'll try to resolve these before you get to it @julesmt