Parsing predicates that contains array operation

[Yoel Kim]

Dear CPAchecker team,

I am developing a custom predicate abstraction approach on top of CPAchecker, which imports predicates from an external file. Currently, I am encountering difficulties with making CPAchecker interpret predicates that contain array subscripting operations in predmap.txt. I have tried several variations on the predicates (e.g., removing @), but none have succeeded.

My current approach uses the PredicateMapParser class, and I have implemented a new method, toFormula, in the PredicatePrecisionBootstrapper class with Options.encodePredicates = PrecisionConverter.INT2BV;, as shown below:

public BooleanFormula toFormula(Path predicatesFile) throws IOException {

    options.encodePredicates = PrecisionConverter.INT2BV;

    PredicatePrecision result = PredicatePrecision.empty();

    PredicateMapParser parser = new PredicateMapParser(cfa, logger, formulaManagerView, abstractionManager, options);

   

    try {

      result = result.mergeWith(parser.parsePredicates(predicatesFile));

      return parser.getPredFormula();

    }

    catch (PredicateParsingFailedException e) {

      e.printStackTrace();

    }

    return null;

  }

This method takes predicatesFile (the predmap.txt file) as input, parses the file for integer-typed predicates, and converts them to bitvector format.

The following are the error messages:

Syntax error near Symbol: : (:1/30(-1) - :1/31(-1)) (PredicateCPA:FormulaParser.report_error, WARNING)

instead expected token classes are []
Couldn't repair and continue parse near Symbol: : (:1/30(-1) - :1/31(-1)) (PredicateCPA:FormulaParser.report_error, WARNING)

Exception in thread "main" java.lang.AssertionError: There was a problem while parsing the formula '''(declare-fun __ADDRESS_OF_main::c@ () Int)'''.
        at org.sosy_lab.cpachecker.util.predicates.precisionConverter.FormulaParser.convert0(FormulaParser.java:215)
        at org.sosy_lab.cpachecker.util.predicates.precisionConverter.FormulaParser.convertFormula(FormulaParser.java:195)
        at org.sosy_lab.cpachecker.cpa.predicate.persistence.PredicateMapParser.convertFormula(PredicateMapParser.java:278)
        at org.sosy_lab.cpachecker.cpa.predicate.persistence.PredicateMapParser.parsePredicates(PredicateMapParser.java:140)
        at org.sosy_lab.cpachecker.cpa.predicate.persistence.PredicateMapParser.parsePredicates(PredicateMapParser.java:118)

[Philipp Wendler]

Dear Yoel Kim,

thank you for your interest in CPAchecker!
Sorry for the late reply, we were quite busy in the last few weeks
working on CPAchecker 4.0.

I am not really sure I understand fully what you are doing.
You have changed the CPAchecker code and something fails?
Does it work if you do not attempt to use the PrecisionConverter?
The parser that is used by it could be incomplete, then it would have to
be extended.

Greetings
Philipp

Am 14.11.24 um 09:56 schrieb Yoel Kim:

--
Philipp Wendler
Software and Computational Systems Lab
LMU Munich, Germany
Oettingenstr. 67 Raum F008 - Tel.: 089/2180-9181

[Yoel Kim]

Dear, Philipp Wendler

Thank you for your response.

Firstly, I reviewed the 'util/predicates/precisionConverter/BVConverter.java' code and noticed that it seems unable to parse array types, likely due to the getSMTType method:
  private String getSMTType(FormulaType<?> t) {
    if (t == FormulaType.BooleanType) {
      return "Bool";
    } else if (t == FormulaType.IntegerType) {
      return "Int";
    } else if (t.isBitvectorType()) {
      return format("(_ BitVec %d)", ((BitvectorType) t).getSize());
    } else {
      throw new AssertionError("unhandled type: " + t);
    }
  }

Secondly, even when I do not use the PrecisionConverter (by setting the options 'cpa.predicate.encodeBitvectorAs = INTEGER' and 'options.encodePredicates = PrecisionConverter.DISABLE'), an error still occurs.
However, the error message differs from the previous one:

org.sosy_lab.cpachecker.cpa.predicate.persistence.PredicatePersistenceUtils$PredicateParsingFailedException: Parsing failed in line 8 of predmap.txt: unrecognized text: :
        at org.sosy_lab.cpachecker.cpa.predicate.persistence.PredicateMapParser.parsePredicates(PredicateMapParser.java:261)
        at org.sosy_lab.cpachecker.cpa.predicate.persistence.PredicateMapParser.parsePredicates(PredicateMapParser.java:118)

This issue seems to be related to the util/predicates/precisionConverter/FormulaParser.java code, which I am unable to fully interpret.

Do I need to provide predicates in the form of bitvectors directly? Or, could you please clarify the syntax that the parser accepts?

Best regards,
Yoel Kim

2024년 11월 26일 화요일 오후 11시 28분 24초 UTC+9에 Philipp Wendler님이 작성:

[Philipp Wendler]

Dear Yoel Kim,

Am 28.11.24 um 09:32 schrieb Yoel Kim:

> Firstly, I reviewed the 'util/predicates/precisionConverter/BVConverter.java'
> code and noticed that it seems unable to parse array types, likely due to
> the getSMTType method:

Yes, that may well be. The conversion of predicates from one theory to
another was an older side project, and it is likely that it only
supports a limited subset of formulas and theories.

> Secondly, even when I do not use the PrecisionConverter (by setting the
> options 'cpa.predicate.encodeBitvectorAs = INTEGER' and
> 'options.encodePredicates = PrecisionConverter.DISABLE'), an error still
> occurs.
> However, the error message differs from the previous one:
>
> org.sosy_lab.cpachecker.cpa.predicate.persistence.PredicatePersistenceUtils$
> PredicateParsingFailedException: Parsing failed in line 8 of predmap.txt:
> unrecognized text: :
> at org.sosy_lab.cpachecker.cpa.predicate.persistence.
> PredicateMapParser.parsePredicates(PredicateMapParser.java:261)
> at org.sosy_lab.cpachecker.cpa.predicate.persistence.
> PredicateMapParser.parsePredicates(PredicateMapParser.java:118)
>
> This issue seems to be related to the util/predicates/precisionConverter/FormulaParser.java
> code, which I am unable to fully interpret.

FormulaParser should not be used at all in this configuration.
We pass the formula to the SMT solver that is used and let it parse it.
The predmap.txt that you sent in your original mail contains invalid
SMTLIB definitions, at least according to MathSAT.
Identifiers with :: need to be quoted within |...|.
The syntax for an array type is (Array Int Int), and there are some
missing parentheses.
After fixing that, CPAchecker can parse the file.

> Do I need to provide predicates in the form of bitvectors directly?

That is a good question.
In the default settings (i.e., bitvector usage), the predicates have to
be based on bitvectors as well (except with encodePredicates, for which
I do not know how well it works).
If you use encodeBitvectorAs=INTEGER the predicates should be written
with integers, and I think this should work, but likely this is even
less often used and tried out than the BV case.

I would recommend to try this out with a simpler example.
For example, take doc/examples/example.c and and verify it
(with --predicateAnalysis for bitvectors or --predicateAnalysis-linear
for integers), take the resulting predmap.txt file and pass it back to
CPAchecker as initial predicates.
If everything works, you get "Number of CEGAR refinements: 0" in the
statistics of CPAchecker (--stats or output/Statistics.txt).
A quick check seems to indicate that this works for
--predicateAnalysis-linear and doc/examples/example.c. So you can build
on this and try out more complex programs and predicate with heap data
or translation of predicates.

I hope this helps!

Greetings
Philipp

[Yoel Kim]

Dear  Philipp Wendler,

Thank you for your answer! It was very helpful.

I have another question about --predicateAnalysis-linear. In this configuration, it uses cpa.predicate.handleFieldAccess = false with the comment: "Precise handling of structs only possible with bitvectors." However, I don’t fully understand the meaning of this comment. Could you explain it in more detail? What happens if I use this option? Is it also related to arrays?

Best Regards,

Yoel

2024년 11월 30일 토요일 오전 12시 18분 48초 UTC+9에 Philipp Wendler님이 작성:

[Philipp Wendler]

Dear Yoel,

Am 02.01.25 um 07:21 schrieb Yoel Kim:

>
> I have another question about --predicateAnalysis-linear. In this
> configuration, it uses cpa.predicate.handleFieldAccess = false with the
> comment: "Precise handling of structs only possible with bitvectors."
> However, I don’t fully understand the meaning of this comment. Could you
> explain it in more detail? What happens if I use this option? Is it also
> related to arrays?

If you have structs in your program and you use
--predicateAnalysis-linear, expect that the modelling of these structs
is not fully correct. Basic usage may work, but especially with aliasing
or copying whole structs not everything will be handled correctly IIRC.
I think this is not related to arrays.