Skip to content

Commit

Permalink
Merge remote-tracking branch 'origin/master' into verificationTaskPer…
Browse files Browse the repository at this point in the history 
…Split
  • Loading branch information
@keyboardDrummer
keyboardDrummer committed Jan 26, 2024
2 parents 1508b9e + 2ba9c4a commit d6446ab
Show file tree
Hide file tree
Showing 50 changed files with 1,421 additions and 1,488 deletions.
4 changes: 2 additions & 2 deletions Source/Concurrency/CivlCoreTypes.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,9 +42,9 @@ public Action(CivlTypeChecker civlTypeChecker, ActionDecl actionDecl, Action ref
new DatatypeTypeCtorDecl(Token.NoToken, choiceDatatypeName, new List<TypeVariable>(), null);
PendingAsyncs.ForEach(elim =>
{
var field = new TypedIdent(Token.NoToken, elim.Name, elim.PendingAsyncType);
var field = new Formal(Token.NoToken, new TypedIdent(Token.NoToken, elim.Name, elim.PendingAsyncType), true);
ChoiceDatatypeTypeCtorDecl.AddConstructor(Token.NoToken, $"{choiceDatatypeName}_{elim.Name}",
new List<TypedIdent>() { field });
new List<Variable>() { field });
});
civlTypeChecker.program.AddTopLevelDeclaration(ChoiceDatatypeTypeCtorDecl);
DesugarSetChoice(civlTypeChecker, ImplWithChoice);
Expand Down
13 changes: 13 additions & 0 deletions Source/Concurrency/CivlTypeChecker.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -297,6 +297,15 @@ private void TypeCheckYieldingProcedures()

private void InlineAtomicActions(HashSet<ActionDecl> actionDecls)
{
var primitiveImpls = program.TopLevelDeclarations.OfType<Implementation>().Where(impl =>
{
var originalDecl = impl.Proc.OriginalDeclWithFormals;
return originalDecl != null && CivlPrimitives.LinearPrimitives.Contains(originalDecl.Name);
});
primitiveImpls.ForEach(impl => {
impl.OriginalBlocks = impl.Blocks;
impl.OriginalLocVars = impl.LocVars;
});
CivlUtil.AddInlineAttribute(SkipActionDecl);
actionDecls.ForEach(proc =>
{
Expand All @@ -319,6 +328,10 @@ private void InlineAtomicActions(HashSet<ActionDecl> actionDecls)
impl.OriginalBlocks = null;
impl.OriginalLocVars = null;
});
primitiveImpls.ForEach(impl => {
impl.OriginalBlocks = null;
impl.OriginalLocVars = null;
});
}

private void CreateAtomicActions(HashSet<ActionDecl> actionDecls)
Expand Down
17 changes: 9 additions & 8 deletions Source/Concurrency/InductiveSequentialization.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -182,7 +182,6 @@ private Cmd Transform(Dictionary<CtorType, Implementation> eliminatedPendingAsyn
public class InductiveSequentialization : Sequentialization
{
private Action invariantAction;
private HashSet<Variable> frame;
private IdentifierExpr choice;
private Dictionary<CtorType, Variable> newPAs;

Expand All @@ -193,7 +192,6 @@ public InductiveSequentialization(CivlTypeChecker civlTypeChecker, Action target
// - the modified set of each of each eliminated and abstract action associated with this invariant.
// - the target and refined action of every application of inductive sequentialization that refers to this invariant.
this.invariantAction = invariantAction;
frame = new HashSet<Variable>(invariantAction.ModifiedGlobalVars);
choice = Expr.Ident(invariantAction.ImplWithChoice.OutParams.Last());
newPAs = invariantAction.PendingAsyncs.ToDictionary(decl => decl.PendingAsyncType,
decl => (Variable)civlTypeChecker.LocalVariable($"newPAs_{decl.Name}", decl.PendingAsyncMultisetType));
Expand All @@ -202,7 +200,7 @@ public InductiveSequentialization(CivlTypeChecker civlTypeChecker, Action target
private List<Declaration> GenerateBaseCaseChecker()
{
var requires = invariantAction.Gate.Select(g => new Requires(false, g.Expr)).ToList();

var subst = targetAction.GetSubstitution(invariantAction);
var cmds = targetAction.GetGateAsserts(subst,
$"Gate of {targetAction.Name} fails in IS base check against invariant {invariantAction.Name}").ToList<Cmd>();
Expand All @@ -215,7 +213,7 @@ private List<Declaration> GenerateBaseCaseChecker()
outputVars.AddRange(targetAction.PendingAsyncs.Select(action =>
invariantAction.Impl.OutParams[pendingAsyncTypeToOutputParamIndex[action.PendingAsyncType]]));
cmds.Add(CmdHelper.CallCmd(targetAction.Impl.Proc, invariantAction.Impl.InParams, outputVars));

// Assign empty multiset to the rest
var remainderPendingAsyncs = invariantAction.PendingAsyncs.Except(targetAction.PendingAsyncs);
if (remainderPendingAsyncs.Any())
Expand All @@ -228,6 +226,7 @@ private List<Declaration> GenerateBaseCaseChecker()
cmds.Add(CmdHelper.AssignCmd(lhss, rhss));
}

var frame = new HashSet<Variable>(invariantAction.ModifiedGlobalVars);
cmds.Add(GetCheck(targetAction.tok, invariantAction.GetTransitionRelation(civlTypeChecker, frame),
$"IS base of {targetAction.Name} failed"));

Expand All @@ -246,6 +245,7 @@ private List<Declaration> GenerateConclusionChecker()
cmds.Add(CmdHelper.CallCmd(invariantAction.Impl.Proc, invariantAction.Impl.InParams,
invariantAction.Impl.OutParams));
cmds.Add(CmdHelper.AssumeCmd(NoPendingAsyncs));
var frame = new HashSet<Variable>(refinedAction.ModifiedGlobalVars);
cmds.Add(GetCheck(targetAction.tok, Substituter.Apply(subst, refinedAction.GetTransitionRelation(civlTypeChecker, frame)),
$"IS conclusion of {targetAction.Name} failed"));

Expand Down Expand Up @@ -300,6 +300,7 @@ private List<Declaration> GenerateStepChecker(Action pendingAsync)
cmds.Add(new AssignCmd(Token.NoToken, lhss, rhss));
}

var frame = new HashSet<Variable>(invariantAction.ModifiedGlobalVars);
cmds.Add(GetCheck(invariantAction.tok, invariantAction.GetTransitionRelation(civlTypeChecker, frame),
$"IS step of {invariantAction.Name} with {abs.Name} failed"));

Expand All @@ -315,7 +316,7 @@ private List<Declaration> GenerateStepChecker(Action pendingAsync)
* A key concept used in the generation of this extra assumption is the input-output transition relation of an action.
* This relation is obtained by taking the conjunction of the gate and transition relation of the action and
* existentially quantifying globals in the pre and the post state.
*
*
* There are two parts to the assumption, one for leftMover and the other for action.
* Both parts are stated in the context of the input-output relation of the invariant action.
* - The invocation of leftMover is identical to the choice made by the invariant.
Expand Down Expand Up @@ -427,7 +428,7 @@ private List<Declaration> GetCheckerTuple(string checkerName, List<Requires> req
inParams,
outParams,
requires,
frame.Select(Expr.Ident).ToList(),
invariantAction.ModifiedGlobalVars.Select(Expr.Ident).ToList(),
new List<Ensures>());
var impl = DeclHelper.Implementation(
proc,
Expand Down Expand Up @@ -457,7 +458,7 @@ private Expr ChoiceTest(CtorType pendingAsyncType)
{
return ExprHelper.IsConstructor(choice, invariantAction.ChoiceConstructor(pendingAsyncType).Name);
}

private Expr NoPendingAsyncs
{
get
Expand All @@ -468,7 +469,7 @@ private Expr NoPendingAsyncs
return expr;
}
}

private AssignCmd RemoveChoice(CtorType pendingAsyncType)
{
var rhs = Expr.Sub(Expr.Select(PAs(pendingAsyncType), Choice(pendingAsyncType)), Expr.Literal(1));
Expand Down
29 changes: 16 additions & 13 deletions Source/Concurrency/LinearDomainCollector.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -176,11 +176,7 @@ private Type GetPermissionType(Type type)
var typeCtorDecl = type.AsCtor.Decl;
var originalTypeCtorDecl = Monomorphizer.GetOriginalDecl(typeCtorDecl);
var actualTypeParams = program.monomorphizer.GetTypeInstantiation(typeCtorDecl);
return
originalTypeCtorDecl.Name == "Lheap"
? new CtorType(Token.NoToken, program.monomorphizer.InstantiateTypeCtorDecl("Ref", actualTypeParams),
new List<Type>())
: actualTypeParams[0];
return actualTypeParams[0];
}

private Dictionary<Type, LinearDomain> MakeLinearDomains()
Expand All @@ -198,14 +194,21 @@ private Dictionary<Type, LinearDomain> MakeLinearDomains()
}
if (!permissionTypeToCollectors[permissionType].ContainsKey(type))
{
var typeParamInstantiationMap = new Dictionary<string, Type> { { "V", actualTypeParams[0] } };
var collector =
originalTypeCtorDecl.Name == "Lheap"
? program.monomorphizer.InstantiateFunction("Lheap_Collector", typeParamInstantiationMap) :
originalTypeCtorDecl.Name == "Lset"
? program.monomorphizer.InstantiateFunction("Lset_Collector", typeParamInstantiationMap) :
program.monomorphizer.InstantiateFunction("Lval_Collector", typeParamInstantiationMap);
permissionTypeToCollectors[permissionType].Add(type, collector);
if (originalTypeCtorDecl.Name == "Lmap")
{
var typeParamInstantiationMap = new Dictionary<string, Type> { { "K", actualTypeParams[0] }, { "V", actualTypeParams[1] } };
var collector = program.monomorphizer.InstantiateFunction("Lmap_Collector", typeParamInstantiationMap);
permissionTypeToCollectors[permissionType].Add(type, collector);
}
else
{
var typeParamInstantiationMap = new Dictionary<string, Type> { { "V", actualTypeParams[0] } };
var collector =
originalTypeCtorDecl.Name == "Lset"
? program.monomorphizer.InstantiateFunction("Lset_Collector", typeParamInstantiationMap) :
program.monomorphizer.InstantiateFunction("Lval_Collector", typeParamInstantiationMap);
permissionTypeToCollectors[permissionType].Add(type, collector);
}
}
}
var permissionTypeToLinearDomain =
Expand Down
4 changes: 2 additions & 2 deletions Source/Concurrency/LinearPermissionInstrumentation.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -46,15 +46,15 @@ public List<Cmd> ProcDisjointnessAndWellFormedAssumeCmds(Procedure proc, bool at
? FilterInParams(proc.InParams)
: FilterInOutParams(proc.InParams.Union(proc.OutParams));
return DisjointnessExprs(availableVars)
.Union(civlTypeChecker.linearTypeChecker.LheapWellFormedExpressions(availableVars))
.Union(civlTypeChecker.linearTypeChecker.LstoreWellFormedExpressions(availableVars))
.Select(expr => CmdHelper.AssumeCmd(expr)).ToList<Cmd>();
}

public List<Cmd> DisjointnessAndWellFormedAssumeCmds(Absy absy, bool addGlobals)
{
var availableVars = AvailableLinearLocalVars(absy).Union(addGlobals ? LinearGlobalVars() : new List<Variable>());
return DisjointnessExprs(availableVars)
.Union(civlTypeChecker.linearTypeChecker.LheapWellFormedExpressions(availableVars))
.Union(civlTypeChecker.linearTypeChecker.LstoreWellFormedExpressions(availableVars))
.Select(expr => CmdHelper.AssumeCmd(expr)).ToList<Cmd>();
}

Expand Down
Loading

0 comments on commit d6446ab

Please sign in to comment.