Skip to content

Commit

Permalink
Merge branch 'master' into patch-3
Browse files Browse the repository at this point in the history
  • Loading branch information
@zmylinxi99
zmylinxi99 authored Jun 13, 2024
2 parents 434d7af + 3da485d commit 7072e64
Show file tree
Hide file tree
Showing 16 changed files with 876 additions and 212 deletions.
1 change: 1 addition & 0 deletions .gitignore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -170,3 +170,4 @@ cython_debug/
schema_doc.css
schema_doc.min.js
*.feather
tmp/
25 changes: 12 additions & 13 deletions README.md
View file
Original file line number Diff line number Diff line change
@@ -1,4 +1,4 @@
# smtcomp
# SMT Competition

[![Release](https://img.shields.io/github/v/release/smtcomp/smtcomp.github.io)](https://img.shields.io/github/v/release/smtcomp/smtcomp.github.io)
[![Build status](https://img.shields.io/github/actions/workflow/status/smtcomp/smtcomp.github.io/main.yml?branch=main)](https://github.com/smtcomp/smtcomp.github.io/actions/workflows/main.yml?query=branch%3Amain)
Expand Down Expand Up @@ -38,7 +38,7 @@ make install

## For starting a new SMT-COMP year

Edit the file `smtcomp/defs.py`, in particular `Config.current_year`, `Logic` for adding new logics and `tracks` for new divisions.
Edit the file `smtcomp/defs.py`, in particular `Config.current_year`, `Logic` for adding new logics and `tracks` for new divisions. Reset `Config.NYSE_seed` to `None`, and set the date the New York Stock Exchange Index will be used in `Config.NYSE_date`.

Download the new benchmarks from zenodo, unpack them, unpack the .tar.zst, you should get something like:

Expand Down Expand Up @@ -74,10 +74,9 @@ smtcomp create-benchmarks-list $DIR/zenodo ./data/

The directory `./data/` is the one present in this repository.

## Using the smtcomp tool for selecting the benchmarks
## Using the `smtcomp` tool for selecting the benchmarks

The list of benchmarks and the previous results are in json which are human
readable, but slow to parse (1min). So locally the tool use the feather format. The
The list of benchmarks and the previous results are in `json` which are human-readable, but slow to parse (1min). So locally the tool use the feather format. The
feather files are generated with:

```
Expand All @@ -87,7 +86,7 @@ smtcomp create-cache ./data/
Working with the feather files with [polars](https://docs.pola.rs/) is very fast,
so no more intermediate files are needed.

However statistics can be shown, for example for the selection of single track:
However, statistics can be shown, for example for the selection of single track:

```
smtcomp show-sq-selection-stats ./data/ 0
Expand All @@ -110,7 +109,7 @@ Which outputs:
...
```

## Using the smtcomp tool for generating benchexec
## Using the `smtcomp` tool for generating `benchexec` configuration

#### Generate submissions [Optional]

Expand All @@ -129,37 +128,37 @@ smtcomp show ../tmp/submissions/YicesQS.json
The solver downloaded using:

```
smtcomp download-archive ../tmp/submissions/*.json ../tmp/benchexec/execution
smtcomp download-archive submissions/*.json ../tmp/execution
```

Trivial tests benchmarks generated with:

```
smtcomp generate-benchmarks ../tmp/benchexec/includes/
smtcomp generate-trivial-benchmarks ../tmp/execution/benchmarks
```

The benchexec tasks generated using:

```
smtcomp generate-benchexec ../tmp/submissions/*.json ../tmp/benchexec/includes/all.xml ../tmp/benchexec/execution
smtcomp generate-benchexec submissions/*.json ../tmp/execution
```

The benchexec execution environment generated using:

```
smtcomp prepare-execution ../tmp/benchexec/execution
smtcomp prepare-execution ../tmp/execution
```

Benchexec started using:

```
(cd ../tmp/benchexec/execution; benchexec ../includes/all.xml --read-only-dir / --overlay-dir /home --full-access-dir .. --numOfThreads 8 -M 2GB -c 1)
(cd ../tmp/execution; PYTHONPATH=$(pwd) benchexec SOLVERNAME.xml --read-only-dir / --overlay-dir /home --full-access-dir .. --numOfThreads 8 -M 2GB -c 1)
```

Benchexec in verifier cloud started using:

```
(cd ../tmp/benchexec/execution; PATH_TO_BENCHEXEC/contrib/vcloud-benchmark.py ../includes/all.xml --read-only-dir / --overlay-dir /home --full-access-dir .. --numOfThreads 8 -M 2GB -c 1 --vcloudMaster VCLOUD_MASTER --vcloudClientHeap 500)
(cd ../tmp/execution; PYTHONPATH=$(pwd) PATH_TO_BENCHEXEC/contrib/vcloud-benchmark.py SOLVERNAME.xml --read-only-dir / --overlay-dir /home --full-access-dir .. --numOfThreads 8 -M 2GB -c 1 --vcloudMaster VCLOUD_MASTER --vcloudClientHeap 500)
```

---
Expand Down
4 changes: 4 additions & 0 deletions smtcomp/archive.py
View file
Original file line number Diff line number Diff line change
Expand Up @@ -38,6 +38,10 @@ def is_unpack_present(archive: defs.Archive, dst: Path) -> bool:
return any(True for _ in d.iterdir())


def command_path(command: defs.Command, archive: defs.Archive, dst: Path) -> Path:
return archive_unpack_dir(archive, dst).joinpath(command.binary)


def find_command(command: defs.Command, archive: defs.Archive, dst: Path) -> Path:
d = archive_unpack_dir(archive, dst)
if not (d.exists()):
Expand Down
160 changes: 115 additions & 45 deletions smtcomp/benchexec.py
View file
Original file line number Diff line number Diff line change
@@ -1,14 +1,40 @@
from pathlib import Path
import rich
from os.path import relpath
from typing import List, cast, Dict, Optional

from yattag import Doc, indent

from smtcomp import defs
from smtcomp.archive import find_command
from smtcomp.archive import find_command, archive_unpack_dir, command_path
from pydantic import BaseModel

import shlex
from re import sub


def get_suffix(track: defs.Track) -> str:
match track:
case defs.Track.Incremental:
return "_inc"
case defs.Track.ModelValidation:
return "_model"
case defs.Track.UnsatCore:
return "_unsatcore"
case defs.Track.SingleQuery:
return ""
case _:
raise ValueError("No Cloud or Parallel")


def get_xml_name(s: defs.Submission, track: defs.Track) -> str:
suffix = get_suffix(track)
return sub(r"\W+", "", s.name.lower()) + suffix + ".xml"


def tool_module_name(s: defs.Submission, incremental: bool) -> str:
suffix = "_inc" if incremental else ""
return sub(r"\W+", "", s.name.lower()) + suffix


class CmdTask(BaseModel):
Expand All @@ -17,7 +43,68 @@ class CmdTask(BaseModel):
includesfiles: List[str]


def generate_xml(timelimit_s: int, memlimit_M: int, cpuCores: int, cmdtasks: List[CmdTask], file: Path) -> None:
def generate_benchmark_yml(benchmark: Path, expected_result: Optional[bool], orig_file: Optional[Path]) -> None:
ymlfile = benchmark.with_suffix(".yml")
with ymlfile.open("w") as f:
f.write("format_version: '2.0'\n\n")

f.write(f"input_files: '{str(benchmark.name)}'\n\n")

if orig_file is not None:
f.write(f"# original_files: '{str(orig_file)}'\n\n")

expected_str = "true" if expected_result else "false"
f.write("properties:\n")
f.write(f" - property_file: '../../properties/SMT.prp'\n")
if expected_result is not None:
f.write(f" expected_verdict: {expected_str}\n")


def generate_tool_module(s: defs.Submission, cachedir: Path, incremental: bool) -> None:
name = tool_module_name(s, incremental)
file = cachedir / "tools" / f"{name}.py"

with file.open("w") as f:
if incremental:
base_module = "incremental_tool"
base_class = "IncrementalSMTCompTool"
else:
base_module = "tool"
base_class = "SMTCompTool"
f.write(f"from tools.{base_module} import {base_class}\n\n")
f.write(f"class Tool({base_class}): # type: ignore\n")

f.write(f" NAME = '{s.name}'\n")
if s.command is not None:
assert s.archive is not None
if s.command.compa_starexec:
executable_path = find_command(s.command, s.archive, cachedir)
executable = str(relpath(executable_path, start=str(cachedir)))
else:
executable = str(command_path(s.command, s.archive, Path()))
f.write(f" EXECUTABLE = '{executable}'\n")

required_paths = []

if s.archive is not None:
archive_path = relpath(archive_unpack_dir(s.archive, cachedir), start=str(cachedir))
required_paths.append(str(archive_path))
for p in s.participations.root:
if p.archive is not None:
archive_path = relpath(archive_unpack_dir(p.archive, cachedir), start=str(cachedir))
required_paths.append(str(archive_path))
if required_paths:
f.write(f" REQUIRED_PATHS = {required_paths}\n")


def generate_tool_modules(s: defs.Submission, cachedir: Path) -> None:
generate_tool_module(s, cachedir, True)
generate_tool_module(s, cachedir, False)


def generate_xml(
timelimit_s: int, memlimit_M: int, cpuCores: int, cmdtasks: List[CmdTask], file: Path, tool_module_name: str
) -> None:
doc, tag, text = Doc().tagtext()

doc.asis('<?xml version="1.0"?>')
Expand All @@ -27,13 +114,18 @@ def generate_xml(timelimit_s: int, memlimit_M: int, cpuCores: int, cmdtasks: Lis
)
with tag(
"benchmark",
tool=f"smtcomp.tool",
tool=f"tools.{tool_module_name}",
timelimit=f"{timelimit_s}s",
hardlimit=f"{timelimit_s+30}s",
memlimit=f"{memlimit_M} MB",
cpuCores=f"{cpuCores}",
displayname="SC",
):
with tag("require", cpuModel="Intel Xeon E3-1230 v5 @ 3.40 GHz"):
text()

with tag("resultfiles"):
text("**/error.log")

for cmdtask in cmdtasks:
for includesfile in cmdtask.includesfiles:
with tag("rundefinition", name=f"{cmdtask.name},{includesfile}"):
Expand All @@ -42,67 +134,45 @@ def generate_xml(timelimit_s: int, memlimit_M: int, cpuCores: int, cmdtasks: Lis
text(option)
with tag("tasks", name="task"):
with tag("includesfile"):
text(includesfile)
text(f"benchmarks/{includesfile}")

with tag("propertyfile"):
text("benchmarks/properties/SMT.prp")

file.write_text(indent(doc.getvalue()))


def cmdtask_for_submission(s: defs.Submission, cachedir: Path) -> List[CmdTask]:
def cmdtask_for_submission(s: defs.Submission, cachedir: Path, target_track: defs.Track) -> List[CmdTask]:
res: List[CmdTask] = []
i = -1
for p in s.participations.root:
command = cast(defs.Command, p.command if p.command else s.command)
archive = cast(defs.Archive, p.archive if p.archive else s.archive)
for track, divisions in p.get().items():
if track != target_track:
continue

i = i + 1
match track:
case defs.Track.Incremental:
suffix = "_inc"
mode = "trace"
case defs.Track.ModelValidation:
suffix = "_model"
mode = "direct"
case defs.Track.UnsatCore:
suffix = ""
mode = "direct"
case defs.Track.ProofExhibition:
suffix = ""
mode = "direct"
case defs.Track.SingleQuery:
suffix = ""
mode = "direct"
case defs.Track.Cloud | defs.Track.Parallel:
continue
suffix = get_suffix(track)
tasks: list[str] = []
for _, logics in divisions.items():
tasks.extend([str(logic) + suffix for logic in logics])
if tasks:
executable_path = find_command(command, archive, cachedir)
executable = str(relpath(executable_path, start=str(cachedir)))
if command.compa_starexec:
assert command.arguments == []
executable_path = find_command(command, archive, cachedir)
executable = str(relpath(executable_path, start=str(cachedir)))
dirname = str(relpath(executable_path.parent, start=str(cachedir)))

if mode == "direct":
options = [
"bash",
"-c",
f'FILE=$(realpath $1); (cd {shlex.quote(dirname)}; exec ./{shlex.quote(executable_path.name)} "$FILE")',
"compa_starexec",
]
else:
assert mode == "trace"
options = [
"bash",
"-c",
f'ROOT=$(pwd); FILE=$(realpath $1); (cd {shlex.quote(dirname)}; exec $ROOT/smtlib2_trace_executor ./{shlex.quote(executable_path.name)} "$FILE")',
"compa_starexec",
]
options = [
"bash",
"-c",
f'FILE=$(realpath $1); (cd {shlex.quote(dirname)}; exec ./{shlex.quote(executable_path.name)} "$FILE")',
"compa_starexec",
]
else:
if mode == "direct":
options = [executable] + command.arguments
else:
options = ["./smtlib2_trace_executor", executable] + command.arguments
executable = str(command_path(command, archive, Path()))
options = [executable] + command.arguments
cmdtask = CmdTask(
name=f"{s.name},{i},{track}",
options=options,
Expand Down
Loading

0 comments on commit 7072e64

Please sign in to comment.