Conversation
keyboardDrummer
changed the title
ssomayyajula
left a comment
ssomayyajula
left a comment
There was a problem hiding this comment.
No objection to the heap encoding itself nor how modifies/ensures clauses are transformed, leaving coding style etc. choices to @joscoh. Two questions:
- Surprised that heap-parameterized procedures aren't their own data type that are
Coercion-able to ordinary procedures, since e.g. one may forget to checkhasHeapOutduring processing and the type system won't save you. OK surprised isn't the right word, just curious if it would be a burden to make the distinction. - When a procedure has a
$heap_outand no modifies clause, do you need that condition because the corresponding Core procedure will mark$heap_outas modified?
Why? The PR needs two reviewers, one of which should be done by a code owner but the other can be done by you. If you approve the PR, could you approve it?
How would a separate datatype prevent you from forgetting to transform the modifies clause?
Then we don't need the condition. The condition is needed when there are modified clauses so we don't generate a clause that refers to a non-existent |
MikaelMayer
left a comment
MikaelMayer
left a comment
There was a problem hiding this comment.
Minor questions and updates but otherwise looks good!
| assert x == y; | ||
| // ^^^^^^^^^^^^^^ error: assertion does not hold |
There was a problem hiding this comment.
| assert x == y; | |
| // ^^^^^^^^^^^^^^ error: assertion does not hold | |
| assert x == y; | |
| //^^^^^^^^^^^^^^ error: assertion does not hold |
Maybe?
| // 3 | ||
| // } | ||
|
|
||
| // procedure caller() { |
There was a problem hiding this comment.
What's the plan to uncomment these procedures?
| procedure multipleModifiesClausesCaller() { | ||
| var c: Container := new Container; | ||
| var d: Container := new Container; | ||
| var e: Container := new Container; |
There was a problem hiding this comment.
Nice, would you be able to add assertions that c != d && d != e && e != c ?
| let freshVar ← freshVarName | ||
| let getCounter := mkMd (.StaticCall "Heap..counter" [mkMd (.Identifier heapVar)]) | ||
| let saveCounter := mkMd (.LocalVariable freshVar ⟨.TInt, #[]⟩ (some getCounter)) | ||
| let newCounter := mkMd (.PrimitiveOp .Add [mkMd (.StaticCall "Heap..counter" [mkMd (.Identifier heapVar)]), mkMd (.LiteralInt 1)]) |
There was a problem hiding this comment.
What about creating a prelude function that increases only the counter of the heap and calling it here?
I think it might be useful down the road if you ever need to trigger and assert "this heap is newer than this other one" so that you guarantee that counter increases
| | none => | ||
| ctx.addSort { name := id, arity := args.length } | ||
| let ctx := ctx.addSort { name := id, arity := args.length } | ||
| args.foldl (fun (ctx : SMT.Context) arg => |
There was a problem hiding this comment.
I'm not sure I understood everything but I remember it was mentioned in the PR description. Could you please point me where this change is tested?
| notModified($obj) ==> readField($heap_in, $obj, fld) == readField($heap_out, $obj, fld) | ||
| Generates: | ||
| forall $obj: Composite, $fld: Field => | ||
| $obj < $heap_in.counter && notModified($obj) ==> readField($heap_in, $obj, $fld) == readField($heap_out, $obj, $fld) |
There was a problem hiding this comment.
Interesting ! That seems right to me. The counter is the next available reference, correct?
4 participants
Changes
Testing
T1_MutableFields. Checking that two created objects are not equal.T2_ModifiesClauses. Checking that newly allocated objects can be modified without being in the modifies clause.