Add benchmarks, rework test scripts

benchmarks/01-pure/10-nil_polymorphism.smt2

@@ -0,0 +1,13 @@
+(set-info :source Astral)
+(set-info :status sat)
+
+(declare-sort Loc 0)
+(declare-heap (Loc Loc))
+
+(declare-const x_ls  LS_t)
+(declare-const x_dls DLS_t)
+(declare-const x_nls NLS_t)
+
+(assert (= nil x_ls x_dls x_nls))
+
+(check-sat)

benchmarks/02-spatial_atoms/13-pointer_sequence_2.smt2

@@ -0,0 +1,17 @@
+(set-info :source Astral)
+(set-info :status sat)
+
+(declare-sort Loc 0)
+(declare-heap (Loc Loc))
+
+(declare-const x1 Loc)
+(declare-const x2 Loc)
+
+(assert
+  (sep
+    (pto x1 x2)
+    (pto x2 nil)
+  )
+)
+
+(check-sat)

benchmarks/03-lists/15-bound-example.smt2

@@ -0,0 +1,28 @@
+(set-info :source Astral)
+(set-info :status unsat)
+
+(declare-sort Loc 0)
+(declare-heap (Loc Loc))
+
+(declare-const a Loc)
+(declare-const b Loc)
+(declare-const c Loc)
+(declare-const d Loc)
+
+(assert
+  (sep
+    (ls a b)
+    (pto b c)
+    (pto c d)
+    (ls d a)
+  )
+)
+
+(assert (not
+  (sep
+    (ls a c)
+    (ls c a)
+  )
+))
+
+(check-sat)

benchmarks/03-lists/16-same_root_sat.smt2

@@ -0,0 +1,18 @@
+(set-info :source Astral)
+(set-info :status sat)
+
+(declare-sort Loc 0)
+(declare-heap (Loc Loc))
+
+(declare-const x Loc)
+(declare-const y1 Loc)
+(declare-const y2 Loc)
+
+(assert
+  (sep
+    (ls x y1)
+    (ls x y2)
+  )
+)
+
+(check-sat)

benchmarks/03-lists/17-same_root_sat2.smt2

@@ -0,0 +1,19 @@
+(set-info :source Astral)
+(set-info :status sat)
+
+(declare-sort Loc 0)
+(declare-heap (Loc Loc))
+
+(declare-const x Loc)
+(declare-const y1 Loc)
+(declare-const y2 Loc)
+
+(assert
+  (sep
+    (distinct y1 y2)
+    (ls x y1)
+    (ls x y2)
+  )
+)
+
+(check-sat)

benchmarks/03-lists/18-same_root_unsat.smt2

@@ -0,0 +1,19 @@
+(set-info :source Astral)
+(set-info :status unsat)
+
+(declare-sort Loc 0)
+(declare-heap (Loc Loc))
+
+(declare-const x Loc)
+(declare-const y1 Loc)
+(declare-const y2 Loc)
+
+(assert
+  (sep
+    (distinct x y1 y2)
+    (ls x y1)
+    (ls x y2)
+  )
+)
+
+(check-sat)

benchmarks/05-wands/config.yaml

@@ -0,0 +1 @@
+ignore: True

benchmarks/06-symbolic_heaps_sat/config.yaml

@@ -0,0 +1 @@
+verify-model: true

benchmarks/09-negative/config.yaml

@@ -0,0 +1,4 @@
+separation: "weak"
+
+#restrict_encodings: ["sets"]
+#restrict_qelims: ["none"]

benchmarks/15-SSL/03-list_length_eq_2_unsat.smt2

@@ -0,0 +1,27 @@
+(set-info :source Astral)
+(set-info :status unsat)
+
+(declare-sort Loc 0)
+(declare-heap (Loc Loc))
+
+(declare-const x Loc)
+(declare-const y Loc)
+
+(assert (ls x y))
+
+(assert
+  (sep
+    (not sep.emp)
+    (not sep.emp)
+  )
+)
+
+(assert (not
+  (sep
+    (not sep.emp)
+    (not sep.emp)
+    (not sep.emp)
+  )
+))
+
+(check-sat)

benchmarks/15-SSL/04-list_length_eq_2_sat.smt2

@@ -0,0 +1,28 @@
+(set-info :source Astral)
+(set-info :status sat)
+
+(declare-sort Loc 0)
+(declare-heap (Loc Loc))
+
+(declare-const x Loc)
+(declare-const y Loc)
+(declare-const z Loc)
+
+(assert (ls x y))
+
+(assert
+  (sep
+    (not sep.emp)
+    (not sep.emp)
+  )
+)
+
+(assert (not
+  (sep
+    (not sep.emp)
+    (not sep.emp)
+    (not sep.emp)
+  )
+))
+
+(check-sat)

benchmarks/15-SSL/config.yaml

@@ -0,0 +1 @@
+separation: "strong"

scripts/run_test_case.py

@@ -0,0 +1,130 @@
+# Runner of a single test case
+#
+# Author: Tomas Dacik (idacik@fit.vut.cz), 2024
+
+import os
+import yaml
+
+from dataclasses import dataclass
+from enum import Enum
+from subprocess import run, PIPE, TimeoutExpired
+
+from utils import *
+
+ASTRAL = "_build/default/main.exe"
+TMP = "/tmp/astral"
+
+
+@dataclass
+class Config:
+    ignore: bool = False
+    verify_model: bool = False  # TODO: implement
+
+    timeout: int = 10
+    backend: str = "z3"
+    encoding: str = "bitvectors"
+    qf_encoding: str = "direct"
+    separation: str = "weak"
+
+    @classmethod
+    def from_file(cls, path):
+        with open(path, "r") as f:
+            json = yaml.safe_load(f)
+
+        kwargs = {
+            key.replace("-", "_"): value for key, value in json.items()
+        }  # if key in vars(Config)}
+        return Config(**kwargs)
+
+    def to_command(self, path):
+        name = os.path.basename(path)
+        # fmt: off
+        return [
+            ASTRAL,
+            "--backend", self.backend,
+            "--encoding", self.encoding,
+            "--qf-encoding", self.qf_encoding,
+            "--separation", self.separation,
+            "--json-output", TMP + name + ".json",
+            path
+        ]
+        # fmt: on
+
+
+class Status(Enum):
+    CORRECT = 0
+    INCORRECT = 1
+    UNKNOWN = 2
+    TIMEOUT = 3
+    ERROR = 4
+
+
+@dataclass
+class Result:
+    name: str
+    status: Status
+    return_code: int = 0
+
+    @classmethod
+    def of_run(cls, name, process):
+        stdout = process.stdout.decode().strip()
+        stderr = process.stderr.decode().strip()
+
+        if process.returncode == 0 and stdout.startswith("unknown"):
+            status = Status.UNKNOWN
+        elif process.returncode == 0:
+            status = Status.CORRECT
+        elif process.returncode == 1:
+            status = Status.INCORRECT
+        else:
+            status = Status.ERROR
+
+        return Result(name, status, process.returncode)
+
+    @classmethod
+    def timeout(cls, name, to):
+        return Result(name, Status.TIMEOUT)
+
+    @property
+    def is_correct(self):
+        return self.status == Status.CORRECT
+
+    @property
+    def is_unknown(self):
+        return self.status in [Status.UNKNOWN, Status.TIMEOUT]
+
+    def is_error(self):
+        return not self.is_correct and not self.is_unknown
+
+    def print(self):
+        if self.status == Status.CORRECT:
+            print_ok(f"[OK] {self.name}")
+        elif self.status == Status.UNKNOWN:
+            print_unknown(f"[UNKNOWN] {self.name}")
+        elif self.status == Status.TIMEOUT:
+            print_unknown(f"[TIMEOUT]: {self.name}")
+        elif self.status == Status.INCORRECT:
+            print_err(f"[INCORRECT]: {self.name}")
+        else:
+            print_err(f"[ERR {self.return_code}]: {self.name}")
+
+
+class TestRunner:
+    def __init__(self, path, config=Config()):
+        self.path = path
+        self.name = os.path.basename(path)
+        self.config = config
+        self.result = None
+
+    def run(self):
+        command = self.config.to_command(self.path)
+        try:
+            process = run(
+                command, timeout=self.config.timeout, stdout=PIPE, stderr=PIPE
+            )
+            result = Result.of_run(self.name, process)
+        except TimeoutExpired as to:
+            result = Result.timeout(self.name, to)
+
+        result.print()
+        return result