From 9ae2a77cb73b5361adb8f63b61942c2e2d8a98b3 Mon Sep 17 00:00:00 2001
From: Bernhard Kragl <bernhard.kragl@gmail.com>
Date: Mon, 2 Mar 2020 18:57:10 +0100
Subject: [PATCH] Add support to inject lemmas into commutativity checks (#211)
---
Source/Concurrency/CivlTypeChecker.cs | 32 +--
Source/Concurrency/CommutativityHints.cs | 259 ++++++++++++++++++
Source/Concurrency/Concurrency.csproj | 2 +-
Source/Concurrency/MoverCheck.cs | 7 +-
.../TransitionRelationComputation.cs | 20 +-
Source/Concurrency/Witnesses.cs | 156 -----------
Source/Core/CivlAttributes.cs | 5 +-
Test/civl/async/2pc-triggers.bpl | 15 +-
Test/civl/async/2pc.bpl | 15 +-
Test/civl/commutativity-lemma.bpl | 23 ++
Test/civl/commutativity-lemma.bpl.expect | 2 +
Test/civl/verified-ft.bpl | 25 +-
12 files changed, 346 insertions(+), 215 deletions(-)
create mode 100644 Source/Concurrency/CommutativityHints.cs
delete mode 100644 Source/Concurrency/Witnesses.cs
create mode 100644 Test/civl/commutativity-lemma.bpl
create mode 100644 Test/civl/commutativity-lemma.bpl.expect
diff --git a/Source/Concurrency/CivlTypeChecker.cs b/Source/Concurrency/CivlTypeChecker.cs
index afec56fd6..e8afd2333 100644
--- a/Source/Concurrency/CivlTypeChecker.cs
+++ b/Source/Concurrency/CivlTypeChecker.cs
@@ -24,8 +24,7 @@ public class CivlTypeChecker
public Dictionary<Procedure, AtomicAction> procToIsAbstraction;
public Dictionary<Procedure, YieldingProc> procToYieldingProc;
public Dictionary<Procedure, IntroductionProc> procToIntroductionProc;
- public Dictionary<Tuple<AtomicAction, AtomicAction>,
- List<WitnessFunction>> atomicActionPairToWitnessFunctions;
+ public CommutativityHints commutativityHints;
public List<InductiveSequentialization> inductiveSequentializations;
@@ -55,8 +54,6 @@ public CivlTypeChecker(Program program)
this.procToYieldingProc = new Dictionary<Procedure, YieldingProc>();
this.procToIntroductionProc = new Dictionary<Procedure, IntroductionProc>();
this.implToPendingAsyncCollector = new Dictionary<Implementation, Variable>();
- this.atomicActionPairToWitnessFunctions = new Dictionary<Tuple<AtomicAction, AtomicAction>,
- List<WitnessFunction>>();
this.inductiveSequentializations = new List<InductiveSequentialization>();
}
@@ -91,7 +88,7 @@ public void TypeCheck()
TypeCheckRefinementLayers();
- TypeCheckWitnessFunctions();
+ TypeCheckCommutativityHints();
AttributeEraser.Erase(this);
}
@@ -129,21 +126,11 @@ private void TypeCheckRefinementLayers()
}
- private void TypeCheckWitnessFunctions()
+ private void TypeCheckCommutativityHints()
{
- WitnessFunctionVisitor wfv = new WitnessFunctionVisitor(this);
- wfv.VisitFunctions();
- foreach (var witnessFunction in wfv.allWitnessFunctions)
- {
- var key = Tuple.Create(
- witnessFunction.firstAction,
- witnessFunction.secondAction);
- if (!atomicActionPairToWitnessFunctions.ContainsKey(key))
- {
- atomicActionPairToWitnessFunctions[key] = new List<WitnessFunction>();
- }
- atomicActionPairToWitnessFunctions[key].Add(witnessFunction);
- }
+ CommutativityHintVisitor visitor = new CommutativityHintVisitor(this);
+ visitor.VisitFunctions();
+ this.commutativityHints = visitor.commutativityHints;
}
private void TypeCheckGlobalVariables()
@@ -893,6 +880,13 @@ public AtomicAction FindIsAbstraction(string name)
return procToIsAbstraction.Values.FirstOrDefault(a => a.proc.Name == name);
}
+ public AtomicAction FindAtomicActionOrAbstraction(string name)
+ {
+ var action = FindAtomicAction(name);
+ if (action != null) return action;
+ return FindIsAbstraction(name);
+ }
+
public IEnumerable<AtomicAction> AllActions =>
procToAtomicAction.Union(procToIsInvariant).Union(procToIsAbstraction)
.Select(x => x.Value);
diff --git a/Source/Concurrency/CommutativityHints.cs b/Source/Concurrency/CommutativityHints.cs
new file mode 100644
index 000000000..f5ca4cb88
--- /dev/null
+++ b/Source/Concurrency/CommutativityHints.cs
@@ -0,0 +1,259 @@
+using System;
+using System.Collections.Generic;
+using System.Diagnostics;
+using System.Linq;
+
+namespace Microsoft.Boogie
+{
+ public class CommutativityHint
+ {
+ public readonly Function function;
+ public readonly AtomicAction firstAction;
+ public readonly AtomicAction secondAction;
+ public List<Expr> args;
+
+ public CommutativityHint(Function function,
+ AtomicAction firstAction, AtomicAction secondAction, List<Expr> args)
+ {
+ this.function = function;
+ this.firstAction = firstAction;
+ this.secondAction = secondAction;
+ this.args = args;
+ }
+ }
+
+ public class CommutativityWitness : CommutativityHint
+ {
+ public readonly Variable witnessedVariable;
+
+ public CommutativityWitness(Function function, Variable witnessedVariable,
+ AtomicAction firstAction, AtomicAction secondAction, List<Expr> args)
+ : base(function, firstAction, secondAction, args)
+ {
+ this.witnessedVariable = witnessedVariable;
+ }
+
+ public CommutativityWitness(Variable witnessedVariable, CommutativityHint h)
+ : this(h.function, witnessedVariable, h.firstAction, h.secondAction, h.args) {}
+ }
+
+ public class CommutativityHints
+ {
+ private Dictionary<Tuple<AtomicAction, AtomicAction>, List<CommutativityWitness>> witnesses;
+ private Dictionary<Tuple<AtomicAction, AtomicAction>, List<CommutativityHint>> lemmas;
+
+ public CommutativityHints()
+ {
+ witnesses = new Dictionary<Tuple<AtomicAction, AtomicAction>, List<CommutativityWitness>>();
+ lemmas = new Dictionary<Tuple<AtomicAction, AtomicAction>, List<CommutativityHint>>();
+ }
+
+ private Tuple<AtomicAction, AtomicAction> Key(AtomicAction first, AtomicAction second)
+ {
+ return Tuple.Create(first, second);
+ }
+
+ public void AddWitness(CommutativityWitness witness)
+ {
+ var key = Key(witness.firstAction, witness.secondAction);
+ if (!witnesses.ContainsKey(key))
+ {
+ witnesses[key] = new List<CommutativityWitness>();
+ }
+ witnesses[key].Add(witness);
+ }
+
+ public void AddLemma(CommutativityHint lemma)
+ {
+ var key = Key(lemma.firstAction, lemma.secondAction);
+ if (!lemmas.ContainsKey(key))
+ {
+ lemmas[key] = new List<CommutativityHint>();
+ }
+ lemmas[key].Add(lemma);
+ }
+
+ public IEnumerable<CommutativityWitness> GetWitnesses(AtomicAction first, AtomicAction second)
+ {
+ witnesses.TryGetValue(Key(first, second), out List<CommutativityWitness> list);
+ if (list == null) return Enumerable.Empty<CommutativityWitness>();
+ return list;
+ }
+
+ public IEnumerable<CommutativityHint> GetLemmas(AtomicAction first, AtomicAction second)
+ {
+ lemmas.TryGetValue(Key(first, second), out List<CommutativityHint> list);
+ if (list == null) return Enumerable.Empty<CommutativityHint>();
+ return list;
+ }
+ }
+
+ class CommutativityHintVisitor
+ {
+ private const string FirstProcInputPrefix = "first_";
+ private const string SecondProcInputPrefix = "second_";
+ private const string PostStateSuffix = "'";
+
+ private readonly CivlTypeChecker ctc;
+ public CommutativityHints commutativityHints;
+
+ private AtomicAction firstAction;
+ private AtomicAction secondAction;
+ private List<Expr> args;
+
+ public CommutativityHintVisitor(CivlTypeChecker ctc)
+ {
+ this.ctc = ctc;
+ commutativityHints = new CommutativityHints();
+ }
+
+ public void VisitFunctions()
+ {
+ foreach (var f in ctc.program.Functions)
+ {
+ VisitFunction(f);
+ }
+ }
+
+ private void VisitFunction(Function function)
+ {
+ Debug.Assert(function.OutParams.Count == 1);
+ List<CommutativityHint> hints = new List<CommutativityHint>();
+ // First we collect all {:commutativity "first_action", "second_action"} attributes
+ for (QKeyValue kv = function.Attributes; kv != null; kv = kv.Next)
+ {
+ if (kv.Key != CivlAttributes.COMMUTATIVITY)
+ continue;
+ if (kv.Params.Count == 2 &&
+ kv.Params[0] is string firstActionName &&
+ kv.Params[1] is string secondActionName)
+ {
+ firstAction = ctc.FindAtomicActionOrAbstraction(firstActionName);
+ secondAction = ctc.FindAtomicActionOrAbstraction(secondActionName);
+ if (firstAction == null)
+ {
+ ctc.Error(kv, $"Could not find atomic action {firstActionName}");
+ }
+ if (secondAction == null)
+ {
+ ctc.Error(kv, $"Could not find atomic action {secondActionName}");
+ }
+ if (firstAction != null && secondAction != null)
+ {
+ CheckInParams(function.InParams);
+ }
+ hints.Add(new CommutativityHint(function, firstAction, secondAction, args));
+ }
+ else
+ {
+ ctc.Error(kv, "Commutativity attribute expects two action names as parameters");
+ }
+ }
+
+ // And then we look for either {:witness "globalVar"} or {:lemma}
+ for (QKeyValue kv = function.Attributes; kv != null; kv = kv.Next)
+ {
+ if (kv.Key == CivlAttributes.WITNESS)
+ {
+ if (kv.Params.Count == 1 &&
+ kv.Params[0] is string witnessedVariableName)
+ {
+ Variable witnessedVariable = ctc.sharedVariables.Find(v => v.Name == witnessedVariableName);
+ if (witnessedVariable == null)
+ {
+ ctc.Error(kv, $"Could not find shared variable {witnessedVariableName}");
+ }
+ else if (!function.OutParams[0].TypedIdent.Type.Equals(witnessedVariable.TypedIdent.Type))
+ {
+ ctc.Error(function, "Result type does not match witnessed variable");
+ }
+ else
+ {
+ hints.ForEach(h => commutativityHints.AddWitness(new CommutativityWitness(witnessedVariable, h)));
+ }
+ }
+ else
+ {
+ ctc.Error(kv, "Witness attribute expects the name of a global variable as parameter");
+ }
+ break;
+ }
+ else if (kv.Key == CivlAttributes.LEMMA)
+ {
+ if (kv.Params.Count == 0)
+ {
+ if (!function.OutParams[0].TypedIdent.Type.Equals(Type.Bool))
+ {
+ ctc.Error(function, "Result type of lemma must be bool");
+ }
+ else
+ {
+ hints.ForEach(h => commutativityHints.AddLemma(h));
+ }
+ }
+ else
+ {
+ ctc.Error(kv, "Lemma attribute does not expect any parameters");
+ }
+ break;
+ }
+ }
+ }
+
+ private void CheckInParams(List<Variable> inParams)
+ {
+ args = new List<Expr>();
+ foreach (var param in inParams)
+ {
+ Expr arg = null;
+ if (param.Name.StartsWith(FirstProcInputPrefix, StringComparison.Ordinal))
+ {
+ arg = CheckLocal(param, firstAction.firstImpl, FirstProcInputPrefix);
+ }
+ else if (param.Name.StartsWith(SecondProcInputPrefix, StringComparison.Ordinal))
+ {
+ arg = CheckLocal(param, secondAction.secondImpl, SecondProcInputPrefix);
+ }
+ else
+ {
+ arg = CheckGlobal(param);
+ }
+ args.Add(arg);
+ }
+ }
+
+ private Expr CheckLocal(Variable param, Implementation impl, string prefix)
+ {
+ var var = FindVariable(param.Name, param.TypedIdent.Type,
+ impl.InParams.Union(impl.OutParams));
+ if (var != null)
+ return Expr.Ident(var);
+ var name = param.Name.Remove(0, prefix.Length);
+ ctc.Error(param, $"Action {impl.Name} does not have parameter {name}:{param.TypedIdent.Type}");
+ return null;
+ }
+
+ private Expr CheckGlobal(Variable param)
+ {
+ bool postState = param.Name.EndsWith(PostStateSuffix, StringComparison.Ordinal);
+ var name = param.Name;
+ if (postState)
+ name = name.Substring(0, name.Length - 1);
+ var var = FindVariable(name, param.TypedIdent.Type, ctc.sharedVariables);
+ if (var != null)
+ {
+ if (!postState)
+ return ExprHelper.Old(Expr.Ident(var));
+ else
+ return Expr.Ident(var);
+ }
+ ctc.Error(param, $"No shared variable {name}:{param.TypedIdent.Type}");
+ return null;
+ }
+
+ private Variable FindVariable(string name, Type type, IEnumerable<Variable> vars)
+ {
+ return vars.FirstOrDefault(i => i.Name == name && i.TypedIdent.Type.Equals(type));
+ }
+ }
+}
diff --git a/Source/Concurrency/Concurrency.csproj b/Source/Concurrency/Concurrency.csproj
index e13116c08..baa73eb01 100644
--- a/Source/Concurrency/Concurrency.csproj
+++ b/Source/Concurrency/Concurrency.csproj
@@ -67,7 +67,7 @@
<Compile Include="YieldingProcDuplicator.cs" />
<Compile Include="YieldTypeChecker.cs" />
<Compile Include="CivlUtil.cs" />
- <Compile Include="Witnesses.cs" />
+ <Compile Include="CommutativityHints.cs" />
<Compile Include="CivlCoreTypes.cs" />
<Compile Include="InductiveSequentialization.cs" />
<Compile Include="PendingAsyncChecker.cs" />
diff --git a/Source/Concurrency/MoverCheck.cs b/Source/Concurrency/MoverCheck.cs
index cb165bf99..515a9e147 100644
--- a/Source/Concurrency/MoverCheck.cs
+++ b/Source/Concurrency/MoverCheck.cs
@@ -147,8 +147,7 @@ private void CreateCommutativityChecker(AtomicAction first, AtomicAction second)
foreach (AssertCmd assertCmd in Enumerable.Union(first.firstGate, second.secondGate))
requires.Add(new Requires(false, assertCmd.Expr));
- civlTypeChecker.atomicActionPairToWitnessFunctions.TryGetValue(
- Tuple.Create(first, second), out List<WitnessFunction> witnesses);
+ var witnesses = civlTypeChecker.commutativityHints.GetWitnesses(first, second);
var transitionRelation = TransitionRelationComputation.
Commutativity(second, first, frame, witnesses);
@@ -165,6 +164,10 @@ private void CreateCommutativityChecker(AtomicAction first, AtomicAction second)
second.secondImpl.OutParams.Select(Expr.Ident).ToList()
) { Proc = second.proc }
};
+ foreach (var lemma in civlTypeChecker.commutativityHints.GetLemmas(first,second))
+ {
+ cmds.Add(CmdHelper.AssumeCmd(ExprHelper.FunctionCall(lemma.function, lemma.args.ToArray())));
+ }
var block = new Block(Token.NoToken, "init", cmds, new ReturnCmd(Token.NoToken));
var secondInParamsFiltered = second.secondImpl.InParams.Where(v => linearTypeChecker.FindLinearKind(v) != LinearKind.LINEAR_IN);
diff --git a/Source/Concurrency/TransitionRelationComputation.cs b/Source/Concurrency/TransitionRelationComputation.cs
index 481c45b3e..8e56e15de 100644
--- a/Source/Concurrency/TransitionRelationComputation.cs
+++ b/Source/Concurrency/TransitionRelationComputation.cs
@@ -12,7 +12,7 @@ public class TransitionRelationComputation
private readonly Dictionary<Variable, Function> triggers;
private readonly HashSet<Variable> frame;
private readonly HashSet<Variable> allInParams, allOutParams, allLocVars;
- private readonly Dictionary<Variable, List<WitnessFunction>> globalVarToWitnesses;
+ private readonly Dictionary<Variable, List<CommutativityWitness>> globalVarToWitnesses;
private readonly bool ignorePostState;
private readonly string messagePrefix;
@@ -36,7 +36,7 @@ public class TransitionRelationComputation
private TransitionRelationComputation(
Implementation first, Implementation second,
- IEnumerable<Variable> frame, List<WitnessFunction> witnesses, Dictionary<Variable, Function> triggers, bool ignorePostState,
+ IEnumerable<Variable> frame, IEnumerable<CommutativityWitness> witnesses, Dictionary<Variable, Function> triggers, bool ignorePostState,
string messagePrefix)
{
this.first = first;
@@ -59,7 +59,7 @@ private TransitionRelationComputation(
this.checkingContext = new CheckingContext(null);
this.pathTranslations = new List<Expr>();
- this.globalVarToWitnesses = new Dictionary<Variable, List<WitnessFunction>>();
+ this.globalVarToWitnesses = new Dictionary<Variable, List<CommutativityWitness>>();
if (witnesses != null)
{
foreach (var witness in witnesses)
@@ -67,7 +67,7 @@ private TransitionRelationComputation(
var gVar = witness.witnessedVariable;
if (!globalVarToWitnesses.ContainsKey(gVar))
{
- globalVarToWitnesses[gVar] = new List<WitnessFunction>();
+ globalVarToWitnesses[gVar] = new List<CommutativityWitness>();
}
globalVarToWitnesses[gVar].Add(witness);
}
@@ -76,7 +76,7 @@ private TransitionRelationComputation(
private static Expr ComputeTransitionRelation(
Implementation first, Implementation second,
- IEnumerable<Variable> frame, Dictionary<Variable, Function> triggers, List<WitnessFunction> witnesses, bool ignorePostState,
+ IEnumerable<Variable> frame, Dictionary<Variable, Function> triggers, IEnumerable<CommutativityWitness> witnesses, bool ignorePostState,
string messagePrefix)
{
var trc = new TransitionRelationComputation(first, second, frame, witnesses, triggers, ignorePostState, messagePrefix);
@@ -88,7 +88,7 @@ private static Expr ComputeTransitionRelation(
}
public static Expr Commutativity(AtomicAction first, AtomicAction second,
- HashSet<Variable> frame, List<WitnessFunction> witnesses)
+ HashSet<Variable> frame, IEnumerable<CommutativityWitness> witnesses)
{
var triggers = first.triggerFunctions.Union(second.triggerFunctions).ToDictionary(kv => kv.Key, kv => kv.Value);
return ComputeTransitionRelation(
@@ -484,7 +484,7 @@ private void ReplacePreOrPostStateVars()
private void ComputeWitnessedTransitionRelationExprs()
{
witnessedTransitionRelations = new List<Expr>();
- Dictionary<Variable, List<WitnessFunction>> varToWitnesses = trc.FrameWithWitnesses.
+ Dictionary<Variable, List<CommutativityWitness>> varToWitnesses = trc.FrameWithWitnesses.
Where(x => NotEliminatedVars.Contains(frameIntermediateCopy[x])).
ToDictionary(
x => frameIntermediateCopy[x],
@@ -492,12 +492,12 @@ private void ComputeWitnessedTransitionRelationExprs()
foreach (var witnessSet in varToWitnesses.Values.CartesianProduct())
{
Dictionary<Variable, Expr> witnessSubst = new Dictionary<Variable, Expr>();
- foreach (Tuple<Variable, WitnessFunction> pair in
+ foreach (Tuple<Variable, CommutativityWitness> pair in
Enumerable.Zip(varToWitnesses.Keys, witnessSet, Tuple.Create))
{
- WitnessFunction witnessFunction = pair.Item2;
+ CommutativityWitness witness = pair.Item2;
witnessSubst[pair.Item1] = ExprHelper.FunctionCall(
- witnessFunction.function, witnessFunction.args.ToArray()
+ witness.function, witness.args.ToArray()
);
}
witnessedTransitionRelations.Add(
diff --git a/Source/Concurrency/Witnesses.cs b/Source/Concurrency/Witnesses.cs
deleted file mode 100644
index 878cad05e..000000000
--- a/Source/Concurrency/Witnesses.cs
+++ /dev/null
@@ -1,156 +0,0 @@
-using System;
-using System.Collections.Generic;
-using System.Diagnostics;
-using System.Linq;
-
-namespace Microsoft.Boogie
-{
- public class WitnessFunction
- {
- public readonly Function function;
- public readonly Variable witnessedVariable;
- public readonly AtomicAction firstAction;
- public readonly AtomicAction secondAction;
- public List<Expr> args;
-
- public WitnessFunction(Function function, Variable witnessedVariable,
- AtomicAction firstAction, AtomicAction secondAction, List<Expr> args)
- {
- this.function = function;
- this.witnessedVariable = witnessedVariable;
- this.firstAction = firstAction;
- this.secondAction = secondAction;
- this.args = args;
- }
- }
-
- class WitnessFunctionVisitor
- {
- private const string FirstProcInputPrefix = "first_";
- private const string SecondProcInputPrefix = "second_";
- private const string PostStateSuffix = "'";
-
- private readonly CivlTypeChecker ctc;
- internal List<WitnessFunction> allWitnessFunctions;
-
- private Variable witnessedVariable;
- private AtomicAction firstAction;
- private AtomicAction secondAction;
- private List<Expr> args;
-
- public WitnessFunctionVisitor(CivlTypeChecker ctc)
- {
- this.ctc = ctc;
- allWitnessFunctions = new List<WitnessFunction>();
- }
-
- public void VisitFunctions()
- {
- foreach (var f in ctc.program.Functions)
- {
- VisitFunction(f);
- }
- }
-
- private void VisitFunction(Function function)
- {
- Debug.Assert(function.OutParams.Count == 1);
- for (QKeyValue kv = function.Attributes; kv != null; kv = kv.Next)
- {
- if (kv.Key != CivlAttributes.WITNESS)
- continue;
- if (kv.Params.Count == 3 &&
- kv.Params[0] is string witnessedVariableName &&
- kv.Params[1] is string firstActionName &&
- kv.Params[2] is string secondActionName)
- {
- witnessedVariable = ctc.sharedVariables.Find(v => v.Name == witnessedVariableName);
- if (witnessedVariable == null)
- {
- ctc.Error(kv, $"Could not find shared variable {witnessedVariableName}");
- }
- else if (!function.OutParams[0].TypedIdent.Type.Equals(witnessedVariable.TypedIdent.Type))
- {
- ctc.Error(function, "Result type does not match witnessed variable");
- }
- firstAction = ctc.FindAtomicAction(firstActionName);
- secondAction = ctc.FindAtomicAction(secondActionName);
- if (firstAction == null)
- {
- ctc.Error(kv, $"Could not find atomic action {firstActionName}");
- }
- if (secondAction == null)
- {
- ctc.Error(kv, $"Could not find atomic action {firstActionName}");
- }
- if (firstAction != null && secondAction != null)
- {
- CheckInParams(function.InParams);
- }
- allWitnessFunctions.Add(new WitnessFunction(function, witnessedVariable,
- firstAction, secondAction, args));
- }
- else
- {
- ctc.Error(kv, "Witness attribute expects three string parameters");
- }
- }
- }
-
- private void CheckInParams(List<Variable> inParams)
- {
- args = new List<Expr>();
- foreach (var param in inParams)
- {
- Expr arg = null;
- if (param.Name.StartsWith(FirstProcInputPrefix, StringComparison.Ordinal))
- {
- arg = CheckLocal(param, firstAction.firstImpl, FirstProcInputPrefix);
- }
- else if (param.Name.StartsWith(SecondProcInputPrefix, StringComparison.Ordinal))
- {
- arg = CheckLocal(param, secondAction.secondImpl, SecondProcInputPrefix);
- }
- else
- {
- arg = CheckGlobal(param);
- }
- args.Add(arg);
- }
- }
-
- private Expr CheckLocal(Variable param, Implementation impl, string prefix)
- {
- var var = FindVariable(param.Name, param.TypedIdent.Type,
- impl.InParams.Union(impl.OutParams));
- if (var != null)
- return Expr.Ident(var);
- var name = param.Name.Remove(0, prefix.Length);
- ctc.Error(param, $"Action {impl.Name} does not have parameter {name}:{param.TypedIdent.Type}");
- return null;
- }
-
- private Expr CheckGlobal(Variable param)
- {
- bool postState = param.Name.EndsWith(PostStateSuffix, StringComparison.Ordinal);
- var name = param.Name;
- if (postState)
- name = name.Substring(0, name.Length - 1);
- var var = FindVariable(name, param.TypedIdent.Type, ctc.sharedVariables);
- if (var != null)
- {
- if (!postState)
- return ExprHelper.Old(Expr.Ident(var));
- else
- return Expr.Ident(var);
- }
- ctc.Error(param, $"No shared variable {name}:{param.TypedIdent.Type}");
- return null;
- }
-
- private Variable FindVariable(string name, Type type, IEnumerable<Variable> vars)
- {
- return vars.FirstOrDefault(i => i.Name == name && i.TypedIdent.Type.Equals(type));
- }
- }
-}
diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs
index d7e815b14..11129463e 100644
--- a/Source/Core/CivlAttributes.cs
+++ b/Source/Core/CivlAttributes.cs
@@ -27,6 +27,8 @@ public static class CivlAttributes
public const string LINEAR_OUT = "linear_out";
public const string BACKWARD = "backward";
+ public const string COMMUTATIVITY = "commutativity";
+ public const string LEMMA = "lemma";
public const string WITNESS = "witness";
public const string PENDING_ASYNC = "pending_async";
@@ -39,7 +41,8 @@ public static class CivlAttributes
public const string CHOICE = "choice";
private static string[] CIVL_ATTRIBUTES =
- {LAYER, YIELDS, ATOMIC, LEFT, RIGHT, BOTH, REFINES, WITNESS,
+ {LAYER, YIELDS, ATOMIC, LEFT, RIGHT, BOTH, REFINES,
+ COMMUTATIVITY, LEMMA, WITNESS,
PENDING_ASYNC, IS, IS_INVARIANT, IS_ABSTRACTION, ELIM, CHOICE };
private static string[] LINEAR_ATTRIBUTES =
diff --git a/Test/civl/async/2pc-triggers.bpl b/Test/civl/async/2pc-triggers.bpl
index 03ad0cc97..1b3849ea8 100644
--- a/Test/civl/async/2pc-triggers.bpl
+++ b/Test/civl/async/2pc-triggers.bpl
@@ -173,13 +173,14 @@ procedure {:yields} {:layer 11} YieldConsistent_11 ()
// ###########################################################################
function
-{:witness "state","atomic_Coordinator_VoteNo","atomic_Coordinator_VoteNo"}
-{:witness "state","atomic_Coordinator_VoteYes","atomic_Coordinator_VoteNo"}
-{:witness "state","atomic_Coordinator_VoteNo","atomic_Coordinator_VoteYes"}
-{:witness "state","atomic_Coordinator_VoteYes","atomic_Coordinator_VoteYes"}
-{:witness "state","atomic_SetParticipantAborted","atomic_Coordinator_VoteYes"}
-{:witness "state","atomic_SetParticipantAborted","atomic_Coordinator_VoteNo"}
-{:witness "state","atomic_Participant_VoteReq","atomic_Participant_VoteReq"}
+{:witness "state"}
+{:commutativity "atomic_Coordinator_VoteNo","atomic_Coordinator_VoteNo"}
+{:commutativity "atomic_Coordinator_VoteYes","atomic_Coordinator_VoteNo"}
+{:commutativity "atomic_Coordinator_VoteNo","atomic_Coordinator_VoteYes"}
+{:commutativity "atomic_Coordinator_VoteYes","atomic_Coordinator_VoteYes"}
+{:commutativity "atomic_SetParticipantAborted","atomic_Coordinator_VoteYes"}
+{:commutativity "atomic_SetParticipantAborted","atomic_Coordinator_VoteNo"}
+{:commutativity "atomic_Participant_VoteReq","atomic_Participant_VoteReq"}
witness (state:GState, state':GState, second_xid:Xid) : GState
{
state[second_xid := state'[second_xid]]
diff --git a/Test/civl/async/2pc.bpl b/Test/civl/async/2pc.bpl
index 8dc78f0af..4c247e720 100644
--- a/Test/civl/async/2pc.bpl
+++ b/Test/civl/async/2pc.bpl
@@ -163,13 +163,14 @@ procedure {:yields} {:layer 11} YieldConsistent_11 ()
// ###########################################################################
function
-{:witness "state","atomic_Coordinator_VoteNo","atomic_Coordinator_VoteNo"}
-{:witness "state","atomic_Coordinator_VoteYes","atomic_Coordinator_VoteNo"}
-{:witness "state","atomic_Coordinator_VoteNo","atomic_Coordinator_VoteYes"}
-{:witness "state","atomic_Coordinator_VoteYes","atomic_Coordinator_VoteYes"}
-{:witness "state","atomic_SetParticipantAborted","atomic_Coordinator_VoteYes"}
-{:witness "state","atomic_SetParticipantAborted","atomic_Coordinator_VoteNo"}
-{:witness "state","atomic_Participant_VoteReq","atomic_Participant_VoteReq"}
+{:witness "state"}
+{:commutativity "atomic_Coordinator_VoteNo","atomic_Coordinator_VoteNo"}
+{:commutativity "atomic_Coordinator_VoteYes","atomic_Coordinator_VoteNo"}
+{:commutativity "atomic_Coordinator_VoteNo","atomic_Coordinator_VoteYes"}
+{:commutativity "atomic_Coordinator_VoteYes","atomic_Coordinator_VoteYes"}
+{:commutativity "atomic_SetParticipantAborted","atomic_Coordinator_VoteYes"}
+{:commutativity "atomic_SetParticipantAborted","atomic_Coordinator_VoteNo"}
+{:commutativity "atomic_Participant_VoteReq","atomic_Participant_VoteReq"}
witness (state:GState, state':GState, second_xid:Xid) : GState
{
state[second_xid := state'[second_xid]]
diff --git a/Test/civl/commutativity-lemma.bpl b/Test/civl/commutativity-lemma.bpl
new file mode 100644
index 000000000..9027364e6
--- /dev/null
+++ b/Test/civl/commutativity-lemma.bpl
@@ -0,0 +1,23 @@
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+// Contrived example to illustrate the injection of lemmas into commutativity checks
+
+var {:layer 0,1} x : int;
+
+function f(x: int, i: int) : int;
+
+function {:inline}
+{:lemma}
+{:commutativity "inc", "inc"}
+lemma (x: int, first_i: int, second_i: int) : bool
+{
+ f(x, first_i) == x + first_i &&
+ f(x + first_i, second_i) == x + first_i + second_i &&
+ f(x, second_i) == x + second_i &&
+ f(x + second_i, first_i) == x + second_i + first_i
+}
+
+procedure {:right} {:layer 1} inc (i: int)
+modifies x;
+{ x := f(x, i); }
diff --git a/Test/civl/commutativity-lemma.bpl.expect b/Test/civl/commutativity-lemma.bpl.expect
new file mode 100644
index 000000000..37fad75c9
--- /dev/null
+++ b/Test/civl/commutativity-lemma.bpl.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/civl/verified-ft.bpl b/Test/civl/verified-ft.bpl
index 36cf6810b..86b3a77fc 100644
--- a/Test/civl/verified-ft.bpl
+++ b/Test/civl/verified-ft.bpl
@@ -1197,18 +1197,19 @@ function {:inline false} f(i: int): bool { true }
function
-{:witness "shadow.VC","AtomicVC.Inc","AtomicVC.Copy"}
-{:witness "shadow.VC","AtomicVC.Inc","AtomicVC.Join"}
-{:witness "shadow.VC","AtomicVCSetElem","AtomicVC.Copy"}
-{:witness "shadow.VC","AtomicVCSetElem","AtomicVC.Join"}
-{:witness "shadow.VC","AtomicVCSetElemShared","AtomicVC.Copy"}
-{:witness "shadow.VC","AtomicVCSetElemShared","AtomicVC.Join"}
-{:witness "shadow.VC","AtomicVCInit","AtomicVC.Copy"}
-{:witness "shadow.VC","AtomicVCInit","AtomicVC.Join"}
-{:witness "shadow.VC","AtomicVC.Copy","AtomicVC.Copy"}
-{:witness "shadow.VC","AtomicVC.Copy","AtomicVC.Join"}
-{:witness "shadow.VC","AtomicVC.Join","AtomicVC.Copy"}
-{:witness "shadow.VC","AtomicVC.Join","AtomicVC.Join"}
+{:witness "shadow.VC"}
+{:commutativity "AtomicVC.Inc","AtomicVC.Copy"}
+{:commutativity "AtomicVC.Inc","AtomicVC.Join"}
+{:commutativity "AtomicVCSetElem","AtomicVC.Copy"}
+{:commutativity "AtomicVCSetElem","AtomicVC.Join"}
+{:commutativity "AtomicVCSetElemShared","AtomicVC.Copy"}
+{:commutativity "AtomicVCSetElemShared","AtomicVC.Join"}
+{:commutativity "AtomicVCInit","AtomicVC.Copy"}
+{:commutativity "AtomicVCInit","AtomicVC.Join"}
+{:commutativity "AtomicVC.Copy","AtomicVC.Copy"}
+{:commutativity "AtomicVC.Copy","AtomicVC.Join"}
+{:commutativity "AtomicVC.Join","AtomicVC.Copy"}
+{:commutativity "AtomicVC.Join","AtomicVC.Join"}
witness (shadow.VC:[Shadowable]VC, shadow.VC':[Shadowable]VC, second_v1:Shadowable) : [Shadowable]VC
{
shadow.VC[second_v1 := shadow.VC'[second_v1]]