Skip to content

Commit

Permalink
[CIVL] Make names of new procedures, variables, and basic blocks uniq…
Browse files Browse the repository at this point in the history 
…ue (#279)

* Make names of new procedures, variables, and basic blocks unique

* Remove unused variable

* Make computation of unique prefix iterate over all names only once

* Use original procedure names in parallel call aggregator name

* Introduce AbsyMap class and improve name uniquification

* Fix linearity preservation in example

* proof update

Co-authored-by: Bernhard Kragl <[email protected]>
  • Loading branch information
@shazqadeer @bkragl
shazqadeer and bkragl authored Sep 6, 2020
1 parent cf4f174 commit b083fb1
Show file tree
Hide file tree
Showing 26 changed files with 311 additions and 207 deletions.
63 changes: 58 additions & 5 deletions Source/Concurrency/CivlTypeChecker.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,6 +15,7 @@ public class CivlTypeChecker
// Use public access methods.
private Dictionary<Variable, LayerRange> globalVarToLayerRange;
private Dictionary<Variable, LayerRange> localVarToLayerRange;
private string namePrefix;

public Dictionary<Block, YieldingLoop> yieldingLoops;
public Dictionary<Block, HashSet<int>> terminatingLoopHeaders;
Expand Down Expand Up @@ -68,9 +69,23 @@ public CivlTypeChecker(Program program)
this.implToPendingAsyncCollector = new Dictionary<Implementation, Variable>();
this.inductiveSequentializations = new List<InductiveSequentialization>();

IEnumerable<string> declNames = program.TopLevelDeclarations.OfType<NamedDeclaration>().Select(x => x.Name);
IEnumerable<string> localVarNames = VariableNameCollector.Collect(program);
IEnumerable<string> blockLabels = program.TopLevelDeclarations.OfType<Implementation>()
.SelectMany(x => x.Blocks.Select(y => y.Label));
var allNames = declNames.Union(localVarNames).Union(blockLabels);
namePrefix = "Civl_";
foreach (var name in allNames)
{
while (name.StartsWith(namePrefix))
{
namePrefix = namePrefix + "_";
}
}

var skipProcedure = new Procedure(
Token.NoToken,
"Skip",
AddNamePrefix("Skip"),
new List<TypeVariable>(),
new List<Variable>(),
new List<Variable>(),
Expand All @@ -79,16 +94,54 @@ public CivlTypeChecker(Program program)
new List<Ensures>());
var skipImplementation = new Implementation(
Token.NoToken,
"Skip",
skipProcedure.Name,
new List<TypeVariable>(),
new List<Variable>(),
new List<Variable>(),
new List<Variable>(),
new List<Block> {new Block(Token.NoToken, "Init", new List<Cmd>(), new ReturnCmd(Token.NoToken))})
new List<Block> {new Block(Token.NoToken, "init", new List<Cmd>(), new ReturnCmd(Token.NoToken))})
{Proc = skipProcedure};
SkipAtomicAction = new AtomicAction(skipProcedure, skipImplementation, LayerRange.MinMax, MoverType.Both);
}

public string AddNamePrefix(string name)
{
return $"{namePrefix}{name}";
}

public LocalVariable LocalVariable(string name, Type type)
{
return VarHelper.LocalVariable($"{namePrefix}{name}", type);
}

public BoundVariable BoundVariable(string name, Type type)
{
return VarHelper.BoundVariable($"{namePrefix}{name}", type);
}

public Formal Formal(string name, Type type, bool incoming)
{
return VarHelper.Formal($"{namePrefix}{name}", type, incoming);
}

private class VariableNameCollector : ReadOnlyVisitor
{
private HashSet<string> localVarNames = new HashSet<string>();

public static HashSet<string> Collect(Program program)
{
var collector = new VariableNameCollector();
collector.VisitProgram(program);
return collector.localVarNames;
}

public override Variable VisitVariable(Variable node)
{
localVarNames.Add(node.Name);
return node;
}
}

public void TypeCheck()
{
TypeCheckGlobalVariables();
Expand Down Expand Up @@ -375,7 +428,7 @@ kv.Params[0] is string refinedActionName &&
if (checkingContext.ErrorCount == 0)
{
inductiveSequentializations.Add(
new InductiveSequentialization(action, action.refinedAction, invariantAction, elim));
new InductiveSequentialization(this, action, action.refinedAction, invariantAction, elim));
}
}
}
Expand Down Expand Up @@ -2112,4 +2165,4 @@ public void VisitAtomicAction(AtomicAction action)
}
}
}
}
}
8 changes: 4 additions & 4 deletions Source/Concurrency/CivlVCGeneration.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,16 +21,16 @@ public static void Transform(CivlTypeChecker civlTypeChecker)
List<Declaration> decls = new List<Declaration>();
if (!CommandLineOptions.Clo.TrustMoverTypes)
{
MoverCheck.AddCheckers(linearTypeChecker, civlTypeChecker, decls);
MoverCheck.AddCheckers(civlTypeChecker, decls);
}

// Desugaring of yielding procedures
YieldingProcChecker.AddCheckers(linearTypeChecker, civlTypeChecker, decls);
YieldingProcChecker.AddCheckers(civlTypeChecker, decls);

// Linear type checks
LinearTypeChecker.AddCheckers(linearTypeChecker, civlTypeChecker, decls);
LinearTypeChecker.AddCheckers(civlTypeChecker, decls);

InductiveSequentializationChecker.AddChecks(civlTypeChecker);
InductiveSequentializationChecker.AddCheckers(civlTypeChecker);
PendingAsyncChecker.AddCheckers(civlTypeChecker);

foreach (AtomicAction action in civlTypeChecker.procToAtomicAction.Values.Union(civlTypeChecker
Expand Down
36 changes: 18 additions & 18 deletions Source/Concurrency/CommutativityHints.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -98,22 +98,22 @@ class CommutativityHintVisitor
private const string SecondProcInputPrefix = "second_";
private const string PostStateSuffix = "'";

private readonly CivlTypeChecker ctc;
private readonly CivlTypeChecker civlTypeChecker;
public CommutativityHints commutativityHints;

private AtomicAction firstAction;
private AtomicAction secondAction;
private List<Expr> args;

public CommutativityHintVisitor(CivlTypeChecker ctc)
public CommutativityHintVisitor(CivlTypeChecker civlTypeChecker)
{
this.ctc = ctc;
this.civlTypeChecker = civlTypeChecker;
commutativityHints = new CommutativityHints();
}

public void VisitFunctions()
{
foreach (var f in ctc.program.Functions)
foreach (var f in civlTypeChecker.program.Functions)
{
VisitFunction(f);
}
Expand All @@ -132,16 +132,16 @@ private void VisitFunction(Function function)
kv.Params[0] is string firstActionName &&
kv.Params[1] is string secondActionName)
{
firstAction = ctc.FindAtomicActionOrAbstraction(firstActionName);
secondAction = ctc.FindAtomicActionOrAbstraction(secondActionName);
firstAction = civlTypeChecker.FindAtomicActionOrAbstraction(firstActionName);
secondAction = civlTypeChecker.FindAtomicActionOrAbstraction(secondActionName);
if (firstAction == null)
{
ctc.Error(kv, $"Could not find atomic action {firstActionName}");
civlTypeChecker.Error(kv, $"Could not find atomic action {firstActionName}");
}

if (secondAction == null)
{
ctc.Error(kv, $"Could not find atomic action {secondActionName}");
civlTypeChecker.Error(kv, $"Could not find atomic action {secondActionName}");
}

if (firstAction != null && secondAction != null)
Expand All @@ -153,7 +153,7 @@ kv.Params[0] is string firstActionName &&
}
else
{
ctc.Error(kv, "Commutativity attribute expects two action names as parameters");
civlTypeChecker.Error(kv, "Commutativity attribute expects two action names as parameters");
}
}

Expand All @@ -165,14 +165,14 @@ kv.Params[0] is string firstActionName &&
if (kv.Params.Count == 1 &&
kv.Params[0] is string witnessedVariableName)
{
Variable witnessedVariable = ctc.GlobalVariables.First(v => v.Name == witnessedVariableName);
Variable witnessedVariable = civlTypeChecker.GlobalVariables.First(v => v.Name == witnessedVariableName);
if (witnessedVariable == null)
{
ctc.Error(kv, $"Could not find shared variable {witnessedVariableName}");
civlTypeChecker.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");
civlTypeChecker.Error(function, "Result type does not match witnessed variable");
}
else
{
Expand All @@ -181,7 +181,7 @@ kv.Params[0] is string firstActionName &&
}
else
{
ctc.Error(kv, "Witness attribute expects the name of a global variable as parameter");
civlTypeChecker.Error(kv, "Witness attribute expects the name of a global variable as parameter");
}

break;
Expand All @@ -192,7 +192,7 @@ kv.Params[0] is string firstActionName &&
{
if (!function.OutParams[0].TypedIdent.Type.Equals(Type.Bool))
{
ctc.Error(function, "Result type of lemma must be bool");
civlTypeChecker.Error(function, "Result type of lemma must be bool");
}
else
{
Expand All @@ -201,7 +201,7 @@ kv.Params[0] is string firstActionName &&
}
else
{
ctc.Error(kv, "Lemma attribute does not expect any parameters");
civlTypeChecker.Error(kv, "Lemma attribute does not expect any parameters");
}

break;
Expand Down Expand Up @@ -239,7 +239,7 @@ private Expr CheckLocal(Variable param, Implementation impl, string prefix)
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}");
civlTypeChecker.Error(param, $"Action {impl.Name} does not have parameter {name}:{param.TypedIdent.Type}");
return null;
}

Expand All @@ -249,7 +249,7 @@ private Expr CheckGlobal(Variable param)
var name = param.Name;
if (postState)
name = name.Substring(0, name.Length - 1);
var var = FindVariable(name, param.TypedIdent.Type, ctc.GlobalVariables);
var var = FindVariable(name, param.TypedIdent.Type, civlTypeChecker.GlobalVariables);
if (var != null)
{
if (!postState)
Expand All @@ -258,7 +258,7 @@ private Expr CheckGlobal(Variable param)
return Expr.Ident(var);
}

ctc.Error(param, $"No shared variable {name}:{param.TypedIdent.Type}");
civlTypeChecker.Error(param, $"No shared variable {name}:{param.TypedIdent.Type}");
return null;
}

Expand Down
5 changes: 3 additions & 2 deletions Source/Concurrency/GlobalSnapshotInstrumentation.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,11 +4,13 @@ namespace Microsoft.Boogie
{
class GlobalSnapshotInstrumentation
{
private CivlTypeChecker civlTypeChecker;
private Dictionary<Variable, Variable> oldGlobalMap;
private List<Variable> newLocalVars;

public GlobalSnapshotInstrumentation(CivlTypeChecker civlTypeChecker)
{
this.civlTypeChecker = civlTypeChecker;
newLocalVars = new List<Variable>();
oldGlobalMap = new Dictionary<Variable, Variable>();
foreach (Variable g in civlTypeChecker.GlobalVariables)
Expand Down Expand Up @@ -63,8 +65,7 @@ public List<Cmd> CreateInitCmds()

private LocalVariable OldGlobalLocal(Variable v)
{
return new LocalVariable(Token.NoToken,
new TypedIdent(Token.NoToken, $"civl_global_old_{v.Name}", v.TypedIdent.Type));
return civlTypeChecker.LocalVariable($"global_old_{v.Name}", v.TypedIdent.Type);
}
}
}
Loading

0 comments on commit b083fb1

Please sign in to comment.