From cd19555063db0ac8eada4dad943a0854a1cafb6c Mon Sep 17 00:00:00 2001
From: laurenzlevi <laurenzlevi@users.noreply.github.com>
Date: Tue, 16 Jan 2024 10:56:59 +0100
Subject: [PATCH] Experimental error message generation

- Implemented better error message generation on choice parsers
- Upgraded  to petitparser 2.4.0
- Upgraded to Java 11
---
 gradle/libs.versions.toml                      |  4 ++--
 .../tools/aqua/konstraints/parser/Parser.kt    |  6 ++++--
 .../tools/aqua/konstraints/ParserTests.kt      | 18 ++++++++++++++++++
 3 files changed, 24 insertions(+), 4 deletions(-)

diff --git a/gradle/libs.versions.toml b/gradle/libs.versions.toml
index f09ea162..6c40f779 100644
--- a/gradle/libs.versions.toml
+++ b/gradle/libs.versions.toml
@@ -14,7 +14,7 @@
 #  See the License for the specific language governing permissions and
 #  limitations under the License.
 [versions]
-java-jdk = "9"
+java-jdk = "11"
 kotlin = "1.9.21"
 nodejs = "20.5.1"
 prettier-toml = "0.3.1"
@@ -35,7 +35,7 @@ versions = { id = "com.github.ben-manes.versions", version = "0.50.0" }
 junit-bom = { group = "org.junit", name = "junit-bom", version = "5.10.1" }
 junit-jupiter = { group = "org.junit.jupiter", name = "junit-jupiter" } # version from BOM
 z3-turnkey = { group = "tools.aqua", name = "z3-turnkey", version = "4.12.2.1" }
-petitparser-core = { group = "com.github.petitparser", name = "petitparser-core", version = "2.3.1" }
+petitparser-core = { group = "com.github.petitparser", name = "petitparser-core", version = "2.4.0" }
 kotlin-coroutines = { group = "org.jetbrains.kotlinx", name = "kotlinx-coroutines-core", version = "1.8.0-RC" }
 
 [bundles]
diff --git a/src/main/kotlin/tools/aqua/konstraints/parser/Parser.kt b/src/main/kotlin/tools/aqua/konstraints/parser/Parser.kt
index 3ae06026..ab57821e 100644
--- a/src/main/kotlin/tools/aqua/konstraints/parser/Parser.kt
+++ b/src/main/kotlin/tools/aqua/konstraints/parser/Parser.kt
@@ -18,6 +18,7 @@
 
 package tools.aqua.konstraints.parser
 
+import org.petitparser.context.Result
 import java.math.BigDecimal
 import org.petitparser.context.Token
 import org.petitparser.parser.Parser
@@ -28,6 +29,7 @@ import org.petitparser.parser.primitive.CharacterParser.anyOf
 import org.petitparser.parser.primitive.CharacterParser.of
 import org.petitparser.parser.primitive.CharacterParser.range
 import org.petitparser.parser.primitive.StringParser.of
+import org.petitparser.utils.FailureJoiner
 import tools.aqua.konstraints.CheckSat
 
 operator fun Parser.plus(other: Parser): ChoiceParser = or(other)
@@ -400,8 +402,8 @@ object Parser {
               rparen)
           .map { results: ArrayList<Any> -> "(set-logic)" }
 
-  val command =
-      assertCMD + checkSatCMD + declareConstCMD + declareFunCMD + exitCMD + setInfoCMD + setLogicCMD
+  val command = ChoiceParser(FailureJoiner.SelectFarthest(), assertCMD, checkSatCMD, declareConstCMD, declareFunCMD, exitCMD, setInfoCMD, setLogicCMD)
+
   val script = command.star().end()
 
   // TODO missing commands
diff --git a/src/test/kotlin/tools/aqua/konstraints/ParserTests.kt b/src/test/kotlin/tools/aqua/konstraints/ParserTests.kt
index d050d038..9dcef142 100644
--- a/src/test/kotlin/tools/aqua/konstraints/ParserTests.kt
+++ b/src/test/kotlin/tools/aqua/konstraints/ParserTests.kt
@@ -22,6 +22,7 @@ import java.lang.Exception
 import org.junit.jupiter.api.TestInstance
 import org.junit.jupiter.params.ParameterizedTest
 import org.junit.jupiter.params.provider.ValueSource
+import org.petitparser.context.Failure
 import org.petitparser.context.ParseError
 import tools.aqua.konstraints.parser.*
 
@@ -58,6 +59,23 @@ class ParserTests {
     }
   }
 
+    @ParameterizedTest
+    @ValueSource(
+        strings =
+        [
+            "(declare-fun A Bool)",
+            "(assert (not (= (bvlshr s (bvshl t #b00000000000000000000000000000000)) (bvlshr s t)))"
+        ]
+    )
+    fun testIllegalCommands(command: String) {
+        val result = Parser.command.parse(command)
+        assert(result.isFailure)
+
+        println(result.message)
+        println(result.position)
+        println(result.buffer)
+    }
+
   @ParameterizedTest
   @ValueSource(
       strings =