Skip to content

Commit 32e2635

Browse files
ailrstailrst
authored
remove duplicate eq ops (#419)
* remove duplicate eq ops * scalafmt * fix exprToPredicate * fix bvconcat * update interferencedomain
1 parent 59f1f2b commit 32e2635

30 files changed

+297
-327
lines changed

‎src/main/scala/analysis/GammaDomains.scala

Lines changed: 13 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -158,12 +158,12 @@ class PredicateDomain(summaries: Procedure => ProcedureSummary) extends Predicat
158158
case m: MemoryStore => b
159159
case a: Assume => {
160160
if (a.checkSecurity) {
161-
and(b, exprToPredicate(a.body).get, lowExpr(a.body)).simplify
161+
and(b, expectPredicate(a.body), lowExpr(a.body)).simplify
162162
} else {
163-
and(b, exprToPredicate(a.body).get).simplify
163+
and(b, expectPredicate(a.body)).simplify
164164
}
165165
}
166-
case a: Assert => and(b, exprToPredicate(a.body).get).simplify
166+
case a: Assert => and(b, expectPredicate(a.body)).simplify
167167
case i: IndirectCall => top
168168
case c: DirectCall =>
169169
c.actualParams.foldLeft(Conj(summaries(c.target).requires.map(_.pred).toSet).simplify) { case (p, (v, e)) =>
@@ -186,6 +186,13 @@ class PredicateDomain(summaries: Procedure => ProcedureSummary) extends Predicat
186186
override def fromPred(p: Predicate): Predicate = p
187187
}
188188

189+
private def expectPredicate(orig: Expr): Predicate = {
190+
exprToPredicate(orig) match {
191+
case Some(p) => p
192+
case None => throw Exception(s"Expected to be able to construct predicate for: $orig")
193+
}
194+
}
195+
189196
/**
190197
* An abstract domain which computes conditions (as predicates) for assertions (including the check that gammas are low on branches) to be violated.
191198
*
@@ -217,12 +224,12 @@ class WpDualDomain(summaries: Procedure => ProcedureSummary) extends PredicateEn
217224
case m: MemoryStore => b
218225
case a: Assume => {
219226
if (a.checkSecurity) {
220-
or(and(b, exprToPredicate(a.body).get), not(lowExpr(a.body))).simplify
227+
or(and(b, expectPredicate(a.body)), not(lowExpr(a.body))).simplify
221228
} else {
222-
and(b, exprToPredicate(a.body).get).simplify
229+
and(b, expectPredicate(a.body)).simplify
223230
}
224231
}
225-
case a: Assert => or(b, not(exprToPredicate(a.body).get)).simplify
232+
case a: Assert => or(b, not(expectPredicate(a.body))).simplify
226233
case i: IndirectCall => bot
227234
case c: DirectCall =>
228235
not(c.actualParams.foldLeft(Conj(summaries(c.target).requires.map(_.pred).toSet).simplify) { case (p, (v, e)) =>

‎src/main/scala/analysis/IrreducibleLoops.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,7 +2,7 @@ package analysis
22

33
import scala.annotation.tailrec
44
import ir.{Block, Command, IntraProcIRCursor, Program, Procedure, GoTo, IRWalk}
5-
import ir.{LocalAssign, Assume, IntLiteral, IntType, IntEQ, BoolOR, LocalVar, BinaryExpr}
5+
import ir.{LocalAssign, Assume, IntLiteral, IntType, EQ, BoolOR, LocalVar, BinaryExpr}
66
import util.intrusive_list.IntrusiveList
77
import util.StaticAnalysisLogger
88

@@ -376,7 +376,7 @@ object LoopTransform {
376376

377377
P_e.groupBy(_.to).map { (destBlock, origins) =>
378378
val idexs = origins.map { b =>
379-
BinaryExpr(IntEQ, LocalVar("FromEntryIdx", IntType), IntLiteral(BigInt(entryids(b.from))))
379+
BinaryExpr(EQ, LocalVar("FromEntryIdx", IntType), IntLiteral(BigInt(entryids(b.from))))
380380
}
381381
idexs.toList match {
382382
case Nil => ()

‎src/main/scala/analysis/KnownBits.scala

Lines changed: 2 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -613,16 +613,12 @@ class TNumDomain extends AbstractDomain[Map[Variable, TNum]] {
613613
case BVSLE => tn1.TSLE(tn2)
614614
case BVSGT => tn1.TSGT(tn2)
615615
case BVSGE => tn1.TSGE(tn2)
616-
case BVEQ => tn1.TEQ(tn2)
617-
case BVNEQ => tn1.TNEQ(tn2)
618616
case BVCONCAT => tn1.TCONCAT(tn2)
619617
case IntADD => tn1.TADD(tn2)
620618
case IntMUL => tn1.TMUL(tn2)
621619
case IntSUB => tn1.TSUB(tn2)
622620
case IntDIV => tn1.TSDIV(tn2)
623621
case IntMOD => tn1.TSMOD(tn2)
624-
case IntEQ => tn1.TEQ(tn2)
625-
case IntNEQ => tn1.TNEQ(tn2)
626622
case IntLT => tn1.TSLT(tn2)
627623
case IntLE => tn1.TSLE(tn2)
628624
case IntGT => tn1.TSGT(tn2)
@@ -632,12 +628,9 @@ class TNumDomain extends AbstractDomain[Map[Variable, TNum]] {
632628

633629
def evaluateBoolBinOp(op: BoolBinOp, tn1: TNum, tn2: TNum): TNum = {
634630
op match {
635-
case BoolEQ => tn1.TEQ(tn2)
636-
case BoolNEQ => tn1.TNEQ(tn2)
637631
case BoolAND => tn1.TAND(tn2)
638632
case BoolOR => tn1.TOR(tn2)
639633
case BoolIMPLIES => (tn1.TOR(tn2.TNOT()))
640-
case BoolEQUIV => tn1.TEQ(tn2)
641634
}
642635
}
643636

@@ -679,6 +672,8 @@ class TNumDomain extends AbstractDomain[Map[Variable, TNum]] {
679672
val arg2TNum = evaluateExprToTNum(s, arg2)
680673

681674
(op, arg1TNum, arg2TNum) match {
675+
case (EQ, tn1, tn2) => tn1.TEQ(tn2)
676+
case (NEQ, tn1, tn2) => tn1.TNEQ(tn2)
682677
case (opVal: BVBinOp, tnum1: TNum, tnum2: TNum) => evaluateValueBinOp(opVal, tnum1, tnum2)
683678
case (opVal: IntBinOp, tnum1: TNum, tnum2: TNum) => evaluateValueBinOp(opVal, tnum1, tnum2)
684679
case (opVal: BoolBinOp, tnum1: TNum, tnum2: TNum) => evaluateBoolBinOp(opVal, tnum1, tnum2)

‎src/main/scala/analysis/Lattice.scala

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -312,6 +312,8 @@ class ValueSetLattice[T] extends Lattice[ValueSet[T]] {
312312

313313
def applyOp(op: BinOp, lhs: ValueSet[T], rhs: Either[ValueSet[T], BitVecLiteral]): ValueSet[T] = {
314314
op match
315+
case EQ => applyOp(EQ, lhs, rhs)
316+
case NEQ => applyOp(NEQ, lhs, rhs)
315317
case bvOp: BVBinOp =>
316318
bvOp match
317319
case BVAND => ???
@@ -346,17 +348,12 @@ class ValueSetLattice[T] extends Lattice[ValueSet[T]] {
346348
case BVSLE => ???
347349
case BVSGT => ???
348350
case BVSGE => ???
349-
case BVEQ => ???
350-
case BVNEQ => ???
351351
case BVCONCAT => ???
352352
case boolOp: BoolBinOp =>
353353
boolOp match
354-
case BoolEQ => applyOp(BVEQ, lhs, rhs)
355-
case BoolNEQ => applyOp(BVNEQ, lhs, rhs)
356354
case BoolAND => applyOp(BVAND, lhs, rhs)
357355
case BoolOR => applyOp(BVOR, lhs, rhs)
358356
case BoolIMPLIES => ???
359-
case BoolEQUIV => ???
360357
case intOp: IntBinOp =>
361358
applyOp(intOp.toBV, lhs, rhs)
362359
}

‎src/main/scala/analysis/NumericalDomains.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -184,8 +184,8 @@ class IntervalDomain(
184184
else if s.size == 1 then fromPred(s.head)
185185
else s.tail.foldLeft(fromPred(s.head)) { (i, p) => i.join(fromPred(p)) }
186186

187-
case BVCmp(BVEQ, BVTerm.Lit(x), BVTerm.Var(v)) => top + (v -> ConcreteInterval(bvto(x), bvto(x), x.size))
188-
case BVCmp(BVEQ, BVTerm.Var(v), BVTerm.Lit(x)) => top + (v -> ConcreteInterval(bvto(x), bvto(x), x.size))
187+
case BVCmp(EQ, BVTerm.Lit(x), BVTerm.Var(v)) => top + (v -> ConcreteInterval(bvto(x), bvto(x), x.size))
188+
case BVCmp(EQ, BVTerm.Var(v), BVTerm.Lit(x)) => top + (v -> ConcreteInterval(bvto(x), bvto(x), x.size))
189189

190190
case BVCmp(BVSLE, BVTerm.Lit(x), BVTerm.Var(v)) if signed =>
191191
top + (v -> ConcreteInterval(bvto(x), inf(x.size), x.size))

‎src/main/scala/analysis/procedure_summaries/Predicate.scala

Lines changed: 49 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -273,8 +273,8 @@ enum Predicate {
273273
case Not(p: Atomic & Predicate) extends Predicate with Atomic
274274
case Conj(s: Set[Predicate])
275275
case Disj(s: Set[Predicate])
276-
case BVCmp(op: BVCmpOp, x: BVTerm, y: BVTerm) extends Predicate with Atomic
277-
case GammaCmp(op: BoolCmpOp, x: GammaTerm, y: GammaTerm) extends Predicate with Atomic
276+
case BVCmp(op: BVCmpOp | PolyCmp, x: BVTerm, y: BVTerm) extends Predicate with Atomic
277+
case GammaCmp(op: BoolCmpOp | PolyCmp, x: GammaTerm, y: GammaTerm) extends Predicate with Atomic
278278

279279
private var simplified: Boolean = false
280280

@@ -578,19 +578,19 @@ enum Predicate {
578578
case Conj(s2) => cur - p ++ s2
579579
case Not(p) if cur.contains(p) => Set(False)
580580
case BVCmp(BVSLE, a, b) if cur.contains(BVCmp(BVSLE, b, a)) =>
581-
cur - p - BVCmp(BVSLE, b, a) + BVCmp(BVEQ, a, b).simplify
581+
cur - p - BVCmp(BVSLE, b, a) + BVCmp(EQ, a, b).simplify
582582
case BVCmp(BVSLE, a, b) if cur.contains(BVCmp(BVSGE, a, b)) =>
583-
cur - p - BVCmp(BVSGE, a, b) + BVCmp(BVEQ, a, b).simplify
583+
cur - p - BVCmp(BVSGE, a, b) + BVCmp(EQ, a, b).simplify
584584
case BVCmp(BVSGE, a, b) if cur.contains(BVCmp(BVSGE, b, a)) =>
585-
cur - p - BVCmp(BVSGE, b, a) + BVCmp(BVEQ, a, b).simplify
585+
cur - p - BVCmp(BVSGE, b, a) + BVCmp(EQ, a, b).simplify
586586
case BVCmp(BVULE, a, b) if cur.contains(BVCmp(BVULE, b, a)) =>
587-
cur - p - BVCmp(BVULE, b, a) + BVCmp(BVEQ, a, b).simplify
587+
cur - p - BVCmp(BVULE, b, a) + BVCmp(EQ, a, b).simplify
588588
case BVCmp(BVULE, a, b) if cur.contains(BVCmp(BVUGE, a, b)) =>
589-
cur - p - BVCmp(BVUGE, a, b) + BVCmp(BVEQ, a, b).simplify
589+
cur - p - BVCmp(BVUGE, a, b) + BVCmp(EQ, a, b).simplify
590590
case BVCmp(BVUGE, a, b) if cur.contains(BVCmp(BVUGE, b, a)) =>
591-
cur - p - BVCmp(BVUGE, b, a) + BVCmp(BVEQ, a, b).simplify
591+
cur - p - BVCmp(BVUGE, b, a) + BVCmp(EQ, a, b).simplify
592592
case GammaCmp(BoolIMPLIES, a, b) if cur.contains(GammaCmp(BoolIMPLIES, b, a)) =>
593-
cur - p - GammaCmp(BoolIMPLIES, b, a) + GammaCmp(BoolEQ, a, b).simplify
593+
cur - p - GammaCmp(BoolIMPLIES, b, a) + GammaCmp(EQ, a, b).simplify
594594
case Disj(s2) if s.intersect(s2).nonEmpty => cur - p
595595
case _ => cur
596596
}
@@ -662,22 +662,22 @@ enum Predicate {
662662
case BVCmp(BVUGT, a, b) if cur.contains(BVCmp(BVUGE, b, a)) => cur - p - BVCmp(BVUGE, b, a) + True
663663
case BVCmp(BVUGT, a, b) if cur.contains(BVCmp(BVULE, a, b)) => cur - p - BVCmp(BVULE, a, b) + True
664664

665-
case BVCmp(BVSLT, a, b) if cur.contains(BVCmp(BVEQ, a, b)) =>
666-
cur - p - BVCmp(BVEQ, a, b) + BVCmp(BVSLE, a, b).simplify
667-
case BVCmp(BVSLT, a, b) if cur.contains(BVCmp(BVEQ, b, a)) =>
668-
cur - p - BVCmp(BVEQ, b, a) + BVCmp(BVSLE, a, b).simplify
669-
case BVCmp(BVSGT, a, b) if cur.contains(BVCmp(BVEQ, a, b)) =>
670-
cur - p - BVCmp(BVEQ, a, b) + BVCmp(BVSGE, a, b).simplify
671-
case BVCmp(BVSGT, a, b) if cur.contains(BVCmp(BVEQ, b, a)) =>
672-
cur - p - BVCmp(BVEQ, b, a) + BVCmp(BVSGE, a, b).simplify
673-
case BVCmp(BVULT, a, b) if cur.contains(BVCmp(BVEQ, a, b)) =>
674-
cur - p - BVCmp(BVEQ, a, b) + BVCmp(BVULE, a, b).simplify
675-
case BVCmp(BVULT, a, b) if cur.contains(BVCmp(BVEQ, b, a)) =>
676-
cur - p - BVCmp(BVEQ, b, a) + BVCmp(BVULE, a, b).simplify
677-
case BVCmp(BVUGT, a, b) if cur.contains(BVCmp(BVEQ, a, b)) =>
678-
cur - p - BVCmp(BVEQ, a, b) + BVCmp(BVUGE, a, b).simplify
679-
case BVCmp(BVUGT, a, b) if cur.contains(BVCmp(BVEQ, b, a)) =>
680-
cur - p - BVCmp(BVEQ, b, a) + BVCmp(BVUGE, a, b).simplify
665+
case BVCmp(BVSLT, a, b) if cur.contains(BVCmp(EQ, a, b)) =>
666+
cur - p - BVCmp(EQ, a, b) + BVCmp(BVSLE, a, b).simplify
667+
case BVCmp(BVSLT, a, b) if cur.contains(BVCmp(EQ, b, a)) =>
668+
cur - p - BVCmp(EQ, b, a) + BVCmp(BVSLE, a, b).simplify
669+
case BVCmp(BVSGT, a, b) if cur.contains(BVCmp(EQ, a, b)) =>
670+
cur - p - BVCmp(EQ, a, b) + BVCmp(BVSGE, a, b).simplify
671+
case BVCmp(BVSGT, a, b) if cur.contains(BVCmp(EQ, b, a)) =>
672+
cur - p - BVCmp(EQ, b, a) + BVCmp(BVSGE, a, b).simplify
673+
case BVCmp(BVULT, a, b) if cur.contains(BVCmp(EQ, a, b)) =>
674+
cur - p - BVCmp(EQ, a, b) + BVCmp(BVULE, a, b).simplify
675+
case BVCmp(BVULT, a, b) if cur.contains(BVCmp(EQ, b, a)) =>
676+
cur - p - BVCmp(EQ, b, a) + BVCmp(BVULE, a, b).simplify
677+
case BVCmp(BVUGT, a, b) if cur.contains(BVCmp(EQ, a, b)) =>
678+
cur - p - BVCmp(EQ, a, b) + BVCmp(BVUGE, a, b).simplify
679+
case BVCmp(BVUGT, a, b) if cur.contains(BVCmp(EQ, b, a)) =>
680+
cur - p - BVCmp(EQ, b, a) + BVCmp(BVUGE, a, b).simplify
681681

682682
case Conj(s2) if s.intersect(s2).nonEmpty => cur - p
683683
case _ => cur
@@ -695,15 +695,15 @@ enum Predicate {
695695
import BVTerm.*
696696
(op, a.simplify, b.simplify) match {
697697
case (op, BVTerm.Lit(a), BVTerm.Lit(b)) => if evalBVLogBinExpr(op, a, b) then True else False
698-
case (BVEQ, a, b) if a == b => True
699-
case (BVEQ, a, Uop(BVNEG, b)) => BVCmp(BVEQ, Bop(BVADD, a, b), BVTerm.Lit(BitVecLiteral(0, a.size))).simplify
700-
case (BVEQ, l: BVTerm.Lit, v: Var) => BVCmp(BVEQ, v, l) // Canonical form-ish (to remove duplicate terms
698+
case (EQ, a, b) if a == b => True
699+
case (EQ, a, Uop(BVNEG, b)) => BVCmp(EQ, Bop(BVADD, a, b), BVTerm.Lit(BitVecLiteral(0, a.size))).simplify
700+
case (EQ, l: BVTerm.Lit, v: Var) => BVCmp(EQ, v, l) // Canonical form-ish (to remove duplicate terms
701701
case (op, a, b) => BVCmp(op, a, b)
702702
}
703703
case GammaCmp(op, a, b) =>
704704
(op, a.simplify, b.simplify) match {
705705
case (BoolIMPLIES, a, b) if a == b => True
706-
case (BoolEQ, a, b) if a == b => True
706+
case (EQ, a, b) if a == b => True
707707
case (op, a, b) => GammaCmp(op, a, b)
708708
}
709709
case _ => this
@@ -748,22 +748,21 @@ object Predicate {
748748

749749
def or(ps: Predicate*): Predicate = Disj(ps.toSet).flatten
750750

751-
def bop(op: BoolBinOp, a: Predicate, b: Predicate): Predicate = {
751+
def bop(op: (BoolBinOp | PolyCmp), a: Predicate, b: Predicate): Predicate = {
752752
op match {
753-
case BoolEQ => or(and(not(a), not(b)), and(a, b))
754-
case BoolNEQ => or(and(not(a), b), and(a, not(b)))
753+
case EQ => or(and(not(a), not(b)), and(a, b))
754+
case NEQ => or(and(not(a), b), and(a, not(b)))
755755
case BoolAND => and(a, b)
756756
case BoolOR => or(a, b)
757757
case BoolIMPLIES => or(not(a), b)
758-
case BoolEQUIV => bop(BoolEQ, a, b)
759758
}
760759
}
761760

762761
def implies(a: Predicate, b: Predicate): Predicate = bop(BoolIMPLIES, a, b)
763762

764763
def gammaLeq(a: GammaTerm, b: GammaTerm) = GammaCmp(BoolIMPLIES, b, a)
765764
def gammaGeq(a: GammaTerm, b: GammaTerm) = GammaCmp(BoolIMPLIES, a, b)
766-
def gammaEq(a: GammaTerm, b: GammaTerm) = GammaCmp(BoolEQ, a, b)
765+
def gammaEq(a: GammaTerm, b: GammaTerm) = GammaCmp(EQ, a, b)
767766
}
768767

769768
/**
@@ -804,10 +803,22 @@ def exprToGammaTerm(e: Expr): Option[GammaTerm] = e match {
804803
def exprToPredicate(e: Expr): Option[Predicate] = e match {
805804
case b: BoolLit => Some(Predicate.Lit(b))
806805
case UnaryExpr(BoolNOT, arg) => exprToPredicate(arg).map(p => Predicate.not(p))
807-
case BinaryExpr(op: BoolBinOp, arg1, arg2) =>
808-
exprToPredicate(arg1).flatMap(p => exprToPredicate(arg2).map(q => Predicate.bop(op, p, q)))
809-
case BinaryExpr(op: BVCmpOp, arg1, arg2) =>
810-
exprToBVTerm(arg1).flatMap(p => exprToBVTerm(arg2).map(q => Predicate.BVCmp(op, p, q)))
806+
case BinaryExpr(op: (PolyCmp | BVCmpOp | BoolCmpOp), arg1, arg2) =>
807+
(
808+
List(arg1, arg2).map(e =>
809+
e.getType match {
810+
case BoolType => exprToPredicate(e)
811+
case _: BitVecType => exprToBVTerm(e)
812+
case _ => None
813+
}
814+
),
815+
op
816+
) match {
817+
case (Some(l: Predicate) :: Some(r: Predicate) :: Nil, op: (BoolCmpOp | PolyCmp)) => Some(Predicate.bop(op, l, r))
818+
case (Some(l: BVTerm) :: Some(r: BVTerm) :: Nil, op: (BVCmpOp | PolyCmp)) => Some(Predicate.BVCmp(op, l, r))
819+
case _ => None
820+
}
821+
811822
case _ => None
812823
}
813824

‎src/main/scala/analysis/rely_guarantee_generation/InterferenceDomains.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -242,7 +242,7 @@ class MonotonicityDomain[S](stateLattice: InterferenceCompatibleLattice[S], stat
242242
// apply assume statement to add constraints to y
243243
val yConstraints = d match {
244244
case Direction.Bot =>
245-
stateTransfer(postState, Assume(BinaryExpr(IntEQ, y, v)))
245+
stateTransfer(postState, Assume(BinaryExpr(EQ, y, v)))
246246
case Direction.Increasing =>
247247
stateTransfer(postState, Assume(BinaryExpr(BVSGE, y, v)))
248248
case Direction.Decreasing =>

‎src/main/scala/boogie/BExpr.scala

Lines changed: 10 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -316,6 +316,7 @@ case class UnaryBExpr(op: UnOp, arg: BExpr) extends BExpr {
316316
case class BinaryBExpr(op: BinOp, arg1: BExpr, arg2: BExpr) extends BExpr {
317317
override def getType: BType = (op, arg1.getType, arg2.getType) match {
318318
case (_: BoolBinOp, BoolBType, BoolBType) => BoolBType
319+
case (EQ | NEQ, _, _) => BoolBType
319320
case (binOp: BVBinOp, bv1: BitVecBType, bv2: BitVecBType) =>
320321
binOp match {
321322
case BVCONCAT =>
@@ -339,13 +340,11 @@ case class BinaryBExpr(op: BinOp, arg1: BExpr, arg2: BExpr) extends BExpr {
339340
} else {
340341
throw new Exception(s"bitvector size mismatch: $arg1, $arg2")
341342
}
342-
case BVEQ | BVNEQ =>
343-
BoolBType
344343
}
345344
case (intOp: IntBinOp, IntBType, IntBType) =>
346345
intOp match {
347346
case IntADD | IntSUB | IntMUL | IntDIV | IntMOD => IntBType
348-
case IntEQ | IntNEQ | IntLT | IntLE | IntGT | IntGE => BoolBType
347+
case IntLT | IntLE | IntGT | IntGE => BoolBType
349348
}
350349
case _ =>
351350
throw new Exception("type mismatch, operator " + op + " type doesn't match args: (" + arg1 + ", " + arg2 + ")")
@@ -370,10 +369,12 @@ case class BinaryBExpr(op: BinOp, arg1: BExpr, arg2: BExpr) extends BExpr {
370369
next match
371370
case b: BinaryBExpr =>
372371
b.op match {
372+
case EQ => infix(b)
373+
case NEQ => infix(b)
373374
case bOp: BoolBinOp => infix(b)
374375
case bOp: BVBinOp =>
375376
bOp match {
376-
case BVEQ | BVNEQ | BVCONCAT => infix(b)
377+
case BVCONCAT => infix(b)
377378
case _ => prefix(b)
378379
}
379380
case bOp: IntBinOp => infix(b)
@@ -386,9 +387,10 @@ case class BinaryBExpr(op: BinOp, arg1: BExpr, arg2: BExpr) extends BExpr {
386387

387388
override def toString: String = op match {
388389
case bOp: BoolBinOp => s"($arg1 $bOp $arg2)"
390+
case EQ | NEQ => s"($arg1 $op $arg2)"
389391
case bOp: BVBinOp =>
390392
bOp match {
391-
case BVEQ | BVNEQ | BVCONCAT =>
393+
case BVCONCAT =>
392394
s"($arg1 $bOp $arg2)"
393395
case _ =>
394396
s"bv$bOp$inSize($arg1, $arg2)"
@@ -398,9 +400,10 @@ case class BinaryBExpr(op: BinOp, arg1: BExpr, arg2: BExpr) extends BExpr {
398400

399401
override def functionOps: Set[FunctionOp] = {
400402
val thisFn = op match {
403+
case EQ | NEQ => Set()
401404
case b: BVBinOp =>
402405
b match {
403-
case BVEQ | BVNEQ | BVCONCAT => Set()
406+
case BVCONCAT => Set()
404407
case _ =>
405408
Set(
406409
BVFunctionOp(s"bv$b$inSize", s"bv$b", List(BParam(arg1.getType), BParam(arg2.getType)), BParam(getType))
@@ -752,7 +755,7 @@ case class SpecGlobal(
752755
override val toAddrVar: BVar = BVariable("$" + s"${name}_addr", BitVecBType(64), Scope.Const)
753756
override val toOldVar: BVar = BVariable(s"${name}_old", BitVecBType(size), Scope.Local)
754757
override val toOldGamma: BVar = BVariable(s"Gamma_${name}_old", BoolBType, Scope.Local)
755-
val toAxiom: BAxiom = BAxiom(BinaryBExpr(BoolEQ, toAddrVar, BitVecBLiteral(address, 64)), List.empty)
758+
val toAxiom: BAxiom = BAxiom(BinaryBExpr(EQ, toAddrVar, BitVecBLiteral(address, 64)), List.empty)
756759
override def acceptVisit(visitor: BVisitor): BExpr = visitor.visitSpecGlobal(this)
757760
}
758761

0 commit comments

Comments
 (0)