Skip to content

Commit

Permalink
third commit
Browse files Browse the repository at this point in the history
  • Loading branch information
@shazqadeer
shazqadeer committed Dec 10, 2023
1 parent 5422f7b commit 22fcb97
Show file tree
Hide file tree
Showing 7 changed files with 206 additions and 93 deletions.
25 changes: 17 additions & 8 deletions Source/Concurrency/LinearDomainCollector.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -198,14 +198,23 @@ 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 == "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);
}
}
}
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
175 changes: 129 additions & 46 deletions Source/Concurrency/LinearRewriter.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,6 +81,12 @@ public List<Cmd> RewriteCallCmd(CallCmd callCmd)
return RewriteLheapAlloc(callCmd);
case "Lheap_Remove":
return RewriteLheapRemove(callCmd);
case "Lmap_Create":
return RewriteLmapCreate(callCmd);
case "Lmap_Get":
return RewriteLmapGet(callCmd);
case "Lmap_Put":
return RewriteLmapPut(callCmd);
case "Lset_Empty":
return RewriteLsetEmpty(callCmd);
case "Lset_Split":
Expand Down Expand Up @@ -259,51 +265,6 @@ private List<Cmd> RewriteLheapPut(CallCmd callCmd)
return cmdSeq;
}

private List<Cmd> CreateAccessAsserts(Expr expr, IToken tok, string msg)
{
if (expr is NAryExpr nAryExpr)
{
if (nAryExpr.Fun is FieldAccess)
{
return CreateAccessAsserts(nAryExpr.Args[0], tok, msg);
}
if (nAryExpr.Fun is MapSelect)
{
var mapExpr = nAryExpr.Args[0];
if (mapExpr is NAryExpr lheapValExpr &&
lheapValExpr.Fun is FieldAccess &&
lheapValExpr.Args[0].Type is CtorType ctorType &&
Monomorphizer.GetOriginalDecl(ctorType.Decl).Name == "Lheap")
{
var cmdSeq = CreateAccessAsserts(lheapValExpr.Args[0], tok, msg);
var lheapContainsFunc = LheapContains(nAryExpr.Type);
cmdSeq.Add(AssertCmd(tok, ExprHelper.FunctionCall(lheapContainsFunc, lheapValExpr.Args[0], nAryExpr.Args[1]), msg));
return cmdSeq;
}
}
}
return new List<Cmd>();
}

private List<Cmd> CreateAccessAsserts(AssignLhs assignLhs, IToken tok, string msg)
{
if (assignLhs is FieldAssignLhs fieldAssignLhs)
{
return CreateAccessAsserts(fieldAssignLhs.Datatype, tok, msg);
}
if (assignLhs is MapAssignLhs mapAssignLhs &&
mapAssignLhs.Map is FieldAssignLhs fieldAssignLhs1 &&
fieldAssignLhs1.Datatype.Type is CtorType ctorType &&
Monomorphizer.GetOriginalDecl(ctorType.Decl).Name == "Lheap")
{
var cmdSeq = CreateAccessAsserts(mapAssignLhs.Map, tok, msg);
var lheapContainsFunc = LheapContains(mapAssignLhs.Map.Type);
cmdSeq.Add(AssertCmd(tok, ExprHelper.FunctionCall(lheapContainsFunc, fieldAssignLhs1.Datatype.AsExpr, mapAssignLhs.Indexes[0]), msg));
return cmdSeq;
}
return new List<Cmd>();
}

private List<Cmd> RewriteLheapAlloc(CallCmd callCmd)
{
GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor,
Expand Down Expand Up @@ -356,6 +317,73 @@ private List<Cmd> RewriteLheapRemove(CallCmd callCmd)
return cmdSeq;
}

private List<Cmd> RewriteLmapCreate(CallCmd callCmd)
{
GetRelevantInfo(callCmd, out Type keyType, out Type valType, out Function lmapConstructor);

var cmdSeq = new List<Cmd>();
var k = callCmd.Ins[0];
var val = callCmd.Ins[1];
var l = callCmd.Outs[0].Decl;

cmdSeq.Add(CmdHelper.AssignCmd(l, ExprHelper.FunctionCall(lmapConstructor, k, val)));

ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
}

private List<Cmd> RewriteLmapGet(CallCmd callCmd)
{
GetRelevantInfo(callCmd, out Type keyType, out Type valType, out Function lmapConstructor);

var cmdSeq = new List<Cmd>();
var path = callCmd.Ins[0];
var k = callCmd.Ins[1];
var l = callCmd.Outs[0].Decl;

var mapImpFunc = MapImp(keyType);
var mapIteFunc = MapIte(keyType, valType);
var mapConstFunc1 = MapConst(keyType, Type.Bool);
var mapConstFunc2 = MapConst(keyType, valType);
var mapDiffFunc = MapDiff(keyType);

cmdSeq.Add(AssertCmd(callCmd.tok,
Expr.Eq(ExprHelper.FunctionCall(mapImpFunc, k, Dom(path)), ExprHelper.FunctionCall(mapConstFunc1, Expr.True)),
"Lmap_Get failed"));

cmdSeq.Add(CmdHelper.AssignCmd(l,
ExprHelper.FunctionCall(lmapConstructor, k,
ExprHelper.FunctionCall(mapIteFunc, k, Val(path), ExprHelper.FunctionCall(mapConstFunc2, Default(valType))))));

cmdSeq.Add(CmdHelper.AssignCmd(CmdHelper.ExprToAssignLhs(path),
ExprHelper.FunctionCall(lmapConstructor, ExprHelper.FunctionCall(mapDiffFunc, Dom(path), k),
ExprHelper.FunctionCall(mapIteFunc, ExprHelper.FunctionCall(mapDiffFunc, Dom(path), k), Val(path),
ExprHelper.FunctionCall(mapConstFunc2, Default(valType))))));

ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
}

private List<Cmd> RewriteLmapPut(CallCmd callCmd)
{
GetRelevantInfo(callCmd, out Type keyType, out Type valType, out Function lmapConstructor);

var cmdSeq = new List<Cmd>();
var path = callCmd.Ins[0];
var l = callCmd.Ins[1];

var mapOrFunc = MapOr(keyType);
var mapIteFunc = MapIte(keyType, valType);
cmdSeq.Add(CmdHelper.AssignCmd(
CmdHelper.ExprToAssignLhs(path),
ExprHelper.FunctionCall(lmapConstructor,
ExprHelper.FunctionCall(mapOrFunc, Dom(path), Dom(l)),
ExprHelper.FunctionCall(mapIteFunc, Dom(path), Val(path), Val(l)))));

ResolveAndTypecheck(options, cmdSeq);
return cmdSeq;
}

private List<Cmd> RewriteLsetEmpty(CallCmd callCmd)
{
GetRelevantInfo(callCmd, out Type type, out Type refType, out Function lheapConstructor,
Expand Down Expand Up @@ -510,7 +538,7 @@ private void GetRelevantInfo(CallCmd callCmd, out Type type, out Type refType, o
{
var instantiation = monomorphizer.GetTypeInstantiation(callCmd.Proc);
type = instantiation["V"];
var actualTypeParams = new List<Type>() { instantiation["V"] };
var actualTypeParams = new List<Type>() { type };
var refTypeCtorDecl = monomorphizer.InstantiateTypeCtorDecl("Ref", actualTypeParams);
refType = new CtorType(Token.NoToken, refTypeCtorDecl, new List<Type>());
var lheapTypeCtorDecl = (DatatypeTypeCtorDecl)monomorphizer.InstantiateTypeCtorDecl("Lheap", actualTypeParams);
Expand All @@ -521,6 +549,16 @@ private void GetRelevantInfo(CallCmd callCmd, out Type type, out Type refType, o
lvalConstructor = lvalTypeCtorDecl.Constructors[0];
}

private void GetRelevantInfo(CallCmd callCmd, out Type keyType, out Type valType, out Function lmapConstructor)
{
var instantiation = monomorphizer.GetTypeInstantiation(callCmd.Proc);
keyType = instantiation["K"];
valType = instantiation["V"];
var actualTypeParams = new List<Type>() { keyType, valType };
var lmapTypeCtorDecl = (DatatypeTypeCtorDecl)monomorphizer.InstantiateTypeCtorDecl("Lmap", actualTypeParams);
lmapConstructor = lmapTypeCtorDecl.Constructors[0];
}

private void ResolveAndTypecheck(CoreOptions options, IEnumerable<Absy> absys)
{
var rc = new ResolutionContext(null, options);
Expand All @@ -535,4 +573,49 @@ private void ResolveAndTypecheck(CoreOptions options, IEnumerable<Absy> absys)
absys.ForEach(absy => absy.Typecheck(tc));
tc.CheckModifies = oldCheckModifies;
}

private List<Cmd> CreateAccessAsserts(Expr expr, IToken tok, string msg)
{
if (expr is NAryExpr nAryExpr)
{
if (nAryExpr.Fun is FieldAccess)
{
return CreateAccessAsserts(nAryExpr.Args[0], tok, msg);
}
if (nAryExpr.Fun is MapSelect)
{
var mapExpr = nAryExpr.Args[0];
if (mapExpr is NAryExpr lheapValExpr &&
lheapValExpr.Fun is FieldAccess &&
lheapValExpr.Args[0].Type is CtorType ctorType &&
Monomorphizer.GetOriginalDecl(ctorType.Decl).Name == "Lheap")
{
var cmdSeq = CreateAccessAsserts(lheapValExpr.Args[0], tok, msg);
var lheapContainsFunc = LheapContains(nAryExpr.Type);
cmdSeq.Add(AssertCmd(tok, ExprHelper.FunctionCall(lheapContainsFunc, lheapValExpr.Args[0], nAryExpr.Args[1]), msg));
return cmdSeq;
}
}
}
return new List<Cmd>();
}

private List<Cmd> CreateAccessAsserts(AssignLhs assignLhs, IToken tok, string msg)
{
if (assignLhs is FieldAssignLhs fieldAssignLhs)
{
return CreateAccessAsserts(fieldAssignLhs.Datatype, tok, msg);
}
if (assignLhs is MapAssignLhs mapAssignLhs &&
mapAssignLhs.Map is FieldAssignLhs fieldAssignLhs1 &&
fieldAssignLhs1.Datatype.Type is CtorType ctorType &&
Monomorphizer.GetOriginalDecl(ctorType.Decl).Name == "Lheap")
{
var cmdSeq = CreateAccessAsserts(mapAssignLhs.Map, tok, msg);
var lheapContainsFunc = LheapContains(mapAssignLhs.Map.Type);
cmdSeq.Add(AssertCmd(tok, ExprHelper.FunctionCall(lheapContainsFunc, fieldAssignLhs1.Datatype.AsExpr, mapAssignLhs.Indexes[0]), msg));
return cmdSeq;
}
return new List<Cmd>();
}
}
39 changes: 33 additions & 6 deletions Source/Concurrency/LinearTypeChecker.cs
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
using System.Collections.Generic;
using System;
using System.Collections.Generic;
using System.Linq;

namespace Microsoft.Boogie
Expand Down Expand Up @@ -929,20 +930,46 @@ public Expr DisjointnessExprForPermissions(LinearDomain domain, IEnumerable<Expr
return expr;
}

public IEnumerable<Expr> LheapWellFormedExpressions(IEnumerable<Variable> availableVars)
private Function LheapWellFormedFunction(Monomorphizer monomorphizer, TypeCtorDecl typeCtorDecl)
{
var typeInstantiation = monomorphizer.GetTypeInstantiation(typeCtorDecl);
var typeParamInstantiationMap = new Dictionary<string, Type>() { { "V", typeInstantiation[0] } };
return monomorphizer.InstantiateFunction("Lheap_WellFormed", typeParamInstantiationMap);
}

private Function LmapWellFormedFunction(Monomorphizer monomorphizer, TypeCtorDecl typeCtorDecl)
{
var typeInstantiation = monomorphizer.GetTypeInstantiation(typeCtorDecl);
var typeParamInstantiationMap = new Dictionary<string, Type>() { { "K", typeInstantiation[0] }, { "V", typeInstantiation[1] } };
return monomorphizer.InstantiateFunction("Lmap_WellFormed", typeParamInstantiationMap);
}

public IEnumerable<Expr> LstoreWellFormedExpressions(IEnumerable<Variable> availableVars)
{
var monomorphizer = civlTypeChecker.program.monomorphizer;
if (monomorphizer == null)
{
return Enumerable.Empty<Expr>();
}
return availableVars.Where(v =>
v.TypedIdent.Type is CtorType ctorType && Monomorphizer.GetOriginalDecl(ctorType.Decl).Name == "Lheap").Select(
v =>
{
if (v.TypedIdent.Type is not CtorType ctorType)
{
return false;
}
var declName = Monomorphizer.GetOriginalDecl(ctorType.Decl).Name;
if (declName is "Lheap" or "Lmap")
{
return true;
}
return false;
}).Select(v =>
{
var ctorType = (CtorType)v.TypedIdent.Type;
var func = monomorphizer.InstantiateFunction("Lheap_WellFormed",
new Dictionary<string, Type>() { { "V", monomorphizer.GetTypeInstantiation(ctorType.Decl)[0] } });
var declName = Monomorphizer.GetOriginalDecl(ctorType.Decl).Name;
var func = declName == "Lheap"
? LheapWellFormedFunction(monomorphizer, ctorType.Decl)
: LmapWellFormedFunction(monomorphizer, ctorType.Decl);
return ExprHelper.FunctionCall(func, Expr.Ident(v));
});
}
Expand Down
2 changes: 1 addition & 1 deletion Source/Concurrency/MoverCheck.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -88,7 +88,7 @@ private IEnumerable<Requires> DisjointnessAndWellFormedRequires(IEnumerable<Vari
{
var availableVars = paramVars.Union(frame);
return civlTypeChecker.linearTypeChecker.DisjointnessExprForEachDomain(availableVars)
.Union(civlTypeChecker.linearTypeChecker.LheapWellFormedExpressions(availableVars))
.Union(civlTypeChecker.linearTypeChecker.LstoreWellFormedExpressions(availableVars))
.Select(expr => new Requires(false, expr));
}

Expand Down
Loading

0 comments on commit 22fcb97

Please sign in to comment.