Some valid terms cannot be parsed

In the new version of the term tests for Skink I’m using the ScalaSMT parser to parse the expected terms. This means we can write tests like this:

val i = s"%z = and i$bits %x, $num"
test(s"$i (math)") {
    hasMathTerm(insn"$i", term"(= %z@0 (mod %x@0 ${num + 1}))")
}

where num and bits vary. In this code “insn” and “term” are Scala string interpolators that invoke the ScalaLLVM instruction parser and the ScalaSMT term parser, respectively.

The problem is that when I parse a term like this:

(= %z@0 (bvuge %x@0 %y@0))

I get this:

QIdAndTermsTerm(SimpleQId(SymbolId(SSymbol(bvuge))),List(ConstantTerm(DecBVLit(BVvalue(1),64)), ConstantTerm(DecBVLit(BVvalue(2),64))))

instead of what I expect which is this:

BVUGreaterThanEqualTerm(ConstantTerm(DecBVLit(BVvalue(1),64)),ConstantTerm(DecBVLit(BVvalue(2),64)))

I think the problem is that BVUGreaterThanEqualTerm and others like it don't appear on the RHS of the Term production, so they are never considered when parsing a term.

This was slightly tricky to spot since the two terms pretty-print the same, so my tests fail with messages like:

(bvuge (_ bv1 64) (_ bv2 64)) was not the same term as (bvuge (_ bv1 64) (_ bv2 64))

Comments (4)