Implement verification coverage analysis #741
There are no files selected for viewing
| Original file line number | Diff line number | Diff line change |
|---|---|---|
|
|
@@ -3723,6 +3723,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options) | |
| Dictionary<Variable, Expr> substMapBound = new Dictionary<Variable, Expr>(); | ||
| List<Variable> /*!*/ | ||
| tempVars = new List<Variable>(); | ||
| string callId = (this as ICarriesAttributes).FindStringAttribute("id"); | ||
|
|
||
| // proc P(ins) returns (outs) | ||
| // requires Pre | ||
|
|
@@ -3841,6 +3842,7 @@ protected override Cmd ComputeDesugaring(PrintOptions options) | |
| AssertCmd /*!*/ | ||
| a = new AssertRequiresCmd(this, reqCopy); | ||
| Contract.Assert(a != null); | ||
|
|
||
| if (Attributes != null) | ||
| { | ||
| // Inherit attributes of call. | ||
|
|
@@ -3849,6 +3851,11 @@ protected override Cmd ComputeDesugaring(PrintOptions options) | |
| a.Attributes = attrCopy; | ||
| } | ||
|
|
||
| // Do this after copying the attributes so it doesn't get overwritten | ||
|
There was a problem hiding this comment. The method being changed is very large, and uses regions instead of submethods to organize code. I want to ask you apply the boyscout principle of "leaving things behind nicer than they were", and to chop this method up into pieces, and also to move the class There was a problem hiding this comment. Created #743 to track this, as I think we need to do it very carefully. There was a problem hiding this comment.
Why? Splitting a method up into pieces can be done in a mostly automated way using Rider. Same for moving a class into a separate file. There was a problem hiding this comment. Yeah, but reorganizing those methods so that they are well-organized and use better abstractions, rather than just slicing them into pieces, would require more thought. There was a problem hiding this comment. I'm paraphrasing an offline discussion I had with @atomb on the above, for the sake of getting some additional eyes on it. @atomb prefers keeping the pacify implementations for various commands in a single method, since that allows having them be vertically adjacent to each other which follows the structure of Figure 3 in this paper, which is what the code is based on. Keeping the structure of the two most similar provides the best way of doing a side-by-side comparison. I would prefer keeping the code for different commands separate. I would even prefer having an abstract I believe that while the paper is structured by putting the concepts at the top-level, and then discussing all commands within each concept, this doesn't mean that's also the right structure for the code. It's easier to discuss just one pair of concept and command at a time, and while the paper doesn't have room to go that slow, in our codebase we can use as many separators, such as files and methods, as we like. Also, the code is more verbose so there is more need to keep the scope of each block to a minimum. I don't think optimizing for comparability between the code and the paper is important. Modern IDEs make it easy to navigate between the code for various commands, so I don't think there's a particular difficulty in making the comparison in any case. |
||
| if (callId is not null) { | ||
| (a as ICarriesAttributes).CopyIdWithSuffixFrom(tok, req, $"${callId}$requires"); | ||
| } | ||
|
|
||
| a.ErrorDataEnhanced = reqCopy.ErrorDataEnhanced; | ||
| newBlockBody.Add(a); | ||
| } | ||
|
|
@@ -3860,6 +3867,11 @@ protected override Cmd ComputeDesugaring(PrintOptions options) | |
| AssumeCmd /*!*/ | ||
| a = new AssumeCmd(req.tok, Substituter.Apply(s, req.Condition)); | ||
| Contract.Assert(a != null); | ||
| // These probably won't have IDs, but copy if they do. | ||
| if (callId is not null) { | ||
| (a as ICarriesAttributes).CopyIdWithSuffixFrom(tok, req, $"${callId}$requires_assumed"); | ||
| } | ||
|
|
||
| newBlockBody.Add(a); | ||
| } | ||
| } | ||
|
|
@@ -4022,6 +4034,10 @@ protected override Cmd ComputeDesugaring(PrintOptions options) | |
|
|
||
| #endregion | ||
|
|
||
| if (callId is not null) { | ||
| (assume as ICarriesAttributes).CopyIdWithSuffixFrom(tok, e, $"${callId}$ensures"); | ||
| } | ||
|
|
||
| newBlockBody.Add(assume); | ||
| } | ||
|
|
||
|
|
@@ -4039,6 +4055,9 @@ protected override Cmd ComputeDesugaring(PrintOptions options) | |
| cout_exp = new IdentifierExpr(cce.NonNull(couts[i]).tok, cce.NonNull(couts[i])); | ||
| Contract.Assert(cout_exp != null); | ||
| AssignCmd assign = Cmd.SimpleAssign(param_i.tok, cce.NonNull(this.Outs[i]), cout_exp); | ||
| if (callId is not null) { | ||
| Attributes = new QKeyValue(param_i.tok, "id", new List<object>(){ $"{callId}$out{i}" }, Attributes); | ||
| } | ||
| newBlockBody.Add(assign); | ||
| } | ||
| } | ||
|
|
||
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
If you define these methods as extension methods, then you can also call them without casting to
ICarriesAttributesfirst.