gradual-verification / gvc0

Gradually Verified C0
6 stars 5 forks source link

Simplifying runtime check conditions results in an infinite loop #20

Closed icmccorm closed 2 years ago

icmccorm commented 2 years ago

When executing this program, simplifying its runtime checks leads to an infinite loop in the frontend when Logic.simplify(Logic.Disjunction(conditions.toSet)) is called.

// Get all checks (grouped by their location) and simplify their conditions
    val collectedChecks = mutable.ListBuffer[RuntimeCheck]()
    for ((loc, locChecks) <- checks)
      for ((check, conditions) <- locChecks) {
        val simplified = Logic.simplify(Logic.Disjunction(conditions.toSet))
        val condition = convertDisjunction(simplified)

The particular condition that triggers this loop is cVal == c->val

conradz commented 2 years ago

Fixed since we are eliminating condition simplification at least for now