Allow adt constructors to have associated axiom

Author: JonasAlaif

src/main/scala/viper/silver/parser/ParseAst.scala

@@ -315,7 +315,7 @@ object PDomainFunctionArg {
 case class PIdnTypeBinding(idndef: PIdnDef, c: PSym.Colon, typ: PType)(val pos: (Position, Position))
 
 /** Anything that can be `PIdnUse`d as an expression (e.g. the receiver of a `PFieldAccess`). */
-sealed trait PTypedVarDecl extends PTypedDeclaration with PDeclarationInner {
+trait PTypedVarDecl extends PTypedDeclaration with PDeclarationInner {
   def idndef: PIdnDef
   def toIdnUse: PIdnUseExp = {
     val ref = PIdnRef[PTypedVarDecl](idndef.name)(idndef.pos)
@@ -1691,7 +1691,11 @@ case class PDomainFunction(annotations: Seq[PAnnotation], unique: Option[PKw.Uni
   override def endLinebreak = false
 }
 
-case class PAxiom(annotations: Seq[PAnnotation], axiom: PKw.Axiom, idndef: Option[PIdnDef], exp: PBracedExp)(val pos: (Position, Position)) extends PDomainMember
+/** Declares that all children expressions must always be well-defined. This is
+ * enforced during type-checking. Used e.g. for axioms. */
+trait PAlwaysWellDefined
+
+case class PAxiom(annotations: Seq[PAnnotation], axiom: PKw.Axiom, idndef: Option[PIdnDef], exp: PBracedExp)(val pos: (Position, Position)) extends PDomainMember with PAlwaysWellDefined
 
 case class PDomainInterpretation(name: PRawString, c: PSym.Colon, lit: PStringLiteral)(val pos: (Position, Position)) extends PNode
 case class PDomainInterpretations(k: PReserved[PKeywordLang], m: PDelimited.Comma[PSym.Paren, PDomainInterpretation])(val pos: (Position, Position)) extends PNode {

src/main/scala/viper/silver/parser/Resolver.scala

@@ -699,7 +699,7 @@ case class TypeChecker(names: NameAnalyser) {
                           check(fd.typ)
                           fd.formalArgs foreach (a => check(a.typ))
                         }
-                        if (pfa.isDescendant[PAxiom] && pfn.pres.toSeq.exists(pre => pre.k.rs == Requires)) {
+                        if (pfa.isDescendant[PAlwaysWellDefined] && pfn.pres.toSeq.exists(pre => pre.k.rs == Requires)) {
                           // A domain axiom, which must always be well-defined, is calling a function that has at least
                           // one real precondition (i.e., not just a requires clause or something similar that's
                           // temporarily represented as a precondition), which means that the call may not always be

src/main/scala/viper/silver/plugin/standard/adt/AdtASTExtension.scala

@@ -66,7 +66,7 @@ case class Adt(name: String, constructors: Seq[AdtConstructor], typVars: Seq[Typ
   * @param typ        the return type of the constructor
   * @param adtName    the name corresponding of the corresponding ADT
   */
-case class AdtConstructor(name: String, formalArgs: Seq[LocalVarDecl])
+case class AdtConstructor(name: String, formalArgs: Seq[LocalVarDecl], axiom: Option[Exp])
                          (val pos: Position, val info: Info, val typ: AdtType, val adtName: String, val errT: ErrorTrafo)
   extends ExtensionMember {
 
@@ -84,19 +84,20 @@ case class AdtConstructor(name: String, formalArgs: Seq[LocalVarDecl])
     if (!forceRewrite && this.children == children && pos.isEmpty)
       this
     else {
-      assert(children.length == 2, s"AdtConstructor : expected length 2 but got ${children.length}")
+      assert(children.length == 3, s"AdtConstructor : expected length 3 but got ${children.length}")
       val first = children.head.asInstanceOf[String]
       val second = children.tail.head.asInstanceOf[Seq[LocalVarDecl]]
-      AdtConstructor(first, second)(this.pos, this.info, this.typ, this.adtName, this.errT).asInstanceOf[this.type]
+      val third = children.tail.tail.head.asInstanceOf[Option[Exp]]
+      AdtConstructor(first, second, third)(this.pos, this.info, this.typ, this.adtName, this.errT).asInstanceOf[this.type]
     }
 
   }
 }
 
 object AdtConstructor {
-  def apply(adt: Adt, name: String, formalArgs: Seq[LocalVarDecl])
+  def apply(adt: Adt, name: String, formalArgs: Seq[LocalVarDecl], axiom: Option[Exp])
            (pos: Position = NoPosition, info: Info = NoInfo, errT: ErrorTrafo = NoTrafos): AdtConstructor = {
-    AdtConstructor(name, formalArgs)(pos, info, AdtType(adt, (adt.typVars zip adt.typVars).toMap), adt.name, errT)
+    AdtConstructor(name, formalArgs, axiom)(pos, info, AdtType(adt, (adt.typVars zip adt.typVars).toMap), adt.name, errT)
   }
 }
 

src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala

@@ -100,15 +100,15 @@ case class PAdtSeq[T <: PNode](seq: PDelimited.Block[T])(val pos: (Position, Pos
 }
 
 /** Any argument to a method, function or predicate. */
-case class PAdtFieldDecl(idndef: PIdnDef, c: PSym.Colon, typ: PType)(val pos: (Position, Position)) extends PAnyFormalArgDecl with PTypedDeclaration with PGlobalDeclaration with PMemberUniqueDeclaration with PAdtChild {
+case class PAdtFieldDecl(idndef: PIdnDef, c: PSym.Colon, typ: PType)(val pos: (Position, Position)) extends PAnyFormalArgDecl with PTypedVarDecl with PGlobalDeclaration with PMemberUniqueDeclaration with PAdtChild {
   def constructor: PAdtConstructor = getAncestor[PAdtConstructor].get
   def annotations: Seq[PAnnotation] = Nil
 }
 object PAdtFieldDecl {
   def apply(d: PIdnTypeBinding): PAdtFieldDecl = PAdtFieldDecl(d.idndef, d.c, d.typ)(d.pos)
 }
 
-case class PAdtConstructor(annotations: Seq[PAnnotation], idndef: PIdnDef, args: PDelimited.Comma[PSym.Paren, PAdtFieldDecl])(val pos: (Position, Position)) extends PExtender with PNoSpecsFunction with PGlobalUniqueDeclaration with PAdtChild {
+case class PAdtConstructor(annotations: Seq[PAnnotation], idndef: PIdnDef, args: PDelimited.Comma[PSym.Paren, PAdtFieldDecl], axiom: Option[(PKw.Axiom, PGrouped.Paren[PExp])])(val pos: (Position, Position)) extends PExtender with PNoSpecsFunction with PGlobalUniqueDeclaration with PAdtChild with PAlwaysWellDefined {
   override def resultType: PType = adt.getAdtType
   def fieldDecls: Seq[PAdtFieldDecl] = this.args.inner.toSeq
   override def typecheck(t: TypeChecker, n: NameAnalyser): Option[Seq[String]] = {
@@ -119,14 +119,18 @@ case class PAdtConstructor(annotations: Seq[PAnnotation], idndef: PIdnDef, args:
       val decl = discClashes.head
       t.messages ++= FastMessaging.message(idndef, "corresponding adt discriminator identifier `" + decl.idndef.name + "` at " + idndef.pos._1 + " is shadowed at " + decl.idndef.pos._1)
     }
+    axiom foreach (a => {
+      t.check(a._2.inner, TypeHelper.Bool)
+    })
     None
   }
 
   override def translateMemberSignature(t: Translator): AdtConstructor = {
     AdtConstructor(
       PAdt.findAdt(adt.idndef, t),
       idndef.name,
-      formalArgs map (_.asInstanceOf[PAdtFieldDecl]) map { arg => LocalVarDecl(arg.idndef.name, t.ttyp(arg.typ))(t.liftPos(arg.idndef)) }
+      formalArgs map (_.asInstanceOf[PAdtFieldDecl]) map { arg => LocalVarDecl(arg.idndef.name, t.ttyp(arg.typ))(t.liftPos(arg.idndef)) },
+      axiom map (axiom => t.exp(axiom._2.inner))
     )(t.liftPos(this), Translator.toInfo(annotations, this))
   }
 

src/main/scala/viper/silver/plugin/standard/adt/AdtPlugin.scala

@@ -20,7 +20,7 @@ class AdtPlugin(@unused reporter: viper.silver.reporter.Reporter,
                 config: viper.silver.frontend.SilFrontendConfig,
                 fp: FastParser) extends SilverPlugin with ParserPluginTemplate {
 
-  import fp.{annotation, argList, idnTypeBinding, idndef, idnref, semiSeparated, typ, typeList, domainTypeVarDecl, ParserExtension, lineCol, _file}
+  import fp.{annotation, argList, idnTypeBinding, idndef, idnref, parenthesizedExp, semiSeparated, typ, typeList, domainTypeVarDecl, ParserExtension, lineCol, _file}
   import FastParserCompanion.{ExtendedParsing, LeadingWhitespace, PositionParsing, reservedKw, reservedSym, whitespace}
 
   /**
@@ -91,7 +91,9 @@ class AdtPlugin(@unused reporter: viper.silver.reporter.Reporter,
 
   def adtConstructorDecls[$: P]: P[PAdtSeq[PAdtConstructor]] = P(semiSeparated(adtConstructorDecl).braces.map(PAdtSeq.apply _)).pos
 
-  def adtConstructorDecl[$: P]: P[PAdtConstructor] = P((annotation.rep ~ idndef ~ argList(idnTypeBinding.map(PAdtFieldDecl(_)))) map (PAdtConstructor.apply _).tupled).pos
+  def adtConstructorDecl[$: P]: P[PAdtConstructor] = P((annotation.rep ~ idndef ~ argList(idnTypeBinding.map(PAdtFieldDecl(_))) ~ adtConstructorAxiom.?) map (PAdtConstructor.apply _).tupled).pos
+
+  def adtConstructorAxiom[$: P]: P[(PKw.Axiom, PGrouped.Paren[PExp])] = P((P(PKw.Axiom) ~ parenthesizedExp))
 
   override def beforeResolve(input: PProgram): PProgram = {
     if (deactivated) {

src/main/scala/viper/silver/plugin/standard/adt/encoding/AdtEncoder.scala

@@ -90,7 +90,7 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
         val domain = Domain(name, null, null, typVars)(adt.pos, adt.info, adt.errT)
         val functions: Seq[DomainFunc] = (constructors map encodeAdtConstructorAsDomainFunc(domain)) ++
           (constructors flatMap generateDestructorDeclarations(domain)) ++ Seq(generateTagDeclaration(domain))
-        val axioms = (constructors flatMap generateInjectivityAxiom(domain)) ++
+        val axioms = (constructors flatMap generateInjectivityAxiom(domain)) ++ (constructors flatMap generatePreconditionAxiom(domain)) ++
           (constructors map generateTagAxiom(domain)) ++ Seq(generateExclusivityAxiom(domain)(constructors))
         val derivingAxioms = if (derivingInfo.contains(getContainsFunctionName))
           constructors filter (_.formalArgs.nonEmpty) map generateContainsAxiom(domain, derivingInfo(getContainsFunctionName)._2) else Seq.empty
@@ -136,6 +136,11 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
     }
   }
 
+  private def formalArgsToLocalVars(ac: AdtConstructor): Seq[LocalVar] = ac.formalArgs map (lv => lv.typ match {
+      case a: AdtType => localVarTFromType(encodeAdtTypeAsDomainType(a), Some(lv.name))(ac.pos, ac.info, ac.errT)
+      case d => localVarTFromType(d, Some(lv.name))(ac.pos, ac.info, ac.errT)
+    })
+
   /**
     * This method encodes an ADT constructor as a domain function
     *
@@ -145,7 +150,7 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
     */
   private def encodeAdtConstructorAsDomainFunc(domain: Domain)(ac: AdtConstructor): DomainFunc = {
     ac match {
-      case AdtConstructor(name, formalArgs) =>
+      case AdtConstructor(name, formalArgs, _) =>
         DomainFunc(name, formalArgs, encodeAdtTypeAsDomainType(ac.typ))(ac.pos, ac.info, domain.name, ac.errT)
     }
   }
@@ -222,7 +227,7 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
     * This method generates the corresponding injectivity axiom for an ADT constructor.
     *
     * axiom {
-    *     forall p_1: T_1, ..., p_n: T_n :: {C(p_1, ..., p_n)} p_i == D_Ci(C(p_1, ..., p_n))
+    *     forall p_1: T_1, ..., p_n: T_n :: {C(p_1, ..., p_n)} p_i == D_i(C(p_1, ..., p_n))
     * }
     *
     * where C is the ADT constructor, D_i the destructor for i-th argument of C
@@ -234,12 +239,7 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
   private def generateInjectivityAxiom(domain: Domain)(ac: AdtConstructor): Seq[AnonymousDomainAxiom] = {
     assert(domain.name == ac.adtName, "AdtEncoder: An error in the ADT encoding occurred.")
     val localVarDecl = ac.formalArgs.collect { case l: LocalVarDecl => l }
-    val localVars = ac.formalArgs.map { lv =>
-      lv.typ match {
-        case a: AdtType => localVarTFromType(encodeAdtTypeAsDomainType(a), Some(lv.name))(ac.pos, ac.info, ac.errT)
-        case d => localVarTFromType(d, Some(lv.name))(ac.pos, ac.info, ac.errT)
-      }
-    }
+    val localVars = formalArgsToLocalVars(ac)
     assert(localVarDecl.size == localVars.size, "AdtEncoder: An error in the ADT encoding occurred.")
 
     val constructorApp = DomainFuncApp(
@@ -256,11 +256,49 @@ class AdtEncoder(val program: Program) extends AdtNameManager {
         defaultTypeVarsFromDomain(domain)
       )(ac.pos, ac.info, lv.typ, ac.adtName, ac.errT)
       val eq = EqCmp(lv, right)(ac.pos, ac.info, ac.errT)
-      val forall = Forall(localVarDecl, Seq(trigger), eq)(ac.pos, ac.info, ac.errT)
+      val cond_eq = ac.axiom.map(p => Implies(p, eq)(ac.pos, ac.info, ac.errT)).getOrElse(eq)
+      val forall = Forall(localVarDecl, Seq(trigger), cond_eq)(ac.pos, ac.info, ac.errT)
       AnonymousDomainAxiom(forall)(ac.pos, ac.info, ac.adtName, ac.errT)
     }
   }
 
+  /**
+    * This method generates the corresponding precondition axiom for an ADT constructor.
+    *
+    * axiom {
+    *     forall t: AdtType :: {D_1(t)}...{D_n(t)} pre
+    * }
+    *
+    * where D_i the destructor for i-th argument of C
+    *
+    * @param domain The domain the encoded constructor belongs to
+    * @param ac     The adt constructor for which we want to generate the precondition axiom
+    * @return The precondition axiom if the constructor has a precondition
+    */
+  private def generatePreconditionAxiom(domain: Domain)(ac: AdtConstructor): Option[AnonymousDomainAxiom] = {
+    assert(domain.name == ac.adtName, "AdtEncoder: An error in the ADT encoding occurred.")
+    ac.axiom.map(pre => {
+      val localVarDecl = localVarTDeclFromType(domainTypeFromDomain(domain))(domain.pos, domain.info, domain.errT)
+      val localVar = localVarTFromType(domainTypeFromDomain(domain))(domain.pos, domain.info, domain.errT)
+
+      val destructorCalls = ac.formalArgs.map { lv =>
+        DomainFuncApp(
+          getDestructorName(domain.name, lv.name),
+          Seq(localVar),
+          defaultTypeVarsFromDomain(domain)
+        )(domain.pos, domain.info, lv.typ, domain.name, domain.errT)
+      }
+      val localVars = formalArgsToLocalVars(ac)
+      assert(destructorCalls.size == localVars.size, "AdtEncoder: An error in the ADT encoding occurred.")
+
+      val triggers = destructorCalls.map { t => Trigger(Seq(t))(domain.pos, domain.info, domain.errT) }
+      val pre_sub = pre.replace(localVars.zip(destructorCalls).toMap)
+      AnonymousDomainAxiom(
+        Forall(Seq(localVarDecl), triggers, pre_sub)(domain.pos, domain.info, domain.errT)
+      )(domain.pos, domain.info, domain.name, domain.errT)
+    })
+  }
+
   /**
     * This method generates the corresponding exclusivity axioms for a sequence of constructors.
     *