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

[don't merge] implement shared as references/pointers #47

Open
wants to merge 8 commits into
base: betr
Choose a base branch
from
Open

[don't merge] implement shared as references/pointers #47

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
44658d7
compile `shared` to references / pointers
tjhance Sep 13, 2021
ce21a49
fix pointer usage a bit
tjhance Sep 14, 2021
f726764
add more test cases
tjhance Sep 14, 2021
d1cdce4
Merge branch 'betr' into shared-refs
tjhance Sep 14, 2021
61603df
Merge branch 'betr' into shared-refs
tjhance Oct 8, 2021
7159b1f
Merge branch 'betr' into shared-refs
tjhance Oct 18, 2021
3d2f853
Merge branch 'betr' into shared-refs
tjhance Oct 18, 2021
64f91c5
fix c++ compile error relating to linear seq
tjhance Oct 19, 2021
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
12 changes: 6 additions & 6 deletions Source/Dafny/Compiler-Csharp.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1371,7 +1371,7 @@ protected override bool DeclareFormal(string prefix, string name, Type type, Bpl
return true;
}

protected override void DeclareLocalVar(string name, Type/*?*/ type, Bpl.IToken/*?*/ tok, Usage usage, bool leaveRoomForRhs, string/*?*/ rhs, TargetWriter wr) {
protected override void DeclareLocalVar(string name, Type/*?*/ type, Bpl.IToken/*?*/ tok, Usage usage, bool leaveRoomForRhs, string/*?*/ rhs, TargetWriter wr, bool as_pointer_for_shared) {
wr.Write("{0} {1}", type != null ? TypeName(type, wr, tok) : "var", name);
if (leaveRoomForRhs) {
Contract.Assert(rhs == null); // follows from precondition
Expand All @@ -1382,7 +1382,7 @@ protected override void DeclareLocalVar(string name, Type/*?*/ type, Bpl.IToken/
}
}

protected override TargetWriter DeclareLocalVar(string name, Type/*?*/ type, Bpl.IToken/*?*/ tok, Usage usage, TargetWriter wr) {
protected override TargetWriter DeclareLocalVar(string name, Type/*?*/ type, Bpl.IToken/*?*/ tok, Usage usage, TargetWriter wr, bool asPointerForShared) {
wr.Write("{0} {1} = ", type != null ? TypeName(type, wr, tok) : "var", name);
var w = wr.Fork();
wr.WriteLine(";");
Expand All @@ -1395,7 +1395,7 @@ protected override void DeclareOutCollector(string collectorVarName, TargetWrite

protected override void DeclareLocalOutVar(string name, Type type, Bpl.IToken tok, Usage usage, string rhs, bool useReturnStyleOuts, TargetWriter wr) {
if (useReturnStyleOuts) {
DeclareLocalVar(name, type, tok, usage, false, rhs, wr);
DeclareLocalVar(name, type, tok, usage, false, rhs, wr, false);
} else {
EmitAssignment(name, type, rhs, null, wr);
}
Expand Down Expand Up @@ -2248,7 +2248,7 @@ private void EmitSeqConstructionExprFromLambda(Expression lengthExpr, BoundVar b

var indexType = lengthExpr.Type;
var lengthVar = FreshId("dim");
DeclareLocalVar(lengthVar, indexType, lengthExpr.tok, boundVar.Usage, lengthExpr, inLetExprBody, wrLamBody);
DeclareLocalVar(lengthVar, indexType, lengthExpr.tok, boundVar.Usage, lengthExpr, inLetExprBody, wrLamBody, false);
var arrVar = FreshId("arr");
wrLamBody.Write("var {0} = ", arrVar);
var wrDims = EmitNewArray(body.Type, body.tok, dimCount: 1, mustInitialize: false, wr: wrLamBody);
Expand Down Expand Up @@ -2699,12 +2699,12 @@ protected override void EmitMapDisplay(MapType mt, Bpl.IToken tok, List<Expressi
}

protected override void EmitSetBuilder_New(TargetWriter wr, SetComprehension e, string collectionName) {
var wrVarInit = DeclareLocalVar(collectionName, null, null, Usage.Ordinary, wr);
var wrVarInit = DeclareLocalVar(collectionName, null, null, Usage.Ordinary, wr, false);
wrVarInit.Write("new System.Collections.Generic.List<{0}>()", TypeName(e.Type.AsSetType.Arg, wrVarInit, e.tok));
}

protected override void EmitMapBuilder_New(TargetWriter wr, MapComprehension e, string collectionName) {
var wrVarInit = DeclareLocalVar(collectionName, null, null, Usage.Ordinary, wr);
var wrVarInit = DeclareLocalVar(collectionName, null, null, Usage.Ordinary, wr, false);
var mt = e.Type.AsMapType;
var domtypeName = TypeName(mt.Domain, wrVarInit, e.tok);
var rantypeName = TypeName(mt.Range, wrVarInit, e.tok);
Expand Down
51 changes: 39 additions & 12 deletions Source/Dafny/Compiler-cpp.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -167,7 +167,22 @@ private string InstantiateTemplate(List<Type> typeArgs) {
if (typeArgs != null) {
var targs = "";
if (typeArgs.Count > 0) {
targs = String.Format("<{0}>", Util.Comma(typeArgs, ta => TypeName(ta, null, null)));
targs = String.Format("<{0}>", Util.Comma(typeArgs, ty => TypeName(ty, null, null)));
}

return targs;
} else {
return "";
}
}

private string InstantiateTemplateFormals(List<Formal> typeArgs) {
if (typeArgs != null) {
var targs = "";
if (typeArgs.Count > 0) {
targs = String.Format("<{0}>", Util.Comma(typeArgs, ta =>
TypeName(ta.Type, null, null, null, false, ta.Usage) + (ta.Usage == Usage.Shared ? "*" : "")
));
}

return targs;
Expand Down Expand Up @@ -727,8 +742,12 @@ public void Finish() { }
string targetReturnTypeReplacement = null;
if (nonGhostOuts.Count == 1) {
targetReturnTypeReplacement = TypeName(nonGhostOuts[0].Type, wr, nonGhostOuts[0].tok, usage:nonGhostOuts[0].Usage);
if (nonGhostOuts[0].Usage == Usage.Shared)
{
targetReturnTypeReplacement += "*";
}
} else if (nonGhostOuts.Count > 1) {
targetReturnTypeReplacement = String.Format("struct Tuple{0}", InstantiateTemplate(nonGhostOuts.ConvertAll(n => n.Type)));
targetReturnTypeReplacement = String.Format("struct Tuple{0}", InstantiateTemplateFormals(nonGhostOuts));
}

if (!createBody) {
Expand Down Expand Up @@ -803,12 +822,13 @@ public void Finish() { }
wr.WriteLine(DeclareTemplate(classArgs));
}

var typeName = TypeName(resultType, wr, tok, usage: resultUsage) + (resultUsage == Usage.Shared ? "*" : "");
wdr.Write("{0}{1} {2}",
isStatic ? "static " : "",
TypeName(resultType, wr, tok, usage:resultUsage),
typeName,
name);
wr.Write("{0} {1}{2}::{3}",
TypeName(resultType, wr, tok, usage:resultUsage),
typeName,
className,
InstantiateTemplate(classArgs),
name);
Expand Down Expand Up @@ -982,6 +1002,10 @@ protected override string TypeName(Type type, TextWriter wr, Bpl.IToken tok, Mem
}

protected override string TypeInitializationValue(Type type, TextWriter wr, Bpl.IToken tok, Usage usage, bool usePlaceboValue, bool constructTypeParameterDefaultsFromTypeDescriptors) {
if (usage == Usage.Shared)
{
return "nullptr";
}
var xType = type.NormalizeExpandKeepConstraints();
if (xType is BoolType) {
return "false";
Expand Down Expand Up @@ -1179,11 +1203,13 @@ private string DeclareFormals(List<Formal> formals) {
return ret;
}

protected override void DeclareLocalVar(string name, Type/*?*/ type, Bpl.IToken/*?*/ tok, Usage usage, bool leaveRoomForRhs, string/*?*/ rhs, TargetWriter wr) {
protected override void DeclareLocalVar(string name, Type/*?*/ type, Bpl.IToken/*?*/ tok, Usage usage, bool leaveRoomForRhs, string/*?*/ rhs, TargetWriter wr, bool as_pointer_for_shared)
{
bool is_shared = usage == Usage.Shared;
if (type != null) {
wr.Write("{0} ", TypeName(type, wr, tok, usage:usage));
wr.Write(is_shared ? (as_pointer_for_shared ? "{0}* " : "{0}& ") : "{0} ", TypeName(type, wr, tok, usage:usage));
} else {
wr.Write("auto ");
wr.Write(is_shared ? (as_pointer_for_shared ? "auto* " : "auto& ") : "auto ");
}
wr.Write("{0}", name);
if (leaveRoomForRhs) {
Expand All @@ -1195,11 +1221,12 @@ protected override void DeclareLocalVar(string name, Type/*?*/ type, Bpl.IToken/
}
}

protected override TargetWriter DeclareLocalVar(string name, Type/*?*/ type, Bpl.IToken/*?*/ tok, Usage usage, TargetWriter wr) {
protected override TargetWriter DeclareLocalVar(string name, Type/*?*/ type, Bpl.IToken/*?*/ tok, Usage usage, TargetWriter wr, bool as_pointer_for_shared = false) {
bool is_shared = usage == Usage.Shared;
if (type != null) {
wr.Write("{0} ", TypeName(type, wr, tok, usage:usage));
wr.Write(is_shared ? (as_pointer_for_shared ? "{0}* " : "{0}& ") : "{0} ", TypeName(type, wr, tok, usage:usage));
} else {
wr.Write("auto ");
wr.Write(is_shared ? (as_pointer_for_shared ? "{0}* " : "{0}& ") : "auto ");
}
wr.Write("{0} = ", name);
var w = wr.Fork();
Expand All @@ -1214,7 +1241,7 @@ protected override void DeclareOutCollector(string collectorVarName, TargetWrite
}

protected override void DeclareLocalOutVar(string name, Type type, Bpl.IToken tok, Usage usage, string rhs, bool useReturnStyleOuts, TargetWriter wr) {
DeclareLocalVar(name, type, tok, usage, false, rhs, wr);
DeclareLocalVar(name, type, tok, usage, false, rhs, wr, true);
}

protected override void EmitOutParameterSplits(string outCollector, List<string> actualOutParamNames, TargetWriter wr) {
Expand Down Expand Up @@ -1270,7 +1297,7 @@ protected override void EmitReturn(List<Formal> outParams, TargetWriter wr) {
} else if (outParams.Count == 1) {
wr.WriteLine("return {0};", IdName(outParams[0]));
} else {
wr.WriteLine("return Tuple{0}({1});", InstantiateTemplate(outParams.ConvertAll(o => o.Type)), Util.Comma(outParams, IdName));
wr.WriteLine("return Tuple{0}({1});", InstantiateTemplateFormals(outParams), Util.Comma(outParams, IdName));
}
}

Expand Down
18 changes: 9 additions & 9 deletions Source/Dafny/Compiler-go.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1112,7 +1112,7 @@ private BlockTargetWriter CreateSubroutine(string name, List<TypeArgumentInstant
if (!instantiatedType.Equals(p.Type)) {
// var p instantiatedType = p.(instantiatedType)
var pName = IdName(inParams[i]);
DeclareLocalVar(pName, instantiatedType, p.tok, Usage.Ordinary, true, null, w);
DeclareLocalVar(pName, instantiatedType, p.tok, Usage.Ordinary, true, null, w, false);
var wRhs = EmitAssignmentRhs(w);
wRhs = EmitCoercionIfNecessary(p.Type, instantiatedType, p.tok, wRhs);
wRhs.Write(pName);
Expand Down Expand Up @@ -1677,14 +1677,14 @@ void EmitDummyVariableUse(string variableName, TargetWriter wr) {
wr.WriteLine("_ = {0}", variableName);
}

protected override void DeclareLocalVar(string name, Type type, Bpl.IToken tok, Usage usage, bool leaveRoomForRhs, string rhs, TargetWriter wr) {
protected override void DeclareLocalVar(string name, Type type, Bpl.IToken tok, Usage usage, bool leaveRoomForRhs, string rhs, TargetWriter wr, bool asPointerForShared) {
var w = DeclareLocalVar(name, type, tok, usage, includeRhs:(rhs != null || leaveRoomForRhs), leaveRoomForRhs:leaveRoomForRhs, wr:wr);
if (rhs != null) {
w.Write(rhs);
}
}

protected override TargetWriter DeclareLocalVar(string name, Type/*?*/ type, Bpl.IToken/*?*/ tok, Usage usage, TargetWriter wr) {
protected override TargetWriter DeclareLocalVar(string name, Type/*?*/ type, Bpl.IToken/*?*/ tok, Usage usage, TargetWriter wr, bool asPointerForShared) {
return DeclareLocalVar(name, type, tok, usage, includeRhs:true, leaveRoomForRhs:false, wr:wr);
}

Expand All @@ -1695,7 +1695,7 @@ protected override TargetWriter DeclareLocalVar(string name, Type/*?*/ type, Bpl
protected override string StmtTerminator => "";

protected override void DeclareLocalOutVar(string name, Type type, Bpl.IToken tok, Usage usage, string rhs, bool useReturnStyleOuts, TargetWriter wr) {
DeclareLocalVar(name, type, tok, usage, false, rhs, wr);
DeclareLocalVar(name, type, tok, usage, false, rhs, wr, false);
}

protected override void EmitActualTypeArgs(List<Type> typeArgs, Bpl.IToken tok, TextWriter wr) {
Expand Down Expand Up @@ -1741,8 +1741,8 @@ protected override void EmitReturn(List<Formal> outParams, TargetWriter wr) {
EmitReturnWithCoercions(outParams, null, null, wr);
}

protected override void EmitReturnExpr(Expression expr, Type resultType, bool inLetExprBody, TargetWriter wr) {
var w = EmitReturnExpr(wr);
protected override void EmitReturnExpr(Expression expr, Type resultType, bool inLetExprBody, TargetWriter wr, bool pointer) {
var w = EmitReturnExpr(wr, pointer);
var fromType = thisContext == null ? expr.Type : Resolver.SubstType(expr.Type, thisContext.ParentFormalTypeParametersToActuals);
w = EmitCoercionIfNecessary(fromType, resultType, expr.tok, w);
TrExpr(expr, w, inLetExprBody);
Expand Down Expand Up @@ -2686,7 +2686,7 @@ protected override TargetWriter EmitBetaRedex(List<string> boundVars, List<Expre

wr.Write(") {0}", TypeName(type, wr, tok));
var wLambdaBody = wr.NewBigExprBlock("", ")");
var w = EmitReturnExpr(wLambdaBody);
var w = EmitReturnExpr(wLambdaBody, false);
TrExprList(arguments, wr, inLetExprBody);
return w;
}
Expand Down Expand Up @@ -3300,12 +3300,12 @@ protected override void EmitMapDisplay(MapType mt, Bpl.IToken tok, List<Expressi
}

protected override void EmitSetBuilder_New(TargetWriter wr, SetComprehension e, string collectionName) {
var wrVarInit = DeclareLocalVar(collectionName, null, null, Usage.Ordinary, wr);
var wrVarInit = DeclareLocalVar(collectionName, null, null, Usage.Ordinary, wr, false);
wrVarInit.Write("_dafny.NewBuilder()");
}

protected override void EmitMapBuilder_New(TargetWriter wr, MapComprehension e, string collectionName) {
var wrVarInit = DeclareLocalVar(collectionName, null, null, Usage.Ordinary, wr);
var wrVarInit = DeclareLocalVar(collectionName, null, null, Usage.Ordinary, wr, false);
wrVarInit.Write("_dafny.NewMapBuilder()");
}

Expand Down
14 changes: 7 additions & 7 deletions Source/Dafny/Compiler-java.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -439,11 +439,11 @@ protected BlockTargetWriter CreateGetter(string name, Type resultType, Bpl.IToke
}

protected override void DeclareLocalVar(string name, Type /*?*/ type, Bpl.IToken /*?*/ tok, Usage usage, Expression rhs,
bool inLetExprBody, TargetWriter wr){
bool inLetExprBody, TargetWriter wr, bool asPointerForShared){
if (type == null){
type = rhs.Type;
}
var w = DeclareLocalVar(name, type, tok, usage, wr);
var w = DeclareLocalVar(name, type, tok, usage, wr, asPointerForShared);
TrExpr(rhs, w, inLetExprBody);
}

Expand Down Expand Up @@ -1104,7 +1104,7 @@ thisContext is NewtypeDecl ||
}

protected override void DeclareLocalVar(string name, Type /*?*/ type, Bpl.IToken /*?*/ tok, Usage usage, bool leaveRoomForRhs,
string /*?*/ rhs, TargetWriter wr){
string /*?*/ rhs, TargetWriter wr, bool asPointerForShared){
if (type != null && type.AsArrayType != null){
arrays.Add(type.AsArrayType.Dims);
}
Expand All @@ -1127,8 +1127,8 @@ protected override void DeclareLocalVar(string name, Type /*?*/ type, Bpl.IToken
}

protected override void DeclareLocalVar(string name, Type /*?*/ type, Bpl.IToken /*?*/ tok, Usage usage, bool leaveRoomForRhs,
string /*?*/ rhs, TargetWriter wr, Type t) {
DeclareLocalVar(name, t, tok, usage, leaveRoomForRhs, rhs, wr);
string /*?*/ rhs, TargetWriter wr, Type t, bool asPointerForShared) {
DeclareLocalVar(name, t, tok, usage, leaveRoomForRhs, rhs, wr, asPointerForShared);
}

protected override void EmitCollectionDisplay(CollectionType ct, Bpl.IToken tok, List<Expression> elements, bool inLetExprBody, TargetWriter wr) {
Expand Down Expand Up @@ -3091,15 +3091,15 @@ protected override string TypeInitializationValue(Type type, TextWriter wr, Bpl.
}
}

protected override TargetWriter DeclareLocalVar(string name, Type type, Bpl.IToken tok, Usage usage, TargetWriter wr) {
protected override TargetWriter DeclareLocalVar(string name, Type type, Bpl.IToken tok, Usage usage, TargetWriter wr, bool asPointerForShared) {
wr.Write("{0} {1} = ", type != null ? TypeName(type, wr, tok, false, false, null) : "var", name);
var w = wr.Fork();
wr.WriteLine(";");
return w;
}

protected override void DeclareLocalOutVar(string name, Type type, Bpl.IToken tok, Usage usage, string rhs, bool useReturnStyleOuts, TargetWriter wr) {
DeclareLocalVar(name, type, tok, usage, false, rhs, wr);
DeclareLocalVar(name, type, tok, usage, false, rhs, wr, false);
}

protected override IClassWriter CreateTrait(string name, bool isExtern, List<TypeParameter>/*?*/ typeParameters, List<Type> superClasses, Bpl.IToken tok, TargetWriter wr) {
Expand Down
16 changes: 8 additions & 8 deletions Source/Dafny/Compiler-js.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -440,12 +440,12 @@ protected override BlockTargetWriter CreateIterator(IteratorDecl iter, TargetWri
// equals method
using (var w = wr.NewBlock("equals(other)")) {
using (var thn = EmitIf("this === other", true, w)) {
EmitReturnExpr("true", thn);
EmitReturnExpr("true", thn, false);
}
i = 0;
foreach (var ctor in dt.Ctors) {
var thn = EmitIf(string.Format("this.$tag === {0}", i), true, w);
var guard = EmitReturnExpr(thn);
var guard = EmitReturnExpr(thn, false);
guard.Write("other.$tag === {0}", i);
var k = 0;
foreach (Formal arg in ctor.Formals) {
Expand Down Expand Up @@ -971,7 +971,7 @@ protected override string TypeName_Companion(Type type, TextWriter wr, Bpl.IToke
protected void DeclareField(string name, bool isStatic, bool isConst, Type type, Bpl.IToken tok, string rhs, TargetWriter wr) {
if (isStatic) {
var w = wr.NewNamedBlock("static get {0}()", name);
EmitReturnExpr(rhs, w);
EmitReturnExpr(rhs, w, false);
} else {
wr.WriteLine("this.{0} = {1};", name, rhs);
}
Expand All @@ -986,7 +986,7 @@ protected override bool DeclareFormal(string prefix, string name, Type type, Bpl
}
}

protected override void DeclareLocalVar(string name, Type/*?*/ type, Bpl.IToken/*?*/ tok, Usage usage, bool leaveRoomForRhs, string/*?*/ rhs, TargetWriter wr) {
protected override void DeclareLocalVar(string name, Type/*?*/ type, Bpl.IToken/*?*/ tok, Usage usage, bool leaveRoomForRhs, string/*?*/ rhs, TargetWriter wr, bool asPointerForShared) {
wr.Write("let {0}", name);
if (leaveRoomForRhs) {
Contract.Assert(rhs == null); // follows from precondition
Expand All @@ -997,7 +997,7 @@ protected override void DeclareLocalVar(string name, Type/*?*/ type, Bpl.IToken/
}
}

protected override TargetWriter DeclareLocalVar(string name, Type/*?*/ type, Bpl.IToken/*?*/ tok, Usage usage, TargetWriter wr) {
protected override TargetWriter DeclareLocalVar(string name, Type/*?*/ type, Bpl.IToken/*?*/ tok, Usage usage, TargetWriter wr, bool asPointerForShared) {
wr.Write("let {0} = ", name);
var w = wr.Fork();
wr.WriteLine(";");
Expand All @@ -1011,7 +1011,7 @@ protected override void DeclareOutCollector(string collectorVarName, TargetWrite
}

protected override void DeclareLocalOutVar(string name, Type type, Bpl.IToken tok, Usage usage, string rhs, bool useReturnStyleOuts, TargetWriter wr) {
DeclareLocalVar(name, type, tok, usage, false, rhs, wr);
DeclareLocalVar(name, type, tok, usage, false, rhs, wr, false);
}

protected override void EmitOutParameterSplits(string outCollector, List<string> actualOutParamNames, TargetWriter wr) {
Expand Down Expand Up @@ -2212,12 +2212,12 @@ protected override void EmitMapDisplay(MapType mt, Bpl.IToken tok, List<Expressi
}

protected override void EmitSetBuilder_New(TargetWriter wr, SetComprehension e, string collectionName) {
var wrVarInit = DeclareLocalVar(collectionName, null, null, Usage.Ordinary, wr);
var wrVarInit = DeclareLocalVar(collectionName, null, null, Usage.Ordinary, wr, false);
wrVarInit.Write($"new {DafnySetClass}()");
}

protected override void EmitMapBuilder_New(TargetWriter wr, MapComprehension e, string collectionName) {
var wrVarInit = DeclareLocalVar(collectionName, null, null, Usage.Ordinary, wr);
var wrVarInit = DeclareLocalVar(collectionName, null, null, Usage.Ordinary, wr, false);
wrVarInit.Write($"new {DafnyMapClass}()");
}

Expand Down
Loading