Skip to content

Add support for uninterpreted predicates in ACSL #37

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

Open
zafer-esen wants to merge 3 commits into
base: master
Choose a base branch
from
Open

Add support for uninterpreted predicates in ACSL #37

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
1fe9710
Add support for uninterpreted predicates in ACSL
Jul 3, 2025
9f09411
Merge branch 'master' into martin-patch
zafer-esen Jul 3, 2025
f67f1e1
Update contributors
zafer-esen Jul 3, 2025
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
14 changes: 9 additions & 5 deletions src/tricera/acsl/ACSLTranslator.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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:
Expand Down Expand Up @@ -33,6 +34,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}
Expand Down Expand Up @@ -87,11 +89,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 =>
Expand Down Expand Up @@ -134,7 +137,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._

Expand Down Expand Up @@ -407,7 +411,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_)
Expand Down
100 changes: 77 additions & 23 deletions src/tricera/acsl/Encoder.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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:
Expand Down Expand Up @@ -30,9 +31,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
Expand Down Expand Up @@ -67,6 +66,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.
Expand Down Expand Up @@ -102,13 +103,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
Expand All @@ -128,8 +181,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) => {
Expand All @@ -138,8 +191,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)
Expand Down Expand Up @@ -205,15 +258,16 @@ class Encoder(reader : CCReader) {

// Handles function calls, e.g:
// f_pre(..) :- mainN(..), .. ==> false :- mainN(..), .., !<pre>
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(predPreSuffix)
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
Expand All @@ -236,20 +290,20 @@ class Encoder(reader : CCReader) {
clauses.collect({
// Handles final clause, e.g:
// f_post(..) :- f1(..) ==> false :- f1(..), !(<post> & <assigns>)
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(predPostSuffix)
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 = {
Expand Down
10 changes: 5 additions & 5 deletions src/tricera/concurrency/CCReader.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -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:
Expand Down Expand Up @@ -376,7 +376,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)]
Expand All @@ -393,6 +392,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()

//////////////////////////////////////////////////////////////////////////////

Expand Down Expand Up @@ -1027,7 +1027,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)
Expand Down Expand Up @@ -4421,7 +4421,7 @@ class CCReader private (prog : Program,
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)),
Expand Down Expand Up @@ -4503,7 +4503,7 @@ class CCReader private (prog : Program,
override val annotationNumLines : Int = 1
}
ACSLTranslator.translateACSL(
"/*@" + annot + "*/", new LocalContext()) match {
"/*@" + annot + "*/", new LocalContext(), uninterpPredDecls) match {
case res : tricera.acsl.LoopAnnotation =>
???
case _ =>
Expand Down
3 changes: 2 additions & 1 deletion src/tricera/params/TriCeraParameters.scala
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand Down