diff --git a/src/main/scala/viper/gobra/translator/encodings/adts/AdtEncoding.scala b/src/main/scala/viper/gobra/translator/encodings/adts/AdtEncoding.scala index 2cae1926c..9cb025aaa 100644 --- a/src/main/scala/viper/gobra/translator/encodings/adts/AdtEncoding.scala +++ b/src/main/scala/viper/gobra/translator/encodings/adts/AdtEncoding.scala @@ -227,10 +227,109 @@ class AdtEncoding extends LeafTypeEncoding { vpr.Forall(Seq(variableDecl), Seq(trigger), vu.bigOr(equalities)(aPos, aInfo, aErrT))(aPos, aInfo, aErrT) )(aPos, aInfo, adtName, aErrT) } + + // The well-founded orders for ADTs are axiomatized WITHOUT resorting to a "rank" function as defined in + // Paul Dahlke's thesis - section 5.3.2 (https://ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Education/Theses/Paul_Dahlke_BA_Report.pdf) + // This makes the implementation simpler. Nonetheless, we can use rank functions in the future if we find a + // good reason to have them. + val terminationMeasureAxioms: Vector[vpr.AnonymousDomainAxiom] = { + // As described in the section "Custom Well-Founded Orders" of the Viper tutorial + // (http://viper.ethz.ch/tutorial/#term_custom_orders), in order to define a custom termination measure for + // a domain type, we need to axiomatize the domain functions "bounded" and "decreasing" (defined in the + // file https://github.com/viperproject/silver/blob/master/src/main/resources/import/decreases/declaration.vpr) + // for that type. Unfortunately, there are no hooks to those domain functions provided by silver, and we refer + // to those methods using the following constants: + val wellFoundedDomainName = "WellFoundedOrder" + val wellFoundedDomainTypeVar = vpr.TypeVar("T") + val boundedFuncName = "bounded" + val decreasingFuncName = "decreasing" + // Note that this is brittle, and changes to the declaration of these functions will be detected + // as runtime errors. + + // l and r must both be instances of the ADT being defined + def applyDecreasing(l: vpr.Exp, r: vpr.Exp): vpr.DomainFuncApp = { + vpr.DomainFuncApp( + funcname = decreasingFuncName, + args = Seq(l,r), + typVarMap = Map(wellFoundedDomainTypeVar -> adtT) + )(aPos, aInfo, vpr.Bool, wellFoundedDomainName, aErrT) + } + + // e must be an instance of the ADT being defined + def applyBounded(e: vpr.Exp): vpr.DomainFuncApp = { + vpr.DomainFuncApp( + funcname = boundedFuncName, + args = Seq(e), + typVarMap = Map(wellFoundedDomainTypeVar -> adtT) + )(aPos, aInfo, vpr.Bool, wellFoundedDomainName, aErrT) + } + + // Every ADT instance has a finite instantiation: + // forall t: X :: { bounded(t) } bounded(t) + val allADTInstancesAreBounded = { + val variableDecl = adtDecl(aPos, aInfo, aErrT) + val variable = variableDecl.localVar + val boundedApp = applyBounded(variable) + val trigger = vpr.Trigger(Seq(boundedApp))(aPos, aInfo, aErrT) + val body = vpr.Forall( + variables = Seq(variableDecl), + triggers = Seq(trigger), + exp = boundedApp + )(aPos, aInfo, aErrT) + vpr.AnonymousDomainAxiom(body)(aPos, aInfo, adtName, aErrT) + } + + // forall x, y, z: X :: { decreasing(x,y), decreasing(y,z) } decreasing(x,z) + val decreasingTransitive = { + val varX = vpr.LocalVarDecl("X", adtT)(aPos, aInfo, aErrT) + val varY = vpr.LocalVarDecl("Y", adtT)(aPos, aInfo, aErrT) + val varZ = vpr.LocalVarDecl("Z", adtT)(aPos, aInfo, aErrT) + val decrApp1 = applyDecreasing(varX.localVar, varY.localVar) + val decrApp2 = applyDecreasing(varY.localVar, varZ.localVar) + val decrApp3 = applyDecreasing(varX.localVar, varZ.localVar) + val trigger = vpr.Trigger(Seq(decrApp1, decrApp2))(aPos, aInfo, aErrT) + val body = vpr.Forall( + variables = Seq(varX, varY, varZ), + triggers = Seq(trigger), + exp = vpr.Implies(vpr.And(decrApp1, decrApp2)(aPos, aInfo, aErrT), decrApp3)(aPos, aInfo, aErrT) + )(aPos, aInfo, aErrT) + vpr.AnonymousDomainAxiom(body)(aPos, aInfo, adtName, aErrT) + } + + // For every non-nullary constructor C of arity n and for every index i of a parameter of C with the ADT type, + // we generate: + // forall p1: T1, ..., pi: X, ..., pn: Tn :: { decreasing(pi, C(p1, ..., pi, ..., pn)) } + // decreasing(pi, C(p1, ..., pi, ..., pn)) + val decreasingAxioms = constructors zip adt.clauses flatMap { + // clause is required here to get a Seq[LocalVarDecl] for the `variables` param of `vpr.Forall` list. From an + // element in constructors, we can get only get a Seq[AnyLocalVarDecl]. An alternative would be to re-compute + // a list of variables for the qtfier. + case (cons, clause) => + val qtfiedConsArgs = fieldDecls(clause) + qtfiedConsArgs collect { + case arg if arg.typ == adtT => + val constructedElem = vpr.DomainFuncApp( + funcname = cons.name, + args = qtfiedConsArgs.map(_.localVar), + typVarMap = Map() + )(aPos, aInfo, cons.typ, adtName, aErrT) + val decreasingApp = applyDecreasing(arg.localVar, constructedElem) + val trigger = vpr.Trigger(Seq(decreasingApp))(aPos, aInfo, aErrT) + val body = vpr.Forall( + variables = qtfiedConsArgs, + triggers = Seq(trigger), + exp = decreasingApp + )(aPos, aInfo, aErrT) + vpr.AnonymousDomainAxiom(body)(aPos, aInfo, adtName, aErrT) + } + } + allADTInstancesAreBounded +: decreasingTransitive +: decreasingAxioms + } + ml.unit(Vector(vpr.Domain( adtName, functions = (defaultFunc +: tagFunc +: clauseTags) ++ constructors ++ destructors, - axioms = (exclusiveAxiom +: constructorAxioms) ++ destructorAxioms + axioms = (exclusiveAxiom +: constructorAxioms) ++ destructorAxioms ++ terminationMeasureAxioms )(pos = aPos, info = aInfo, errT = aErrT))) } diff --git a/src/test/resources/regressions/features/adts/termination-fail1.gobra b/src/test/resources/regressions/features/adts/termination-fail1.gobra new file mode 100644 index 000000000..3555c6132 --- /dev/null +++ b/src/test/resources/regressions/features/adts/termination-fail1.gobra @@ -0,0 +1,41 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package pkg + +type tree adt{ + leaf{ value int } + node{ left, right tree } +} + +ghost +pure +decreases // cause: wrong termination measure +func leafCount(t tree) int { + return match t { + case leaf{_}: 1 + //:: ExpectedOutput(pure_function_termination_error) + case node{?l, ?r}: leafCount(l) + leafCount(r) + } +} + +type list adt { + Empty{} + + Cons{ + head any + tail list + } +} + +ghost +decreases l +func length(l list) int { + match l { + case Empty{}: + return 0 + case Cons{_, ?t}: + //:: ExpectedOutput(function_termination_error) + return 1 + length(l) // cause: pass l to length instead of t + } +} \ No newline at end of file diff --git a/src/test/resources/regressions/features/adts/termination-success1.gobra b/src/test/resources/regressions/features/adts/termination-success1.gobra new file mode 100644 index 000000000..885345fc8 --- /dev/null +++ b/src/test/resources/regressions/features/adts/termination-success1.gobra @@ -0,0 +1,39 @@ +// Any copyright is dedicated to the Public Domain. +// http://creativecommons.org/publicdomain/zero/1.0/ + +package pkg + +type tree adt{ + leaf{ value int } + node{ left, right tree } +} + +ghost +pure +decreases t +func leafCount(t tree) int { + return match t { + case leaf{_}: 1 + case node{?l, ?r}: leafCount(l) + leafCount(r) + } +} + +type list adt { + Empty{} + + Cons{ + head any + tail list + } +} + +ghost +decreases l +func length(l list) int { + match l { + case Empty{}: + return 0 + case Cons{_, ?t}: + return 1 + length(t) + } +} \ No newline at end of file