From 60036a94bf56dcb15e7f426f0e485e16fb85b651 Mon Sep 17 00:00:00 2001 From: leino Date: Thu, 21 Aug 2014 23:23:20 -0700 Subject: Added .Trunc field to real-based types Changed semantics of real-to-int conversions--these now have a precondition that the number converted is already an integer --- Binaries/DafnyPrelude.bpl | 14 +------ Source/Dafny/Resolver.cs | 74 +++++++++++++++++++++++++++------- Source/Dafny/Translator.cs | 37 +++++++++++++++-- Test/dafny0/DerivedTypes.dfy | 8 ++++ Test/dafny0/DerivedTypesResolution.dfy | 3 ++ Test/dafny0/RealCompare.dfy | 2 +- Test/dafny0/RealTypes.dfy | 16 ++++++-- Test/dafny0/RealTypes.dfy.expect | 19 +++++---- 8 files changed, 129 insertions(+), 44 deletions(-) diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 3d5bf111..bf9ef568 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -432,8 +432,7 @@ axiom (forall o: ref :: 0 <= _System.array.Length(o)); // -- Reals ------------------------------------------------------ // --------------------------------------------------------------- -function _System.Real.RealToInt(h: Heap, x: real): int { int(x) } -function _System.Real.IntToReal(h: Heap, x: int): real { real(x) } +function {:inline true} _System.real.Trunc(x: real): int { int(x) } // --------------------------------------------------------------- // -- The heap --------------------------------------------------- @@ -868,17 +867,6 @@ axiom (forall s, t: Seq T :: function Seq#FromArray(h: Heap, a: ref): Seq Box; axiom (forall h: Heap, a: ref :: { Seq#Length(Seq#FromArray(h,a)) } - /* -<<<<<<< local - Seq#Length(Seq#FromArray(h, a)) == _System.array.Length(a)); -axiom (forall h: Heap, a: ref :: { Seq#FromArray(h,a): Seq Box } - (forall i: int :: 0 <= i && i < Seq#Length(Seq#FromArray(h, a)) ==> Seq#Index(Seq#FromArray(h, a), i) == read(h, a, IndexField(i)))); -axiom (forall h: Heap, o: ref, f: Field alpha, v: alpha, a: ref :: - { Seq#FromArray(update(h, o, f, v), a) } - o != a ==> Seq#FromArray(update(h, o, f, v), a) == Seq#FromArray(h, a) ); -axiom (forall h: Heap, i: int, v: Box, a: ref :: -======= -*/ Seq#Length(Seq#FromArray(h, a)) == _System.array.Length(a)); axiom (forall h: Heap, a: ref, i: int :: { Seq#Index(Seq#FromArray(h, a): Seq Box, i) } diff --git a/Source/Dafny/Resolver.cs b/Source/Dafny/Resolver.cs index dd600e18..dbfdf846 100644 --- a/Source/Dafny/Resolver.cs +++ b/Source/Dafny/Resolver.cs @@ -141,6 +141,12 @@ namespace Microsoft.Dafny readonly Dictionary> classMembers = new Dictionary>(); readonly Dictionary> datatypeMembers = new Dictionary>(); readonly Dictionary> datatypeCtors = new Dictionary>(); + enum BasicTypeVariety { Bool = 0, Int, Real, None } // note, these are ordered, so they can be used as indices into basicTypeMembers + readonly Dictionary[] basicTypeMembers = new Dictionary[] { + new Dictionary(), + new Dictionary(), + new Dictionary() + }; readonly Graph dependencies = new Graph(); private ModuleSignature systemNameInfo = null; private bool useCompileSignatures = false; @@ -149,6 +155,9 @@ namespace Microsoft.Dafny public Resolver(Program prog) { Contract.Requires(prog != null); builtIns = prog.BuiltIns; + // Populate the members of the basic types + var trunc = new SpecialField(Token.NoToken, "Trunc", "ToBigInteger()", "", "", false, false, false, Type.Int, null); + basicTypeMembers[(int)BasicTypeVariety.Real].Add(trunc.Name, trunc); } [ContractInvariantMethod] @@ -6072,6 +6081,16 @@ namespace Microsoft.Dafny nptype = null; // prepare for the worst receiverType = receiverType.NormalizeExpand(); + var opProxy = receiverType as OperationTypeProxy; + if (opProxy != null) { + if (opProxy.JustInts) { + // close enough to do member lookups for int-based types + receiverType = Type.Int; + } else if (opProxy.JustReals) { + // close enough to do member lookups for real-based types + receiverType = Type.Real; + } + } if (receiverType is TypeProxy) { Error(tok, "type of the receiver is not fully determined at this program point", receiverType); return null; @@ -6110,6 +6129,24 @@ namespace Microsoft.Dafny } } + BasicTypeVariety basic; + if (receiverType.IsBoolType) { + basic = BasicTypeVariety.Bool; + } else if (receiverType.IsNumericBased(Type.NumericPersuation.Int)) { + basic = BasicTypeVariety.Int; + } else if (receiverType.IsNumericBased(Type.NumericPersuation.Real)) { + basic = BasicTypeVariety.Real; + } else { + basic = BasicTypeVariety.None; + } + if (basic != BasicTypeVariety.None) { + MemberDecl member; + if (basicTypeMembers[(int)basic].TryGetValue(memberName, out member)) { + nptype = (NonProxyType)receiverType; + return member; + } + } + Error(tok, "type {0} does not have a member {1}", receiverType, memberName); return null; } @@ -6470,18 +6507,22 @@ namespace Microsoft.Dafny Contract.Assert(e.Obj.Type != null); // follows from postcondition of ResolveExpression NonProxyType nptype; MemberDecl member = ResolveMember(expr.tok, e.Obj.Type, e.MemberName, out nptype); -#if !NO_WORK_TO_BE_DONE - UserDefinedType ctype = nptype as UserDefinedType; -#endif if (member == null) { // error has already been reported by ResolveMember } else if (member is Function) { var fn = member as Function; e.Member = fn; // build the type substitution map - var subst = TypeSubstitutionMap(ctype.ResolvedClass.TypeArgs, ctype.TypeArgs); - // instantiate all type arguments from the functions. no polymorphic application - e.TypeApplication = new List(ctype.TypeArgs); + e.TypeApplication = new List(); + Dictionary subst; + var ctype = nptype as UserDefinedType; + if (ctype == null) { + subst = new Dictionary(); + } else { + subst = TypeSubstitutionMap(ctype.ResolvedClass.TypeArgs, ctype.TypeArgs); + // instantiate all type arguments from the functions. no polymorphic application + e.TypeApplication.AddRange(ctype.TypeArgs); + } foreach (var tp in fn.TypeArgs) { Type prox = new InferredTypeProxy(); subst[tp] = prox; @@ -6489,20 +6530,23 @@ namespace Microsoft.Dafny } e.Type = SubstType(fn.Type, subst); AddCallGraphEdge(e, opts.codeContext, fn); - } else if (!(member is Field)) { - Error(expr, "member {0} in type {1} does not refer to a field or a function", e.MemberName, - cce.NonNull(ctype).Name); - } else { - Contract.Assert(member is Field); - Contract.Assert(ctype != null && ctype.ResolvedClass != null); // follows from postcondition of ResolveMember + } else if (member is Field) { var field = (Field)member; e.Member = field; if (e.Obj is StaticReceiverExpr) { Error(expr, "a field must be selected via an object, not just a class name"); } - // build the type substitution map - var subst = TypeSubstitutionMap(ctype.ResolvedClass.TypeArgs, ctype.TypeArgs); - e.Type = SubstType(field.Type, subst); + var ctype = nptype as UserDefinedType; + if (ctype == null) { + e.Type = field.Type; + } else { + Contract.Assert(ctype.ResolvedClass != null); // follows from postcondition of ResolveMember + // build the type substitution map + var subst = TypeSubstitutionMap(ctype.ResolvedClass.TypeArgs, ctype.TypeArgs); + e.Type = SubstType(field.Type, subst); + } + } else { + Error(expr, "member {0} in type {1} does not refer to a field or a function", e.MemberName, nptype); } } else if (expr is SeqSelectExpr) { diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 1036d539..a261f396 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -60,6 +60,7 @@ namespace Microsoft.Dafny { private readonly Bpl.TypeSynonymDecl multiSetTypeCtor; private readonly Bpl.TypeCtorDecl mapTypeCtor; public readonly Bpl.Function ArrayLength; + public readonly Bpl.Function RealTrunc; private readonly Bpl.TypeCtorDecl seqTypeCtor; readonly Bpl.TypeCtorDecl fieldName; public readonly Bpl.Type HeapType; @@ -82,6 +83,7 @@ namespace Microsoft.Dafny { Contract.Invariant(setTypeCtor != null); Contract.Invariant(multiSetTypeCtor != null); Contract.Invariant(ArrayLength != null); + Contract.Invariant(RealTrunc != null); Contract.Invariant(seqTypeCtor != null); Contract.Invariant(fieldName != null); Contract.Invariant(HeapVarName != null); @@ -143,7 +145,8 @@ namespace Microsoft.Dafny { } public PredefinedDecls(Bpl.TypeCtorDecl refType, Bpl.TypeCtorDecl boxType, Bpl.TypeCtorDecl tickType, - Bpl.TypeSynonymDecl setTypeCtor, Bpl.TypeSynonymDecl multiSetTypeCtor, Bpl.TypeCtorDecl mapTypeCtor, Bpl.Function arrayLength, Bpl.TypeCtorDecl seqTypeCtor, Bpl.TypeCtorDecl fieldNameType, + Bpl.TypeSynonymDecl setTypeCtor, Bpl.TypeSynonymDecl multiSetTypeCtor, Bpl.TypeCtorDecl mapTypeCtor, + Bpl.Function arrayLength, Bpl.Function realTrunc, Bpl.TypeCtorDecl seqTypeCtor, Bpl.TypeCtorDecl fieldNameType, Bpl.TypeCtorDecl tyType, Bpl.TypeCtorDecl tyTagType, Bpl.GlobalVariable heap, Bpl.TypeCtorDecl classNameType, Bpl.TypeCtorDecl nameFamilyType, Bpl.TypeCtorDecl datatypeType, Bpl.TypeCtorDecl handleType, Bpl.TypeCtorDecl layerType, Bpl.TypeCtorDecl dtCtorId, @@ -156,6 +159,7 @@ namespace Microsoft.Dafny { Contract.Requires(multiSetTypeCtor != null); Contract.Requires(mapTypeCtor != null); Contract.Requires(arrayLength != null); + Contract.Requires(realTrunc != null); Contract.Requires(seqTypeCtor != null); Contract.Requires(fieldNameType != null); Contract.Requires(heap != null); @@ -176,6 +180,7 @@ namespace Microsoft.Dafny { this.multiSetTypeCtor = multiSetTypeCtor; this.mapTypeCtor = mapTypeCtor; this.ArrayLength = arrayLength; + this.RealTrunc = realTrunc; this.seqTypeCtor = seqTypeCtor; this.fieldName = fieldNameType; this.HeapType = heap.TypedIdent.Type; @@ -204,6 +209,7 @@ namespace Microsoft.Dafny { Bpl.TypeSynonymDecl setTypeCtor = null; Bpl.TypeSynonymDecl multiSetTypeCtor = null; Bpl.Function arrayLength = null; + Bpl.Function realTrunc = null; Bpl.TypeCtorDecl seqTypeCtor = null; Bpl.TypeCtorDecl fieldNameType = null; Bpl.TypeCtorDecl classNameType = null; @@ -271,8 +277,11 @@ namespace Microsoft.Dafny { } } else if (d is Bpl.Function) { var f = (Bpl.Function)d; - if (f.Name == "_System.array.Length") + if (f.Name == "_System.array.Length") { arrayLength = f; + } else if (f.Name == "_System.real.Trunc") { + realTrunc = f; + } } } if (seqTypeCtor == null) { @@ -285,6 +294,8 @@ namespace Microsoft.Dafny { Console.WriteLine("Error: Dafny prelude is missing declaration of type Map"); } else if (arrayLength == null) { Console.WriteLine("Error: Dafny prelude is missing declaration of function _System.array.Length"); + } else if (realTrunc == null) { + Console.WriteLine("Error: Dafny prelude is missing declaration of function _System.real.Trunc"); } else if (fieldNameType == null) { Console.WriteLine("Error: Dafny prelude is missing declaration of type Field"); } else if (classNameType == null) { @@ -315,7 +326,11 @@ namespace Microsoft.Dafny { Console.WriteLine("Error: Dafny prelude is missing declaration of constant alloc"); } else { return new PredefinedDecls(refType, boxType, tickType, - setTypeCtor, multiSetTypeCtor, mapTypeCtor, arrayLength, seqTypeCtor, fieldNameType, tyType, tyTagType, heap, classNameType, nameFamilyType, datatypeType, handleType, layerType, dtCtorId, + setTypeCtor, multiSetTypeCtor, mapTypeCtor, + arrayLength, realTrunc, seqTypeCtor, fieldNameType, + tyType, tyTagType, + heap, classNameType, nameFamilyType, + datatypeType, handleType, layerType, dtCtorId, allocField); } return null; @@ -4657,6 +4672,18 @@ namespace Microsoft.Dafny { } else if (expr is UnaryExpr) { UnaryExpr e = (UnaryExpr)expr; CheckWellformed(e.E, options, locals, builder, etran); + if (e is ConversionExpr) { + var ee = (ConversionExpr)e; + if (ee.ToType is IntType && ee.E.Type.IsNumericBased(Type.NumericPersuation.Real)) { + // this operation is well-formed only if the real-based number represents an integer + // assert ToReal(ToInt(e.E)) == e.E + var arg = etran.TrExpr(e.E); + Bpl.Expr isAnInt = new Bpl.NAryExpr(e.tok, new ArithmeticCoercion(e.tok, ArithmeticCoercion.CoercionType.ToInt), new List { arg }); + isAnInt = new Bpl.NAryExpr(e.tok, new ArithmeticCoercion(e.tok, ArithmeticCoercion.CoercionType.ToReal), new List { isAnInt }); + isAnInt = Bpl.Expr.Binary(e.tok, BinaryOperator.Opcode.Eq, isAnInt, arg); + builder.Add(Assert(expr.tok, isAnInt, "the real-based number must be an integer (if you want truncation, apply .Trunc to the real-based number)")); + } + } } else if (expr is BinaryExpr) { BinaryExpr e = (BinaryExpr)expr; CheckWellformed(e.E0, options, locals, builder, etran); @@ -5525,7 +5552,6 @@ namespace Microsoft.Dafny { Contract.Requires(f != null && !f.IsMutable); Contract.Requires(sink != null && predef != null); Contract.Ensures(Contract.Result() != null); - Bpl.Function ff; if (fieldFunctions.TryGetValue(f, out ff)) { @@ -5534,6 +5560,9 @@ namespace Microsoft.Dafny { if (f.EnclosingClass is ArrayClassDecl && f.Name == "Length") { // link directly to the function in the prelude. fieldFunctions.Add(f, predef.ArrayLength); return predef.ArrayLength; + } else if (f.EnclosingClass == null && f.Name == "Trunc") { // link directly to the function in the prelude. + fieldFunctions.Add(f, predef.RealTrunc); + return predef.RealTrunc; } // function f(Ref): ty; Bpl.Type ty = TrType(f.Type); diff --git a/Test/dafny0/DerivedTypes.dfy b/Test/dafny0/DerivedTypes.dfy index ef9b7dae..127a3b08 100644 --- a/Test/dafny0/DerivedTypes.dfy +++ b/Test/dafny0/DerivedTypes.dfy @@ -11,6 +11,7 @@ method M() var s: set; var x: posReal; var y: posReal; + var yOrig := y; var z: int32; x := 5.3; z := 12; @@ -35,4 +36,11 @@ method M() y := 60.0; var dr: posReal := y / 2.0 + 120.0 / y; assert dr == 32.0; + + if yOrig == 0.3 { + var truncated := r0.Trunc + x.Trunc; + assert truncated == 5 + 5; + var rounded := (r0 + 0.5).Trunc; + assert rounded == 6; + } } diff --git a/Test/dafny0/DerivedTypesResolution.dfy b/Test/dafny0/DerivedTypesResolution.dfy index c3a02eeb..29f6e859 100644 --- a/Test/dafny0/DerivedTypesResolution.dfy +++ b/Test/dafny0/DerivedTypesResolution.dfy @@ -61,5 +61,8 @@ module Goodies { assert forall ii :: 0 <= ii < |sq| ==> sq[ii] == sq[ii]; var ms := multiset{23.0, 50.0}; assert forall rr :: 0.0 <= rr < 100.0 ==> ms[rr] == ms[rr]; + + var truncated := r0.Trunc + x.Trunc; + var rounded := (r0 + 0.5).Trunc; } } diff --git a/Test/dafny0/RealCompare.dfy b/Test/dafny0/RealCompare.dfy index b1dae47d..f5256d6f 100644 --- a/Test/dafny0/RealCompare.dfy +++ b/Test/dafny0/RealCompare.dfy @@ -145,7 +145,7 @@ method Test_AbsInt1() { var a, i := 0.3, 0.0; while i < 10.0 - invariant i <= 10.0 && i == real(int(i)); + invariant i <= 10.0 && i == real(i.Trunc); invariant a == 0.3 + 0.5 * i; { a, i := a + 0.5, i + 1.0; diff --git a/Test/dafny0/RealTypes.dfy b/Test/dafny0/RealTypes.dfy index e51b76ad..76ac9d93 100644 --- a/Test/dafny0/RealTypes.dfy +++ b/Test/dafny0/RealTypes.dfy @@ -4,8 +4,15 @@ method R1(ghost x: real, ghost y: real, i: int) { assert x + y == y + x; assert int(real(i)) == i; - assert real(int(x)) <= x; - assert real(int(x)) >= x; // error + assert real(x.Trunc) <= x; + if { + case real(x.Trunc) >= x => + assert x.Trunc == int(x); // the cast to int is allowed here + case true => + var t := int(x); // error: x may be a non-integer + case true => + assert real(x.Trunc) >= x; // error + } } method R2(ghost x: real, ghost y: real) { @@ -31,6 +38,7 @@ function R4(x:int, r:real) : int method RoundingDirection() { - assert int(51.500277) == 51; - assert int(-0.194771) == -1; + assert 51.500277.Trunc == 51; + assert (-0.194771).Trunc == -1; + assert -0.194771.Trunc == 0; } diff --git a/Test/dafny0/RealTypes.dfy.expect b/Test/dafny0/RealTypes.dfy.expect index 1f4d22a8..0d132948 100644 --- a/Test/dafny0/RealTypes.dfy.expect +++ b/Test/dafny0/RealTypes.dfy.expect @@ -1,18 +1,23 @@ -RealTypes.dfy(8,23): Error: assertion violation +RealTypes.dfy(12,16): Error: the real-based number must be an integer (if you want truncation, apply .Trunc to the real-based number) Execution trace: (0,0): anon0 -RealTypes.dfy(14,12): Error: possible division by zero + (0,0): anon6_Then +RealTypes.dfy(14,28): Error: assertion violation Execution trace: (0,0): anon0 - RealTypes.dfy(13,23): anon3_Else + (0,0): anon7_Then +RealTypes.dfy(21,12): Error: possible division by zero +Execution trace: + (0,0): anon0 + RealTypes.dfy(20,23): anon3_Else (0,0): anon2 -RealTypes.dfy(14,20): Error: assertion violation +RealTypes.dfy(21,20): Error: assertion violation Execution trace: (0,0): anon0 - RealTypes.dfy(13,23): anon3_Else + RealTypes.dfy(20,23): anon3_Else (0,0): anon2 -RealTypes.dfy(22,12): Error: assertion violation +RealTypes.dfy(29,12): Error: assertion violation Execution trace: (0,0): anon0 -Dafny program verifier finished with 6 verified, 4 errors +Dafny program verifier finished with 6 verified, 5 errors -- cgit v1.2.3