Skip to content

Commit

Permalink
Undo revert 966 and add fixes (#968)
Browse files Browse the repository at this point in the history 
### Changes
- Undo revert #966, which was
reverted because it caused unintended Dafny changes
- Change the isolation of returns, so that each ensures clause gets its
own VC when `{:vcs_split_on_every_assert}` is used, so we get #returns *
#ensures additional VCs from return statements.
- Change the isolation of returns, so that only explicit return
statement are given their own VC branch

### Testing
- Added a CLI test that tests the above two changes
- I have checked that updating Dafny to this latest Boogie version only
causes expected failures in Dafny tests that can easily be repaired.
  • Loading branch information
@keyboardDrummer
keyboardDrummer authored Oct 22, 2024
1 parent 09093a2 commit 7ea138f
Show file tree
Hide file tree
Showing 107 changed files with 3,589 additions and 2,575 deletions.
6 changes: 4 additions & 2 deletions Source/Concurrency/CivlUtil.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -307,14 +307,16 @@ public static HavocCmd HavocCmd(params IdentifierExpr[] vars)

public static class BlockHelper
{
public static readonly IToken /*!*/ ReportedNoToken = new Token();

public static Block Block(string label, List<Cmd> cmds)
{
return new Block(Token.NoToken, label, cmds, CmdHelper.ReturnCmd);
return new Block(ReportedNoToken, label, cmds, CmdHelper.ReturnCmd);
}

public static Block Block(string label, List<Cmd> cmds, List<Block> gotoTargets)
{
return new Block(Token.NoToken, label, cmds, new GotoCmd(Token.NoToken, gotoTargets));
return new Block(ReportedNoToken, label, cmds, new GotoCmd(Token.NoToken, gotoTargets));
}
}

Expand Down
12 changes: 6 additions & 6 deletions Source/Core/AST/Absy.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1300,7 +1300,7 @@ public override void Resolve(ResolutionContext rc)

public void ResolveWhere(ResolutionContext rc)
{
if (QKeyValue.FindBoolAttribute(Attributes, "assumption") && this.TypedIdent.WhereExpr != null)
if (Attributes.FindBoolAttribute("assumption") && this.TypedIdent.WhereExpr != null)
{
rc.Error(tok, "assumption variable may not be declared with a where clause");
}
Expand All @@ -1315,7 +1315,7 @@ public override void Typecheck(TypecheckingContext tc)
{
(this as ICarriesAttributes).TypecheckAttributes(tc);
this.TypedIdent.Typecheck(tc);
if (QKeyValue.FindBoolAttribute(Attributes, "assumption") && !this.TypedIdent.Type.IsBool)
if (Attributes.FindBoolAttribute("assumption") && !this.TypedIdent.Type.IsBool)
{
tc.Error(tok, "assumption variable must be of type 'bool'");
}
Expand Down Expand Up @@ -2059,7 +2059,7 @@ public override void Emit(TokenTextWriter stream, int level)

stream.Write(this, level, (AlwaysRevealed ? "revealed " : "") + "function ");
EmitAttributes(stream);
if (Body != null && !QKeyValue.FindBoolAttribute(Attributes, "inline"))
if (Body != null && !Attributes.FindBoolAttribute("inline"))
{
Contract.Assert(DefinitionBody == null);
// Boogie inlines any function whose .Body field is non-null. The parser populates the .Body field
Expand All @@ -2069,7 +2069,7 @@ public override void Emit(TokenTextWriter stream, int level)
stream.Write("{:inline} ");
}

if (DefinitionBody != null && !QKeyValue.FindBoolAttribute(Attributes, "define"))
if (DefinitionBody != null && !Attributes.FindBoolAttribute("define"))
{
// Boogie defines any function whose .DefinitionBody field is non-null. The parser populates the .DefinitionBody field
// if the :define attribute is present, but if someone creates the Boogie file directly as an AST, then
Expand Down Expand Up @@ -2350,7 +2350,7 @@ public String ErrorMessage

public bool CanAlwaysAssume()
{
return Free && QKeyValue.FindBoolAttribute(Attributes, "always_assume");
return Free && Attributes.FindBoolAttribute("always_assume");
}


Expand Down Expand Up @@ -2490,7 +2490,7 @@ public String ErrorMessage

public bool CanAlwaysAssume ()
{
return Free && QKeyValue.FindBoolAttribute(this.Attributes, "always_assume");
return Free && this.Attributes.FindBoolAttribute("always_assume");
}

public Ensures(IToken token, bool free, Expr condition, string comment, QKeyValue kv)
Expand Down
274 changes: 0 additions & 274 deletions Source/Core/AST/AbsyQuant.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -330,280 +330,6 @@ protected List<TypeVariable> GetUnmentionedTypeParameters()
}
}

public class QKeyValue : Absy
{
public readonly string /*!*/
Key;

private readonly List<object /*!*/> /*!*/
_params; // each element is either a string or an Expr

public void AddParam(object p)
{
Contract.Requires(p != null);
this._params.Add(p);
}

public void AddParams(IEnumerable<object> ps)
{
Contract.Requires(cce.NonNullElements(ps));
this._params.AddRange(ps);
}

public void ClearParams()
{
this._params.Clear();
}

public IList<object> Params
{
get
{
Contract.Ensures(cce.NonNullElements(Contract.Result<IList<object>>()));
Contract.Ensures(Contract.Result<IList<object>>().IsReadOnly);
return this._params.AsReadOnly();
}
}

public QKeyValue Next;

[ContractInvariantMethod]
void ObjectInvariant()
{
Contract.Invariant(Key != null);
Contract.Invariant(cce.NonNullElements(this._params));
}

public QKeyValue(IToken tok, string key, IList<object /*!*/> /*!*/ parameters, QKeyValue next)
: base(tok)
{
Contract.Requires(key != null);
Contract.Requires(tok != null);
Contract.Requires(cce.NonNullElements(parameters));
Key = key;
this._params = new List<object>(parameters);
Next = next;
}

public void Emit(TokenTextWriter stream)
{
Contract.Requires(stream != null);
stream.Write("{:");
stream.Write(Key);
string sep = " ";
foreach (object p in Params)
{
stream.Write(sep);
sep = ", ";
if (p is string)
{
stream.Write("\"");
stream.Write((string) p);
stream.Write("\"");
}
else
{
((Expr) p).Emit(stream);
}
}

stream.Write("}");
}

public override void Resolve(ResolutionContext rc)
{
//Contract.Requires(rc != null);

if ((Key == "minimize" || Key == "maximize") && Params.Count != 1)
{
rc.Error(this, "attributes :minimize and :maximize accept only one argument");
}

if (Key == "verified_under" && Params.Count != 1)
{
rc.Error(this, "attribute :verified_under accepts only one argument");
}

if (Key == CivlAttributes.LAYER)
{
foreach (var o in Params)
{
if (o is LiteralExpr l && l.isBigNum)
{
var n = l.asBigNum;
if (n.IsNegative)
{
rc.Error(this, "layer must be non-negative");
}
else if (!n.InInt32)
{
rc.Error(this, "layer is too large (max value is Int32.MaxValue)");
}
}
else
{
rc.Error(this, "layer must be a non-negative integer");
}
}
}

foreach (object p in Params)
{
if (p is Expr)
{
var oldCtxtState = rc.StateMode;
if (oldCtxtState == ResolutionContext.State.Single)
{
rc.StateMode = ResolutionContext.State.Two;
}

((Expr) p).Resolve(rc);
if (oldCtxtState != rc.StateMode)
{
rc.StateMode = oldCtxtState;
}
}
}
}

public override void Typecheck(TypecheckingContext tc)
{
//Contract.Requires(tc != null);
foreach (object p in Params)
{
var expr = p as Expr;
if (expr != null)
{
expr.Typecheck(tc);
}

if ((Key == "minimize" || Key == "maximize")
&& (expr == null || !(expr.Type.IsInt || expr.Type.IsReal || expr.Type.IsBv)))
{
tc.Error(this, "attributes :minimize and :maximize accept only one argument of type int, real or bv");
break;
}

if (Key == "verified_under" && (expr == null || !expr.Type.IsBool))
{
tc.Error(this, "attribute :verified_under accepts only one argument of type bool");
break;
}
}
}

public void AddLast(QKeyValue other)
{
Contract.Requires(other != null);
QKeyValue current = this;
while (current.Next != null)
{
current = current.Next;
}

current.Next = other;
}

public static QKeyValue FindAttribute(QKeyValue kv, Func<QKeyValue, bool> property)
{
for (; kv != null; kv = kv.Next)
{
if (property(kv))
{
return kv;
}
}
return null;
}

// Look for {:name string} in list of attributes.
[Pure]
public static string FindStringAttribute(QKeyValue kv, string name)
{
Contract.Requires(name != null);
kv = FindAttribute(kv, qkv => qkv.Key == name && qkv.Params.Count == 1 && qkv.Params[0] is string);
if (kv != null)
{
Contract.Assert(kv.Params.Count == 1 && kv.Params[0] is string);
return (string) kv.Params[0];
}
return null;
}

// Look for {:name expr} in list of attributes.
public static Expr FindExprAttribute(QKeyValue kv, string name)
{
Contract.Requires(name != null);
kv = FindAttribute(kv, qkv => qkv.Key == name && qkv.Params.Count == 1 && qkv.Params[0] is Expr);
if (kv != null)
{
Contract.Assert(kv.Params.Count == 1 && kv.Params[0] is Expr);
return (Expr) kv.Params[0];
}
return null;
}

// Return 'true' if {:name true} or {:name} is an attribute in 'kv'
public static bool FindBoolAttribute(QKeyValue kv, string name)
{
Contract.Requires(name != null);
kv = FindAttribute(kv, qkv => qkv.Key == name && (qkv.Params.Count == 0 ||
(qkv.Params.Count == 1 && qkv.Params[0] is LiteralExpr &&
((LiteralExpr) qkv.Params[0]).IsTrue)));
return kv != null;
}

public static int FindIntAttribute(QKeyValue kv, string name, int defl)
{
Contract.Requires(name != null);
Expr e = FindExprAttribute(kv, name);
LiteralExpr l = e as LiteralExpr;
if (l != null && l.isBigNum)
{
return l.asBigNum.ToIntSafe;
}

return defl;
}

public override Absy Clone()
{
List<object> newParams = new List<object>();
foreach (object o in Params)
{
newParams.Add(o);
}

return new QKeyValue(tok, Key, newParams, (Next == null) ? null : (QKeyValue) Next.Clone());
}

public override Absy StdDispatch(StandardVisitor visitor)
{
return visitor.VisitQKeyValue(this);
}

public override bool Equals(object obj)
{
var other = obj as QKeyValue;
if (other == null)
{
return false;
}
else
{
return Key == other.Key && object.Equals(Params, other.Params) &&
(Next == null
? other.Next == null
: object.Equals(Next, other.Next));
}
}

public override int GetHashCode()
{
throw new NotImplementedException();
}
}

public class Trigger : Absy
{
public readonly bool Pos;
Expand Down
Loading

0 comments on commit 7ea138f

Please sign in to comment.