Handle && and || in binary operators (#34)

arrow-kt · Apr 4, 2022 · 6e10eac · 6e10eac
1 parent 8932118
commit 6e10eac
Show file tree

Hide file tree

Showing 2 changed files with 81 additions and 4 deletions.
diff --git a/...n/src/main/kotlin/arrow/meta/plugins/analysis/phases/analysis/solver/check/Expressions.kt b/...n/src/main/kotlin/arrow/meta/plugins/analysis/phases/analysis/solver/check/Expressions.kt
@@ -112,9 +112,8 @@ import arrow.meta.plugins.analysis.phases.analysis.solver.state.checkConditionsI
 import arrow.meta.plugins.analysis.phases.analysis.solver.state.checkInvariant
 import arrow.meta.plugins.analysis.phases.analysis.solver.state.checkInvariantConsistency
 import arrow.meta.plugins.analysis.phases.analysis.solver.valueArgumentExpressions
-import arrow.meta.plugins.analysis.smt.ObjectFormula
+import arrow.meta.plugins.analysis.smt.*
 import arrow.meta.plugins.analysis.smt.renameObjectVariables
-import arrow.meta.plugins.analysis.smt.substituteDeclarationConstraints
 import arrow.meta.plugins.analysis.smt.substituteObjectVariables
 import arrow.meta.plugins.analysis.types.PrimitiveType
 import arrow.meta.plugins.analysis.types.asFloatingLiteral
@@ -1269,6 +1268,27 @@ private fun SolverState.checkBinaryExpression(
         }
       }
     }
+    (operator == "ANDAND" || operator == "OROR") -> {
+      val lhs = solver.makeObjectVariable(newName(data.context, "left", left))
+      val rhs = solver.makeObjectVariable(newName(data.context, "right", right))
+      checkExpressionConstraints(lhs, left, data).checkReturnInfo { stateAfterLhs ->
+        checkExpressionConstraints(rhs, right, data).checkReturnInfo { stateAfterRhs ->
+          cont {
+            when (operator) {
+              "ANDAND" -> solver.boolAnd(listOf(solver.boolValue(lhs), solver.boolValue(rhs)))
+              "OROR" -> solver.boolOr(listOf(solver.boolValue(lhs), solver.boolValue(rhs)))
+              else -> null
+            }?.let {
+              addConstraint(
+                NamedConstraint("boolean operator $operator", it),
+                stateAfterRhs.data.context
+              )
+            }
+            stateAfterRhs
+          }
+        }
+      }
+    }
     else -> fallThrough(associatedVarName, expression, data)
   }
 }

diff --git a/analysis/kotlin-plugin/src/test/kotlin/arrow/meta/plugins/analysis/AnalysisTests.kt b/analysis/kotlin-plugin/src/test/kotlin/arrow/meta/plugins/analysis/AnalysisTests.kt
@@ -1939,8 +1939,65 @@ class AnalysisTests {
          Field(tag, field)
       """(
       withPlugin = { compilesNoUnreachable },
-      withoutPlugin = { compiles },
-      isMultiplatform = true
+      withoutPlugin = { compiles }
+    )
+  }
+
+  @Test
+  fun `double conditional, part 1 (issue #31)`() {
+    """
+      ${imports()}
+      
+      @JvmInline
+      value class String5till10(val value: String) {
+        init {
+          require(value.length >= 5) { "String should be minimal 5 characters" }
+          require(value.length <= 10) { "String should be maximum 10 characters" }
+        }
+      }
+      
+      fun getRandomString(): String = "hello!"
+      
+      // This works
+      fun f() {
+        val value = getRandomString()
+        if (value.length > 6) {
+          if (value.length < 10) {
+            String5till10(value)
+          }
+        }
+      }
+      """(
+      withPlugin = { compilesNoUnreachable },
+      withoutPlugin = { compiles }
+    )
+  }
+
+  @Test
+  fun `double conditional, part 2 (issue #31)`() {
+    """
+      ${imports()}
+      
+      @JvmInline
+      value class String5till10(val value: String) {
+        init {
+          require(value.length >= 5) { "String should be minimal 5 characters" }
+          require(value.length <= 10) { "String should be maximum 10 characters" }
+        }
+      }
+      
+      fun getRandomString(): String = "hello!"
+      
+      // This does not
+      fun f() {
+        val value = getRandomString()
+        if (value.length > 6 && value.length < 10) {
+          String5till10(value)
+        }
+      }
+      """(
+      withPlugin = { compilesNoUnreachable },
+      withoutPlugin = { compiles }
     )
   }
 }