From 1fe971045f69b233d1fd84d4fda14e10b43c308c Mon Sep 17 00:00:00 2001 From: Martin Nilsson Date: Thu, 3 Jul 2025 14:41:59 +0200 Subject: [PATCH 1/2] Add support for uninterpreted predicates in ACSL See https://kth.diva-portal.org/smash/record.jsf?pid=diva2:1957907 --- src/tricera/acsl/ACSLTranslator.scala | 11 ++- src/tricera/acsl/Encoder.scala | 103 +++++++++++++++++++------ src/tricera/concurrency/CCReader.scala | 8 +- 3 files changed, 89 insertions(+), 33 deletions(-) diff --git a/src/tricera/acsl/ACSLTranslator.scala b/src/tricera/acsl/ACSLTranslator.scala index 80de672c..ae7fcbc6 100644 --- a/src/tricera/acsl/ACSLTranslator.scala +++ b/src/tricera/acsl/ACSLTranslator.scala @@ -33,6 +33,7 @@ package tricera.acsl import tricera.acsl.{Absyn => AST} import collection.JavaConverters._ +import scala.collection.mutable.{HashMap => MHashMap} import ap.parser._ import ap.theories.nia.GroebnerMultiplication._ import ap.types.{Sort, SortedConstantTerm} @@ -87,11 +88,12 @@ object ACSLTranslator { @throws[ACSLException]("if not called with the right context") @throws[ACSLParseException]("if parsing or translation fails") def translateACSL(annot : String, - ctx : AnnotationContext) : ParsedAnnotation = { + ctx : AnnotationContext, + preds : MHashMap[String, tricera.concurrency.CCReader.CCPredicate]) : ParsedAnnotation = { val l : Yylex = new Yylex(new java.io.StringReader(preprocess(annot))) val p : parser = new parser(l, l.getSymbolFactory()) val ast : AST.Annotation = p.pAnnotation() - val translator = new ACSLTranslator(ctx) + val translator = new ACSLTranslator(ctx, preds) ast match { case ac : AST.AnnotContract => @@ -134,7 +136,8 @@ object ACSLTranslator { * @param ctx Context providing information about the parsed program where * the ACSL annotation appears in. */ -class ACSLTranslator(ctx : ACSLTranslator.AnnotationContext) { +class ACSLTranslator(ctx : ACSLTranslator.AnnotationContext, + preds : MHashMap[String, tricera.concurrency.CCReader.CCPredicate]) { import scala.collection.mutable.{HashMap => MHashMap} import ACSLTranslator._ @@ -407,7 +410,7 @@ class ACSLTranslator(ctx : ACSLTranslator.AnnotationContext) { case e : AST.EStructPtrFieldAccess => ??? case e : AST.EArrayFunMod => ??? case e : AST.EFieldFunMod => ??? - case e : AST.EApplication => ??? + case e : AST.EApplication => new CCFormula(IAtom(preds(e.id_).pred, e.listexpr_.asScala.map(a => translate(a).toTerm)), CCBool, None) case e : AST.EOld => translateOldExpr(e) case e : AST.EValid => translateValidExpr(e) case e : AST.ELit => translateLitExpr(e.lit_) diff --git a/src/tricera/acsl/Encoder.scala b/src/tricera/acsl/Encoder.scala index e70ef171..8c5b13a4 100644 --- a/src/tricera/acsl/Encoder.scala +++ b/src/tricera/acsl/Encoder.scala @@ -30,9 +30,7 @@ package tricera.acsl -import ap.parser.IExpression -import ap.parser.CollectingVisitor -import ap.parser.{IAtom, IFormula, ITerm} +import ap.parser.{CollectingVisitor, IAtom, IBinFormula, IBinJunctor, IExpression, IFormula, ITerm} import lazabs.horn.bottomup.HornClauses.Clause import lazabs.horn.bottomup.HornClauses.FALSE import hornconcurrency.ParametricEncoder.System @@ -70,6 +68,8 @@ class Encoder(reader : CCReader) { val hasACSLEntryFunction : Boolean = reader.hasACSLEntryFunction + val uninterpPreds : Set[IExpression.Predicate] = reader.uninterpPredDecls.values.map(_.pred).toSet + def encode : System = { import ParametricEncoder._ // NOTE: Order of encoding matters. @@ -105,13 +105,65 @@ class Encoder(reader : CCReader) { } val newPreClauses : Seq[CCAssertionClause] = - preClauses.map(c => buildPreClause(reader.getRichClause(c).get)) + preClauses.flatMap(c => buildPreClause(reader.getRichClause(c).get)) val newPostClauses : Seq[CCAssertionClause] = buildPostAsserts others.map( c => reader.getRichClause(c).get.asInstanceOf[CCAssertionClause]) ++ newPreClauses ++ newPostClauses } + // E₁ ∧ ⋯ ∧ E_n ↦ (E₁, …, E_n) + private def conjuncts(form : IFormula) : Seq[IFormula] = form match { + case IBinFormula(IBinJunctor.And, l, r) => conjuncts(l) ++ conjuncts(r) + case _ => form::Nil + } + + // Make a clause where uninterpreted predicates given in the constraint are instead placed in the body. For example: + // + // Input: (P₁(⋯), + // (P₂(⋯), P₃(⋯), P₄(⋯)), + // E₁ ∧ P₅(⋯) ∧ E₂ ∧ P₆(⋯) ∧ E₃) + // + // Output: P₁(⋯) :− P₂(⋯), P₃(⋯), P₄(⋯), P₅(⋯), P₆(⋯), E₁ ∧ E₂ ∧ E₃ + // i.e. + // P₁(⋯) ← P₂(⋯) ∧ P₃(⋯) ∧ P₄(⋯) ∧ P₅(⋯) ∧ P₆(⋯) ∧ E₁ ∧ E₂ ∧ E₃ + // + private def clauseWUninterpPredsInBody(oldHead : IAtom, oldBody : List[IAtom], oldConstr : IFormula) : Clause = { + val (newBody, newConstr) : (List[IAtom], Seq[IFormula]) = + conjuncts(oldConstr) + .map(elem => elem.asInstanceOf[IFormula]) + .foldRight((oldBody, Nil : List[IFormula]))((cur, acc) => + cur match { + case a@IAtom(pred, _) if uninterpPreds(pred) => (a::acc._1, acc._2) + case _ => (acc._1, cur::acc._2) + }) + Clause(oldHead, newBody, IExpression.and(newConstr)) + } + + // Make an assertion and other clauses that together correspond to the assertion consisting of the given body and the conjunction of the first given constraint and the negation of the second given constraint. Uninterpreted predicates given in the second constraint instead become heads. For example: + // + // Input: ((P₂(⋯), P₃(⋯), P₄(⋯)), + // E₄ ∧ E₅, + // E₁ ∧ P₅(⋯) ∧ E₂ ∧ P₆(⋯) ∧ E₃) + // + // Output: (⊥ :− P₂(⋯), P₃(⋯), P₄(⋯), (E₄ ∧ E₅) ∧ ¬(E₁ ∧ E₂ ∧ E₃), + // P₅ :− P₂(⋯), P₃(⋯), P₄(⋯), (E₄ ∧ E₅), + // P₆ :− P₂(⋯), P₃(⋯), P₄(⋯), (E₄ ∧ E₅)) + // i.e. + // P₂(⋯) ∧ P₃(⋯) ∧ P₄(⋯) ∧ E₄ ∧ E₅ → E₁ ∧ P₅(⋯) ∧ E₂ ∧ P₆(⋯) ∧ E₃ + // + private def assertWNegConstrAndUninterpPredsInHeads(oldBody : List[IAtom], oldConstr : IFormula, oldNegConstr : IFormula) : Seq[Clause] = { + val (newAssert, newClauses) : (Seq[IFormula], List[Clause]) = + conjuncts(oldNegConstr) + .map(elem => elem.asInstanceOf[IFormula]) + .foldRight((Nil : List[IFormula], Nil : List[Clause]))((cur, acc) => + cur match { + case a@IAtom(pred, _) if uninterpPreds(pred) => (acc._1, Clause(a, oldBody, oldConstr)::acc._2) + case _ => (cur::acc._1, acc._2) + }) + Clause(falseHead, oldBody, oldConstr &&& IExpression.and(newAssert).unary_!)::newClauses + } + /** * * @return background axioms and a backmapping from these to the original clauses @@ -131,8 +183,8 @@ class Encoder(reader : CCReader) { val preAtom : IAtom = funToPreAtom(name) val preCond : IFormula = funToContract(name).pre val constr : IFormula = applyArgs(preCond, preAtom, atom) - new CCClause(Clause(head, List(), constr), - reader.getRichClause(c).get.srcInfo) + val clause : Clause = clauseWUninterpPredsInBody(head, Nil, constr) + new CCClause(clause, reader.getRichClause(c).get.srcInfo)::Nil } case c@Clause(head, body, oldConstr) if prePredsToReplace(head.pred) => { @@ -141,8 +193,8 @@ class Encoder(reader : CCReader) { buildPreClause(reader.getRichClause(c).get) } case c@Clause(head, _, _) if !postPredsToReplace(head.pred) => - replacePostPredInBody(reader.getRichClause(c).get) - }) + replacePostPredInBody(reader.getRichClause(c).get)::Nil + }).flatten (preds, encoded) } case NoBackgroundAxioms => (Nil, Nil) @@ -208,15 +260,16 @@ class Encoder(reader : CCReader) { // Handles function calls, e.g: // f_pre(..) :- mainN(..), .. ==> false :- mainN(..), .., !
-  private def buildPreClause(old : CCClause) : CCAssertionClause = {
+  private def buildPreClause(old : CCClause) : Seq[CCAssertionClause] = {
     assert(prePredsToReplace(old.clause.head.pred))
     val name    : String   = old.clause.head.pred.name.stripSuffix(preSuffix)
-    val preCond : IFormula = funToContract(name).pre
     val preAtom : IAtom    = funToPreAtom(name)
-    val constr  : IFormula = applyArgs(preCond, preAtom, old.clause.head).unary_!
-    reader.mkRichAssertionClause(Clause(falseHead, old.clause.body, constr),
-                              old.srcInfo,
-                              tricera.properties.FunctionPrecondition(name, old.srcInfo))
+    val preCond : IFormula = funToContract(name).pre
+    val constr  : IFormula = applyArgs(preCond, preAtom, old.clause.head)
+    for (clause <- assertWNegConstrAndUninterpPredsInHeads(old.clause.body, IExpression i true, constr))
+      yield reader.mkRichAssertionClause(clause,
+                                         old.srcInfo,
+                                         tricera.properties.FunctionPrecondition(name, old.srcInfo))
   }
 
   // Fetches clauses from system.processes and system.backgroundAxioms implying
@@ -239,20 +292,20 @@ class Encoder(reader : CCReader) {
     clauses.collect({
       // Handles final clause, e.g:
       // f_post(..) :- f1(..) ==> false :- f1(..), !( & )
-      case CCClause(Clause(head, body, oldConstr), srcInfo)
+      case CCClause(Clause(head, oldBody, oldConstr), srcInfo)
         if postPredsToReplace(head.pred) =>
-        val name     : String   = head.pred.name.stripSuffix(postSuffix)
-        val postAtom : IAtom    = funToPostAtom(name)
-        val postCond : IFormula = funToContract(name).post
+        val name     : String     = head.pred.name.stripSuffix(postSuffix)
+        val postAtom : IAtom      = funToPostAtom(name)
+        val postCond : IFormula   = funToContract(name).post
         val postSrc  : SourceInfo = funToContract(name).postSrcInfo
-        val constr   : IFormula = applyArgs(postCond, postAtom, head)
-        val assigns  : IFormula =
+        val constr   : IFormula   = applyArgs(postCond, postAtom, head)
+        val assigns  : IFormula   =
           applyArgs(funToContract(name).assignsAssert, postAtom, head)
-        reader.mkRichAssertionClause(Clause(
-          falseHead, body, oldConstr &&& (constr &&& assigns).unary_!),
-                                  Some(postSrc),
-                                  tricera.properties.FunctionPostcondition(name, srcInfo))
-    })
+        for (clause <- assertWNegConstrAndUninterpPredsInHeads(oldBody, oldConstr, constr &&& assigns))
+          yield reader.mkRichAssertionClause(clause,
+                                             Some(postSrc),
+                                             tricera.properties.FunctionPostcondition(name, srcInfo))
+    }).flatten
   }
 
   private def applyArgs(formula : IFormula, predParams : IAtom, predArgs : IAtom) : IFormula = {
diff --git a/src/tricera/concurrency/CCReader.scala b/src/tricera/concurrency/CCReader.scala
index beef2b0d..6103395e 100644
--- a/src/tricera/concurrency/CCReader.scala
+++ b/src/tricera/concurrency/CCReader.scala
@@ -373,7 +373,6 @@ class CCReader private (prog              : Program,
   private val enumDefs      = new MHashMap[String, CCType]
   private val enumeratorDefs= new MHashMap[String, CCExpr]
 
-  private val uninterpPredDecls     = new MHashMap[String, CCPredicate]
   private val interpPredDefs        = new MHashMap[String, CCFormula]
   private val loopInvariants        =
     new MHashMap[String, (CCPredicate, SourceInfo)]
@@ -390,6 +389,7 @@ class CCReader private (prog              : Program,
   val prePredsToReplace : MHashSet[Predicate] = new MHashSet()
   val postPredsToReplace : MHashSet[Predicate] = new MHashSet()
   val clauseToRichClause : MHashMap[Clause, CCClause] = new MHashMap()
+  val uninterpPredDecls : MHashMap[String, CCPredicate] = new MHashMap()
 
   //////////////////////////////////////////////////////////////////////////////
 
@@ -1018,7 +1018,7 @@ class CCReader private (prog              : Program,
         val possibleACSLAnnotation = annot.asInstanceOf[MaybeACSLAnnotation]
         // todo: try / catch and print msg?
         val contract = ACSLTranslator.translateACSL(
-          "/*@" + possibleACSLAnnotation.annot + "*/", funContext.acslContext)
+          "/*@" + possibleACSLAnnotation.annot + "*/", funContext.acslContext, uninterpPredDecls)
 
         prePredsToReplace.add(funContext.prePred.pred)
         postPredsToReplace.add(funContext.postPred.pred)
@@ -4397,7 +4397,7 @@ private def collectVarDecls(dec                    : Dec,
             override val annotationNumLines : Int = 1
           }
           ACSLTranslator.translateACSL(
-            "/*@" + annot + "*/", new LocalContext()) match {
+            "/*@" + annot + "*/", new LocalContext(), uninterpPredDecls) match {
             case res: tricera.acsl.StatementAnnotation =>
               if (res.isAssert) {
                 stmSymex.assertProperty(res.f, Some(getSourceInfo(stm)),
@@ -4479,7 +4479,7 @@ private def collectVarDecls(dec                    : Dec,
             override val annotationNumLines : Int = 1
           }
           ACSLTranslator.translateACSL(
-            "/*@" + annot + "*/", new LocalContext()) match {
+            "/*@" + annot + "*/", new LocalContext(), uninterpPredDecls) match {
             case res : tricera.acsl.LoopAnnotation =>
                 ???
             case _ =>

From f67f1e12462fbd2722f6522e7a20769619fc79b0 Mon Sep 17 00:00:00 2001
From: Zafer Esen 
Date: Thu, 3 Jul 2025 15:06:59 +0200
Subject: [PATCH 2/2] Update contributors

---
 src/tricera/acsl/ACSLTranslator.scala      | 3 ++-
 src/tricera/acsl/Encoder.scala             | 3 ++-
 src/tricera/concurrency/CCReader.scala     | 2 +-
 src/tricera/params/TriCeraParameters.scala | 3 ++-
 4 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/src/tricera/acsl/ACSLTranslator.scala b/src/tricera/acsl/ACSLTranslator.scala
index ae7fcbc6..9ddad918 100644
--- a/src/tricera/acsl/ACSLTranslator.scala
+++ b/src/tricera/acsl/ACSLTranslator.scala
@@ -1,6 +1,7 @@
 /**
  * Copyright (c) 2021-2022 Pontus Ernstedt
- *               2022-2023 Zafer Esen. All rights reserved.
+ *               2022-2025 Zafer Esen
+ *               2025 Martin Nilsson. All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
diff --git a/src/tricera/acsl/Encoder.scala b/src/tricera/acsl/Encoder.scala
index 4661d27f..9d25aa97 100644
--- a/src/tricera/acsl/Encoder.scala
+++ b/src/tricera/acsl/Encoder.scala
@@ -1,6 +1,7 @@
 /**
  * Copyright (c) 2021-2022 Pontus Ernstedt
- *               2024      Zafer Esen. All rights reserved.
+ *               2024-2025 Zafer Esen
+ *               2025 Martin Nilsson. All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
diff --git a/src/tricera/concurrency/CCReader.scala b/src/tricera/concurrency/CCReader.scala
index 2a520ff8..14019754 100644
--- a/src/tricera/concurrency/CCReader.scala
+++ b/src/tricera/concurrency/CCReader.scala
@@ -1,5 +1,5 @@
 /**
- * Copyright (c) 2015-2024 Zafer Esen, Philipp Ruemmer. All rights reserved.
+ * Copyright (c) 2015-2025 Zafer Esen, Philipp Ruemmer. All rights reserved.
  *
  * Redistribution and use in source and binary forms, with or without
  * modification, are permitted provided that the following conditions are met:
diff --git a/src/tricera/params/TriCeraParameters.scala b/src/tricera/params/TriCeraParameters.scala
index 594b86ee..e9ad9c73 100644
--- a/src/tricera/params/TriCeraParameters.scala
+++ b/src/tricera/params/TriCeraParameters.scala
@@ -128,7 +128,8 @@ class TriCeraParameters extends GlobalParameters {
   private val greeting =
     s"""TriCera v$version.
         |(C) Copyright 2012-2025 Zafer Esen and Philipp Ruemmer
-        |Contributors: Pontus Ernstedt, Hossein Hojjat, Oskar Soederberg, Scania CV AB""".stripMargin
+        |Contributors: Pontus Ernstedt, Hossein Hojjat, Martin Nilsson,
+        |              Oskar Soederberg, Scania CV AB""".stripMargin
 
 
   private def parseArgs(args: List[String], shouldExecute : Boolean = true): Boolean =