Skip to content

Commit

Permalink
Merge branch 'master' into triggers-for-such-that
Browse files Browse the repository at this point in the history 
# Conflicts:
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny0/BitvectorResolution.dfy.expect
#	Source/IntegrationTests/TestFiles/LitTests/LitTest/dafny4/Bug170.dfy.expect
  • Loading branch information
@RustanLeino
RustanLeino committed Jan 14, 2025
2 parents ed934a9 + 0fcac3a commit 585aef2
Show file tree
Hide file tree
Showing 193 changed files with 1,062 additions and 784 deletions.
5 changes: 5 additions & 0 deletions .github/workflows/integration-tests-reusable.yml
View file
Original file line number Diff line number Diff line change
Expand Up @@ -72,6 +72,11 @@ jobs:
uses: actions/setup-dotnet@v4
with:
dotnet-version: ${{ env.dotnet-version }}
# Setup dotnet 6.0 for running Boogie. Alternatively we could try running Boogie with a roll forward policy, or updating Boogie.
- name: Setup dotnet
uses: actions/setup-dotnet@v4
with:
dotnet-version: 6.0.x
- name: C++ for ubuntu 20.04
if: matrix.os == 'ubuntu-20.04'
run: |
Expand Down
2 changes: 1 addition & 1 deletion README.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@ A reference manual is available both [online](https://dafny-lang.github.io/dafny

## Community

You can ask questions about Dafny on [Stack Overflow](https://stackoverflow.com/questions/tagged/dafny) or participate in general discussion on Dafny's [![Gitter](https://badges.gitter.im/dafny-lang/community.svg)](https://gitter.im/dafny-lang/community?utm_source=badge&utm_medium=badge&utm_campaign=pr-badge).
Feel free to report issues here on GitHub or to ask for questions on our :speech_balloon: [Zulip](https://dafny.zulipchat.com/) channel.

## Try Dafny

Expand Down
1 change: 0 additions & 1 deletion Scripts/package.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -161,7 +161,6 @@ def build(self):
if path.exists(self.buildDirectory):
shutil.rmtree(self.buildDirectory)
run(["make", "--quiet", "clean"])
self.run_publish("DafnyLanguageServer")
self.run_publish("DafnyServer")
self.run_publish("DafnyRuntime", "netstandard2.0")
self.run_publish("DafnyRuntime", "net452")
Expand Down
6 changes: 6 additions & 0 deletions Source/Dafny.sln
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,8 @@ Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyDriver.Test", "DafnyDr
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "DafnyCore.Test", "DafnyCore.Test\DafnyCore.Test.csproj", "{33C29F26-A27B-474D-B436-83EA615B09FC}"
EndProject
Project("{FAE04EC0-301F-11D3-BF4B-00C04F79EFBC}") = "Scripts", "Scripts\Scripts.csproj", "{3FAB051A-1745-497B-B4C0-D49194BB5D32}"
EndProject
EndProject
Global
GlobalSection(SolutionConfigurationPlatforms) = preSolution
Expand Down Expand Up @@ -130,6 +132,10 @@ Global
{96B8ADA8-6190-49F7-8C38-CDA60DC92293}.Debug|Any CPU.Build.0 = Debug|Any CPU
{96B8ADA8-6190-49F7-8C38-CDA60DC92293}.Release|Any CPU.ActiveCfg = Release|Any CPU
{96B8ADA8-6190-49F7-8C38-CDA60DC92293}.Release|Any CPU.Build.0 = Release|Any CPU
{3FAB051A-1745-497B-B4C0-D49194BB5D32}.Debug|Any CPU.ActiveCfg = Debug|Any CPU
{3FAB051A-1745-497B-B4C0-D49194BB5D32}.Debug|Any CPU.Build.0 = Debug|Any CPU
{3FAB051A-1745-497B-B4C0-D49194BB5D32}.Release|Any CPU.ActiveCfg = Release|Any CPU
{3FAB051A-1745-497B-B4C0-D49194BB5D32}.Release|Any CPU.Build.0 = Release|Any CPU
EndGlobalSection
GlobalSection(SolutionProperties) = preSolution
HideSolutionNode = FALSE
Expand Down
49 changes: 36 additions & 13 deletions Source/DafnyCore/Backends/CSharp/CsharpCodeGenerator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -265,15 +265,27 @@ protected override ConcreteSyntaxTree CreateStaticMain(IClassWriter cw, string a
return wr.NewBlock($"public static void _StaticMain(Dafny.ISequence<Dafny.ISequence<{CharTypeName}>> {argsParameterName})");
}

/// <summary>
/// Compute the name of the class to use to translate a data-type or a class
/// </summary>
private string protectedTypeName(TopLevelDecl dt) {
var protectedName = IdName(dt);
if (dt.EnclosingModuleDefinition is { Name: var moduleName } && moduleName == protectedName) {
return $"_{protectedName}";
}
return protectedName;
}

string IdProtectModule(string moduleName) {
Contract.Requires(moduleName != null);
return string.Join(".", moduleName.Split(".").Select(IdProtect));
}

protected override ConcreteSyntaxTree CreateModule(ModuleDefinition module, string moduleName, bool isDefault,
ModuleDefinition externModule,
string libraryName /*?*/, Attributes moduleAttributes, ConcreteSyntaxTree wr) {
moduleName = IdProtectModule(moduleName);
return wr.NewBlock($"namespace {moduleName}", " // end of " + $"namespace {moduleName}");
var protectedModuleName = IdProtectModule(moduleName);
return wr.NewBlock($"namespace {protectedModuleName}", " // end of " + $"namespace {protectedModuleName}");
}

protected override string GetHelperModuleName() => DafnyHelpersClass;
Expand Down Expand Up @@ -305,8 +317,9 @@ string PrintVariance(TypeParameter.TPVariance variance) {
return $"<{targs.Comma(PrintTypeParameter)}>";
}

protected override IClassWriter CreateClass(string moduleName, string name, bool isExtern, string /*?*/ fullPrintName,
protected override IClassWriter CreateClass(string moduleName, bool isExtern, string /*?*/ fullPrintName,
List<TypeParameter> typeParameters, TopLevelDecl cls, List<Type>/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) {
var name = protectedTypeName(cls);
var wBody = WriteTypeHeader("partial class", name, typeParameters, superClasses, tok, wr);

ConcreteSyntaxTree/*?*/ wCtorBody = null;
Expand Down Expand Up @@ -442,7 +455,7 @@ protected override ConcreteSyntaxTree CreateIterator(IteratorDecl iter, Concrete
// }
// }

var cw = (ClassWriter)CreateClass(IdProtect(iter.EnclosingModuleDefinition.GetCompileName(Options)), IdName(iter), iter, wr);
var cw = (ClassWriter)CreateClass(IdProtect(iter.EnclosingModuleDefinition.GetCompileName(Options)), iter, wr);
var w = cw.InstanceMemberWriter;
// here come the fields

Expand Down Expand Up @@ -559,7 +572,7 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
// }
var nonGhostTypeArgs = SelectNonGhost(dt, dt.TypeArgs);
var DtT_TypeArgs = TypeParameters(nonGhostTypeArgs);
var DtT_protected = IdName(dt) + DtT_TypeArgs;
var DtT_protected = protectedTypeName(dt) + DtT_TypeArgs;
var simplifiedType = DatatypeWrapperEraser.SimplifyType(Options, UserDefinedType.FromTopLevelDecl(dt.Origin, dt));
var simplifiedTypeName = TypeName(simplifiedType, wr, dt.Origin);

Expand All @@ -581,7 +594,7 @@ IClassWriter CompileDatatypeBase(DatatypeDecl dt, ConcreteSyntaxTree wr) {
} else {
EmitTypeDescriptorsForClass(dt.TypeArgs, dt, out var wTypeFields, out var wCtorParams, out _, out var wCtorBody);
wr.Append(wTypeFields);
wr.Format($"public {IdName(dt)}({wCtorParams})").NewBlock().Append(wCtorBody);
wr.Format($"public {protectedTypeName(dt)}({wCtorParams})").NewBlock().Append(wCtorBody);
}

var wDefault = new ConcreteSyntaxTree();
Expand Down Expand Up @@ -995,7 +1008,7 @@ private void CompileDatatypeConstructors(DatatypeDecl dt, ConcreteSyntaxTree wrx
// public override _IDt<T> _Get() { if (c != null) { d = c(); c = null; } return d; }
// public override string ToString() { return _Get().ToString(); }
// }
var w = wrx.NewNamedBlock($"public class {dt.GetCompileName(Options)}__Lazy{typeParams} : {IdName(dt)}{typeParams}");
var w = wrx.NewNamedBlock($"public class {dt.GetCompileName(Options)}__Lazy{typeParams} : {protectedTypeName(dt)}{typeParams}");
w.WriteLine($"public {NeedsNew(dt, "Computer")}delegate {DtTypeName(dt)} Computer();");
w.WriteLine($"{NeedsNew(dt, "c")}Computer c;");
w.WriteLine($"{NeedsNew(dt, "d")}{DtTypeName(dt)} d;");
Expand All @@ -1017,7 +1030,7 @@ private void CompileDatatypeConstructors(DatatypeDecl dt, ConcreteSyntaxTree wrx
int constructorIndex = 0; // used to give each constructor a different name
foreach (var ctor in dt.Ctors.Where(ctor => !ctor.IsGhost)) {
var wr = wrx.NewNamedBlock(
$"public class {DtCtorDeclarationName(ctor)}{TypeParameters(nonGhostTypeArgs)} : {IdName(dt)}{typeParams}");
$"public class {DtCtorDeclarationName(ctor)}{TypeParameters(nonGhostTypeArgs)} : {protectedTypeName(dt)}{typeParams}");
DatatypeFieldsAndConstructor(ctor, constructorIndex, wr);
constructorIndex++;
}
Expand Down Expand Up @@ -1191,7 +1204,7 @@ string DtCtorDeclarationName(DatatypeCtor ctor) {
Contract.Ensures(Contract.Result<string>() != null);

var dt = ctor.EnclosingDatatype;
return dt.IsRecordType ? IdName(dt) : dt.GetCompileName(Options) + "_" + ctor.GetCompileName(Options);
return dt.IsRecordType ? protectedTypeName(dt) : dt.GetCompileName(Options) + "_" + ctor.GetCompileName(Options);
}

/// <summary>
Expand All @@ -1217,7 +1230,7 @@ string DtCtorName(DatatypeCtor ctor) {
Contract.Ensures(Contract.Result<string>() != null);

var dt = ctor.EnclosingDatatype;
var dtName = IdName(dt);
var dtName = protectedTypeName(dt);
if (!dt.EnclosingModuleDefinition.TryToAvoidName) {
dtName = IdProtectModule(dt.EnclosingModuleDefinition.GetCompileName(Options)) + "." + dtName;
}
Expand All @@ -1235,7 +1248,7 @@ string DtCreateName(DatatypeCtor ctor) {
}

protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTree wr) {
var cw = (ClassWriter)CreateClass(IdProtect(nt.EnclosingModuleDefinition.GetCompileName(Options)), IdName(nt), nt, wr);
var cw = (ClassWriter)CreateClass(IdProtect(nt.EnclosingModuleDefinition.GetCompileName(Options)), nt, wr);
var w = cw.StaticMemberWriter;
if (nt.NativeType != null) {
var wEnum = w.NewBlock($"public static System.Collections.Generic.IEnumerable<{GetNativeTypeName(nt.NativeType)}> IntegerRange(BigInteger lo, BigInteger hi)");
Expand Down Expand Up @@ -1304,7 +1317,7 @@ void DeclareBoxedNewtype(NewtypeDecl nt, ConcreteSyntaxTree wr) {
}

protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree wr) {
var cw = (ClassWriter)CreateClass(IdProtect(sst.EnclosingModuleDefinition.GetCompileName(Options)), IdName(sst), sst, wr);
var cw = (ClassWriter)CreateClass(IdProtect(sst.EnclosingModuleDefinition.GetCompileName(Options)), sst, wr);
if (sst.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
var sw = new ConcreteSyntaxTree(cw.InstanceMemberWriter.RelativeIndentLevel);
var wStmts = cw.InstanceMemberWriter.Fork();
Expand Down Expand Up @@ -2477,6 +2490,7 @@ public override string PublicIdProtect(string name) {
case "ToString":
case "GetHashCode":
case "Main":
case "Default":
return "_" + name;
default:
return name;
Expand Down Expand Up @@ -2507,13 +2521,22 @@ private string FullTypeName(UserDefinedType udt, MemberDecl/*?*/ member = null,
return (cl.EnclosingModuleDefinition.TryToAvoidName ? "" : IdProtectModule(cl.EnclosingModuleDefinition.GetCompileName(Options)) + ".") + DtTypeName(cl, false);
}

if (cl is DatatypeDecl) {
return (cl.EnclosingModuleDefinition.TryToAvoidName ? "" : IdProtectModule(cl.EnclosingModuleDefinition.GetCompileName(Options)) + ".") + protectedTypeName(cl as DatatypeDecl);
}

if (cl.EnclosingModuleDefinition.TryToAvoidName) {
return IdProtect(cl.GetCompileName(Options));
}

if (cl.IsExtern(Options, out _, out _)) {
return cl.EnclosingModuleDefinition.GetCompileName(Options) + "." + cl.GetCompileName(Options);
}

if (cl is ClassDecl) {
return (cl.EnclosingModuleDefinition.TryToAvoidName ? "" : IdProtectModule(cl.EnclosingModuleDefinition.GetCompileName(Options)) + ".") + protectedTypeName(cl as ClassDecl);
}

return IdProtectModule(cl.EnclosingModuleDefinition.GetCompileName(Options)) + "." + IdProtect(cl.GetCompileName(Options));
}

Expand All @@ -2528,7 +2551,7 @@ protected override void EmitThis(ConcreteSyntaxTree wr, bool callToInheritedMemb

protected override void EmitDatatypeValue(DatatypeValue dtv, string typeDescriptorArguments, string arguments, ConcreteSyntaxTree wr) {
var dt = dtv.Ctor.EnclosingDatatype;
var dtName = IdProtectModule(dt.EnclosingModuleDefinition.GetCompileName(Options)) + "." + IdName(dt);
var dtName = IdProtectModule(dt.EnclosingModuleDefinition.GetCompileName(Options)) + "." + protectedTypeName(dt);

var nonGhostInferredTypeArgs = SelectNonGhost(dt, dtv.InferredTypeArgs);
var typeParams = nonGhostInferredTypeArgs.Count == 0 ? "" : $"<{TypeNames(nonGhostInferredTypeArgs, wr, dtv.Origin)}>";
Expand Down
41 changes: 25 additions & 16 deletions Source/DafnyCore/Backends/Cplusplus/CppCodeGenerator.cs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -149,7 +149,7 @@ protected override void EmitFooter(Program program, ConcreteSyntaxTree wr) {
public override void EmitCallToMain(Method mainMethod, string baseName, ConcreteSyntaxTree wr) {
var w = wr.NewBlock("int main(int argc, char *argv[])");
var tryWr = w.NewBlock("try");
tryWr.WriteLine(string.Format("{0}::{1}::{2}(dafny_get_args(argc, argv));", mainMethod.EnclosingClass.EnclosingModuleDefinition.GetCompileName(Options), mainMethod.EnclosingClass.GetCompileName(Options), mainMethod.Name));
tryWr.WriteLine(string.Format("{0}::{1}::{2}(dafny_get_args(argc, argv));", mainMethod.EnclosingClass.EnclosingModuleDefinition.GetCompileName(Options), clName(mainMethod.EnclosingClass), mainMethod.Name));
var catchWr = w.NewBlock("catch (DafnyHaltException & e)");
catchWr.WriteLine("std::cout << \"Program halted: \" << e.what() << std::endl;");
}
Expand Down Expand Up @@ -226,9 +226,18 @@ private string InstantiateTemplate(List<Type> typeArgs) {

protected override string GetHelperModuleName() => "_dafny";

protected override IClassWriter CreateClass(string moduleName, string name, bool isExtern, string/*?*/ fullPrintName, List<TypeParameter>/*?*/ typeParameters, TopLevelDecl cls, List<Type>/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) {
private string clName(TopLevelDecl cl) {
var className = IdName(cl);
if (cl is ClassDecl || cl is DefaultClassDecl) {
return className;
}
return "class_" + className;
}

protected override IClassWriter CreateClass(string moduleName, bool isExtern, string/*?*/ fullPrintName, List<TypeParameter>/*?*/ typeParameters, TopLevelDecl cls, List<Type>/*?*/ superClasses, IOrigin tok, ConcreteSyntaxTree wr) {
var className = clName(cls);
if (isExtern) {
throw new UnsupportedFeatureException(tok, Feature.ExternalClasses, String.Format("extern in class {0}", name));
throw new UnsupportedFeatureException(tok, Feature.ExternalClasses, String.Format("extern in class {0}", className));
}
if (superClasses != null && superClasses.Any(trait => !trait.IsObject)) {
throw new UnsupportedFeatureException(tok, Feature.Traits);
Expand All @@ -242,17 +251,17 @@ protected override IClassWriter CreateClass(string moduleName, string name, bool
classDefWriter.WriteLine(DeclareTemplate(typeParameters));
}

var methodDeclWriter = classDefWriter.NewBlock(string.Format("class {0}", name), ";");
var methodDeclWriter = classDefWriter.NewBlock(string.Format("class {0}", className), ";");
var methodDefWriter = wr;

classDeclWriter.WriteLine("class {0};", name);
classDeclWriter.WriteLine("class {0};", className);

methodDeclWriter.Write("public:\n");
methodDeclWriter.WriteLine("// Default constructor");
methodDeclWriter.WriteLine("{0}() {{}}", name);
methodDeclWriter.WriteLine("{0}() {{}}", className);

// Create the code for the specialization of get_default
var fullName = moduleName + "::" + name;
var fullName = moduleName + "::" + className;
var getDefaultStr = String.Format("template <{0}>\nstruct get_default<std::shared_ptr<{1}{2} > > {{\n",
TypeParameters(typeParameters),
fullName,
Expand All @@ -266,7 +275,7 @@ protected override IClassWriter CreateClass(string moduleName, string name, bool

var fieldWriter = methodDeclWriter;

return new ClassWriter(name, this, methodDeclWriter, methodDefWriter, fieldWriter, wr);
return new ClassWriter(className, this, methodDeclWriter, methodDefWriter, fieldWriter, wr);
}

protected override bool SupportsProperties { get => false; }
Expand Down Expand Up @@ -615,8 +624,8 @@ protected override IClassWriter DeclareNewtype(NewtypeDecl nt, ConcreteSyntaxTre
} else {
throw new UnsupportedFeatureException(nt.Origin, Feature.NonNativeNewtypes);
}
var className = "class_" + IdName(nt);
var cw = CreateClass(nt.EnclosingModuleDefinition.GetCompileName(Options), className, nt, wr) as ClassWriter;
var cw = CreateClass(nt.EnclosingModuleDefinition.GetCompileName(Options), nt, wr) as ClassWriter;
var className = clName(nt);
var w = cw.MethodDeclWriter;
if (nt.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
var witness = new ConcreteSyntaxTree(w.RelativeIndentLevel);
Expand Down Expand Up @@ -653,8 +662,8 @@ protected override void DeclareSubsetType(SubsetTypeDecl sst, ConcreteSyntaxTree

this.modDeclWr.WriteLine("{0} using {1} = {2};", templateDecl, IdName(sst), TypeName(sst.Var.Type, wr, sst.Origin));

var className = "class_" + IdName(sst);
var cw = CreateClass(sst.EnclosingModuleDefinition.GetCompileName(Options), className, sst, wr) as ClassWriter;
var cw = CreateClass(sst.EnclosingModuleDefinition.GetCompileName(Options), sst, wr) as ClassWriter;
var className = clName(sst);
var w = cw.MethodDeclWriter;

if (sst.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
Expand Down Expand Up @@ -785,7 +794,7 @@ public void Finish() { }

wr.Write("{0} {1}{2}::{3}",
targetReturnTypeReplacement ?? "void",
m.EnclosingClass.GetCompileName(Options),
clName(m.EnclosingClass),
InstantiateTemplate(m.EnclosingClass.TypeArgs),
IdName(m));

Expand Down Expand Up @@ -1043,7 +1052,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
} else if (cl is NewtypeDecl) {
var td = (NewtypeDecl)cl;
if (td.Witness != null) {
return td.EnclosingModuleDefinition.GetCompileName(Options) + "::class_" + td.GetCompileName(Options) + "::Witness";
return td.EnclosingModuleDefinition.GetCompileName(Options) + "::" + clName(td) + "::Witness";
} else if (td.NativeType != null) {
return "0";
} else {
Expand All @@ -1052,7 +1061,7 @@ protected override string TypeInitializationValue(Type type, ConcreteSyntaxTree
} else if (cl is SubsetTypeDecl) {
var td = (SubsetTypeDecl)cl;
if (td.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
return td.EnclosingModuleDefinition.GetCompileName(Options) + "::class_" + td.GetCompileName(Options) + "::Witness";
return td.EnclosingModuleDefinition.GetCompileName(Options) + "::" + clName(td) + "::Witness";
} else if (td.WitnessKind == SubsetTypeDecl.WKind.Special) {
// WKind.Special is only used with -->, ->, and non-null types:
Contract.Assert(ArrowType.IsPartialArrowTypeName(td.Name) || ArrowType.IsTotalArrowTypeName(td.Name) || td is NonNullTypeDecl);
Expand Down Expand Up @@ -1762,7 +1771,7 @@ protected override ILvalue EmitMemberSelect(Action<ConcreteSyntaxTree> obj, Type
// This used to work, but now obj comes in wanting to use TypeName on the class, which results in (std::shared_ptr<_module::MyClass>)::c;
//return SuffixLvalue(obj, "::{0}", member.CompileName);
return SimpleLvalue(wr => {
wr.Write("{0}::{1}::{2}", IdProtect(member.EnclosingClass.EnclosingModuleDefinition.GetCompileName(Options)), IdProtect(member.EnclosingClass.GetCompileName(Options)), IdProtect(member.GetCompileName(Options)));
wr.Write("{0}::{1}::{2}", IdProtect(member.EnclosingClass.EnclosingModuleDefinition.GetCompileName(Options)), IdProtect(clName(member.EnclosingClass)), IdProtect(member.GetCompileName(Options)));
});
} else if (member is DatatypeDestructor dtor && dtor.EnclosingClass is TupleTypeDecl) {
return SuffixLvalue(obj, ".get<{0}>()", dtor.Name);
Expand Down
Loading

0 comments on commit 585aef2

Please sign in to comment.