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

Jump to bottom

fix: Compilation of subset types constrained by type parameter #3893

Merged
merged 15 commits into from
May 4, 2023
Merged

fix: Compilation of subset types constrained by type parameter #3893

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
15 commits
Select commit Hold shift + click to select a range
162a95e
Add test cases
RustanLeino Apr 20, 2023
d2dca99
fix: Improve Subrange verification to reduce a completeness issue
RustanLeino Apr 20, 2023
1035bed
fix: Crash in resolver
RustanLeino Apr 20, 2023
4bd9803
fix: For Java
RustanLeino Apr 21, 2023
079dde2
fix: For C#
RustanLeino Apr 21, 2023
34a2db0
fix: For Go
RustanLeino Apr 21, 2023
59e1a32
fix: Add cast required by Java for functions
RustanLeino Apr 21, 2023
0b6ecd4
Add tests
RustanLeino Apr 21, 2023
8973cd7
Remove apparently unreachable code
RustanLeino Apr 21, 2023
f65ec61
Update tests
RustanLeino Apr 21, 2023
aa15dc9
Add release notes
RustanLeino Apr 21, 2023
2bd8e7e
Merge branch 'master' into issue-3883
RustanLeino Apr 21, 2023
dc7fb51
Update 3892-fix to cover additional bugs
RustanLeino Apr 22, 2023
539c006
Merge branch 'master' into issue-3883
RustanLeino Apr 26, 2023
d65ad03
Merge branch 'master' into issue-3883
RustanLeino May 4, 2023
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
Prev Previous commit
Next Next commit
Update 3892-fix to cover additional bugs
  • Loading branch information
@RustanLeino
RustanLeino committed Apr 22, 2023
commit dc7fb514c7aefbb57761558b216096ff00bdd777
21 changes: 15 additions & 6 deletions Source/DafnyCore/Compilers/Java/Compiler-java.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -399,7 +399,11 @@ private enum JavaNativeType { Byte, Short, Int, Long }
cw.DeclareField("Witness", sst, true, true, sst.Rhs, sst.tok, witness, null);
witness = "Witness";
}
var w = cw.StaticMemberWriter.NewBlock($"public static {TypeParameters(sst.TypeArgs, " ")}{typeName} defaultValue()");
cw.StaticMemberWriter.Write($"public static {TypeParameters(sst.TypeArgs, " ")}{typeName} defaultValue(");
var typeDescriptorParams = sst.TypeArgs.Where(NeedsTypeDescriptor);
cw.StaticMemberWriter.Write(typeDescriptorParams.Comma(tp =>
$"{DafnyTypeDescriptor}<{tp.GetCompileName(Options)}> {FormatTypeDescriptorVariable(tp.GetCompileName(Options))}"));
var w = cw.StaticMemberWriter.NewBlock(")");
w.WriteLine($"return {witness};");
}
}
Expand Down Expand Up @@ -1018,10 +1022,8 @@ protected class ClassWriter : IClassWriter {
typeDescriptorExpr = "_TYPE";
}
wr.Write($"public static {TypeParameters(typeParams, " ")}{DafnyTypeDescriptor}<{targetTypeName}> {TypeMethodName}(");
if (typeParams.Count != 0) {
var typeDescriptorParams = typeParams.Where(tp => NeedsTypeDescriptor(tp)).ToList();
wr.Write(typeDescriptorParams.Comma(tp => $"{DafnyTypeDescriptor}<{tp.GetCompileName(Options)}> {FormatTypeDescriptorVariable(tp.GetCompileName(Options))}"));
}
var typeDescriptorParams = typeParams.Where(NeedsTypeDescriptor);
wr.Write(typeDescriptorParams.Comma(tp => $"{DafnyTypeDescriptor}<{tp.GetCompileName(Options)}> {FormatTypeDescriptorVariable(tp.GetCompileName(Options))}"));
var wTypeMethodBody = wr.NewBlock(")", "");
var typeDescriptorCast = $"({DafnyTypeDescriptor}<{targetTypeName}>) ({DafnyTypeDescriptor}<?>)";
wTypeMethodBody.WriteLine($"return {typeDescriptorCast} {typeDescriptorExpr};");
Expand Down Expand Up @@ -3085,7 +3087,14 @@ protected class ClassWriter : IClassWriter {
} else if (cl is SubsetTypeDecl) {
var td = (SubsetTypeDecl)cl;
if (td.WitnessKind == SubsetTypeDecl.WKind.Compiled) {
return FullTypeName(udt) + ".defaultValue()";
var relevantTypeArgs = new List<Type>();
for (int i = 0; i < td.TypeArgs.Count; i++) {
if (NeedsTypeDescriptor(td.TypeArgs[i])) {
relevantTypeArgs.Add(udt.TypeArgs[i]);
}
}
string typeParameters = Util.Comma(relevantTypeArgs, arg => TypeDescriptor(arg, wr, tok));
return $"{FullTypeName(udt)}.defaultValue({typeParameters})";
} 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
11 changes: 11 additions & 0 deletions Test/git-issues/git-issue-3883.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -60,9 +60,20 @@ method Print<X(0)>(x: X, suffix: string) {
type pos = x | 1 <= x witness 9
type Fn<R(0)> = f: int -> R | true witness * // this used to generate malformed Java code (issue #3892)

datatype Option<T> = Some(t: T) | None
type Fn0<R(0)> = f: int -> Option<R> | true witness PartialFnWitness // this used to generate malformed Java code (issue #3892)
type Fn1<R> = f: int -> Option<R> | true witness PartialFnWitness // this used to generate malformed Java code (issue #3892)

function PartialFnWitness<R>(x: int): Option<R> {
None
}

method Arrows() {
var f: Fn<int>;
var g: Fn<pos>;

var h: Fn0<pos>;
var k: Fn1<pos>;
}

module MoreTests {
Expand Down
Loading