Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Undo revert 966 and add fixes #968

Merged
merged 4 commits into from
Oct 22, 2024
Merged

Undo revert 966 and add fixes #968

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
f01b081
Revert "Revert isolation (#966)"
keyboardDrummer Oct 18, 2024
160b0f7
Fix problems with isolate each assertion and isolating jumps
keyboardDrummer Oct 18, 2024
f27d1eb
Update expect file
keyboardDrummer Oct 18, 2024
4cbed7f
Refactoring to make code more robust
keyboardDrummer Oct 21, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 4 additions & 2 deletions Source/Concurrency/CivlUtil.cs
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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
Loading