Merge branch 'atlas-labsparse'

HISTORY

@@ -1,3 +1,11 @@
+Version 4.0 - 2023-05
+
+C translation: general improvements
+LAbS: Added conditional processes (cond => P) (C encoding only)
+LAbS: Added multi-dimensional arrays (e.g., arr[x, y, z]) (C encoding only)
+SLiVER: Fixed ESBMC backend for SMT-based BMC
+SLiVER: Improved performance of CBMC simulation workflow
+
 Version 3.0 - 2022-07
 
 LAbS: Added blocks of actions "{a1; a2; ... ; an}"
@@ -9,7 +17,6 @@ LAbS: Added nondeterministic agent selection "pick"
 LAbS: Added ternary operator "if cond then expr1 else expr2"
 LAbS: Underscores ("_") can now be used within all names (but not at the beginning of a name)
 LAbS: Arithmetic expressions can now be used where a Boolean expression is expected ("expr" is desugared into "expr != 0")
-
 SLiVER: CBMC backend now supports simulation
 SLiVER: Added a compositional CADP backend "cadp-comp" (experimental)
 

Makefile

@@ -17,6 +17,7 @@ VERSION := $(strip $(shell grep version sliver/app/__about__.py | grep = | sed '
 RELEASENAME = sliver-v$(VERSION)_$(strip $(subst -,_, ${platform}))
 BUILD_DIR = build/$(platform)
 SLIVER_DIR = $(BUILD_DIR)/sliver
+BLACKLIST = $(shell git ls-files --others --exclude-standard)
 
 build/%/sliver/labs/LabsTranslate : $(labs_sources) $(labs_templates)
 	@echo Building LabsTranslate...
@@ -28,6 +29,8 @@ build/%/sliver.py :
 	@cp ./HISTORY $(@D) ;
 	@cp ./LICENSE $(@D) ;
 	@cp ./*.* $(@D) ;
+	@# Remove untracked files from release directory
+	@rm $(foreach f, $(BLACKLIST), $(@D)/$(f)) ;
 
 build/%/examples/README.md : $(labs_examples)
 	@echo Copying examples...

README.txt

@@ -1,6 +1,6 @@
 
-            SLiVER  4.0-230417
-              18 April 2023
+            SLiVER  4.0
+            10 May 2023
 
 The SLiVER LAbS VERification tool
 
@@ -27,13 +27,19 @@ sliver/           SLiVER code
 
 To install SLiVER, please follow the steps below:
 
-    1. install Python 3.10 or higher
+    1. install Python 3.10 or higher.
+       We recommend setting up a dedicated Python installation/environment
+       by using pyenv or similar tools.
 
     2. create a directory, suppose this is called /workspace
 
     3. extract the entire package contents in /workspace
 
-    4. set execution permissions (chmod +x) for sliver.py and cbmc-simulator
+    4. set execution permissions (chmod +x) for the following files:
+        - sliver.py
+        - sliver/cbmc/cbmc-simulator
+        - sliver/cbmc/cbmc-5-74
+        - sliver/minisat/minisat
 
     5. Install dependencies with (pip install -r requirements.txt)
 

sliver/analysis/value_analysis.py

@@ -7,8 +7,8 @@
 from itertools import product
 
 from ..app.cli import Args
-from ..labsparse.labs_ast import Expr, QueryResult
-from ..labsparse.labs_parser import Attr, NodeType, parse_to_dict
+from ..labsparse.labsparse.labs_ast import Expr, QueryResult
+from ..labsparse.labsparse.labs_parser import Attr, NodeType, parse_to_dict
 
 
 def merge(s0, s1, State):
@@ -47,7 +47,7 @@ def make_init(info, local_names, domain):
                 else:
                     s0[var.name] = abstract
 
-    s0["id"] = domain.abstract(*range(0, info.spawn.num_agents() - 1))
+    s0["id"] = domain.abstract_range(range(0, info.spawn.num_agents()))
     State = namedtuple("State", [*local_names, *s0.keys()])
     for x in local_names:
         s0[x] = domain.NO
@@ -273,7 +273,7 @@ def value_analysis(cli, info, domain):
             blocks.update(n for n in node.walk() if n(NodeType.BLOCK))
             guards.update(
                 (a, n) for n in node.walk()
-                if n(NodeType.GUARDED))
+                if n(NodeType.GUARDED) or n(NodeType.CONDITIONAL))
             calls = (
                 n[Attr.NAME] for n in node.walk()
                 if n(NodeType.CALL)

sliver/app/__about__.py

@@ -6,5 +6,5 @@
 __summary__ = "The SLiVER LAbS VERification tool"
 __uri__ = "https://github.com/labs-lang/sliver"
 
-__version__ = "4.0-230418"
-__date__ = "18 April 2023"
+__version__ = "4.0"
+__date__ = "10 May 2023"

sliver/app/cli.py

@@ -2,9 +2,12 @@
 
 import logging
 import sys
+import time
 from dataclasses import dataclass
 from enum import Enum
 
+import click
+
 from .__about__ import __date__, __summary__, __version__
 
 log = logging.getLogger('backend')
@@ -13,22 +16,23 @@
 class Args(Enum):
     BACKEND = "backend"
     BV = "bv"
+    CONCRETIZATION = "concretization"
     CORES = "cores"
+    CORES_FROM = "from"
+    CORES_TO = "to"
     DEBUG = "debug"
     FAIR = "fair"
-    CORES_FROM = "from"
-    KEEP_FILES = "keep_files"
     INCLUDE = "include"
-    PROPERTY = "property"
-    CONCRETIZATION = "concretization"
+    KEEP_FILES = "keep_files"
     NO_PROPERTIES = "no_properties"
+    PROPERTY = "property"
+    RND_SEED = "rnd_seed"
     SHOW = "show"
     SIMULATE = "simulate"
     STEPS = "steps"
     SYNC = "sync"
     TIMEOUT = "timeout"
     TRANSLATE_CEX = "translate_cex"
-    CORES_TO = "to"
     VALUES = "values"
     VERBOSE = "verbose"
 
@@ -43,53 +47,37 @@ class Args(Enum):
 
 HELPMSG = {
     Args.BACKEND: "Backend to use in verification mode.",
-
     Args.BV: "Enable bitvector optimization where supported.",
-
     Args.CONCRETIZATION: "Type of concretization (only for simulation).",
-
+    Args.CORES_FROM: "Parallel analysis: partition start.",
+    Args.CORES_TO: "Parallel analysis: partition end.",
     Args.CORES: "Number of CPU cores for parallel analysis.",
-
     Args.DEBUG: "Enable additional checks in the backend.",
-
     Args.FAIR: "Enforce fair interleaving of components.",
-
-    Args.CORES_FROM: "Parallel analysis: partition start.",
-
-    Args.KEEP_FILES: "Do not remove intermediate files.",
-
     Args.INCLUDE: (
         "Add custom code to generated program "
         "(may be specified multiple times)."),
-
-    Args.PROPERTY: "Property to consider, others will be ignored.",
-
+    Args.KEEP_FILES: "Do not remove intermediate files.",
     Args.NO_PROPERTIES: "Ignore all properties.",
-
+    Args.PROPERTY: "Property to consider, others will be ignored.",
+    Args.RND_SEED: (
+        "Seed for the random number generator."
+        "If none is given, the current time will be used."),
     Args.SHOW: "Print emulation program and exit.",
-
     Args.SIMULATE: (
         "Number of simulation traces to generate. "
         "If 0, run in verification mode."),
-
     Args.STEPS: (
         "Number of system evolutions. "
         "If 0, generate an unbounded system."),
-
     Args.SYNC: "Force synchronous stigmergy messages.",
-
     Args.TIMEOUT: (
         "Configure time limit (seconds). "
         "Set to 0 to disable timeout."),
-
     Args.TRANSLATE_CEX: (
         "Translate given counterexample to LAbS and exit."
     ),
-
-    Args.CORES_TO: "Parallel analysis: partition end.",
-
     Args.VALUES: "assign values for parameterised specification (key=value)",
-
     Args.VERBOSE: "Print additional messages from the backend."
 }
 
@@ -100,31 +88,51 @@ class Args(Enum):
     Args.CORES: 1,
     Args.DEBUG: False,
     Args.FAIR: False,
-    Args.CORES_FROM: None,
     Args.INCLUDE: tuple(),
     Args.KEEP_FILES: False,
-    Args.PROPERTY: None,
     Args.NO_PROPERTIES: False,
     Args.SHOW: False,
     Args.SIMULATE: 0,
     Args.STEPS: 0,
     Args.SYNC: False,
     Args.TIMEOUT: 0,
-    Args.TRANSLATE_CEX: None,
-    Args.CORES_TO: None,
     Args.VALUES: tuple(),
     Args.VERBOSE: False
 }
 
 
+__existing = click.Path(exists=True)
+__nonnegative = click.IntRange(min=0)
+
+TYPES = {
+    Args.CONCRETIZATION: click.Choice(("src", "sat", "none")),
+    Args.CORES_FROM: __nonnegative,
+    Args.CORES_TO: __nonnegative,
+    Args.CORES: __nonnegative,
+    Args.INCLUDE: __existing,
+    Args.RND_SEED: click.IntRange(min=1),
+    Args.SIMULATE: __nonnegative,
+    Args.STEPS: __nonnegative,
+    Args.TIMEOUT: __nonnegative,
+    Args.TRANSLATE_CEX: __existing
+}
+
+
 def CLICK(name, **kwargs):
-    return {
-        "help": HELPMSG[name],
+    result = {
         "show_default": name in DEFAULTS,
-        **({} if DEFAULTS[name] is None else {"default": DEFAULTS[name]}),
         **kwargs
     }
 
+    def maybe_add_from(some_dict, kwarg):
+        if name in some_dict:
+            result[kwarg] = some_dict[name]
+
+    maybe_add_from(HELPMSG, "help")
+    maybe_add_from(DEFAULTS, "default")
+    maybe_add_from(TYPES, "type")
+    return result
+
 
 class CliArgs(dict):
     def __init__(self, file, __dict) -> None:
@@ -136,14 +144,18 @@ def __init__(self, file, __dict) -> None:
             self.externs[k] = int(v)
 
     def __getitem__(self, key: Args):
-        return self.get(key.value, DEFAULTS[key])
+        return self.get(key.value, DEFAULTS.get(key))
 
     def __setitem__(self, key: Args, value):
         if isinstance(key, Args):
             self[key.value] = value
         else:
             super().__setitem__(key, value)
 
+    def get_seed(self) -> int:
+        seed = self[Args.RND_SEED]
+        return time.time_ns() % (1 << 32) if seed is None else seed
+
 
 class ExitStatus(Enum):
     SUCCESS = 0

sliver/app/main.py

@@ -14,40 +14,35 @@
     __file__ = inspect.getfile(inspect.currentframe())
 
 __DIR = Path(__file__).parent.resolve()
-__existing = click.Path(exists=True)
+backends_type = click.Choice(tuple(ALL_BACKENDS.keys()))
+
 log = logging.getLogger("sliver")
 
 
 @click.command(help=LONGDESCR)
 @click.version_option(__version__, prog_name=__title__.lower())
-@click.argument('file', required=True, type=__existing)
+@click.argument('file', required=True, type=click.Path(exists=True))
 @click.argument('values', nargs=-1)
-@click.option('--backend',
-              type=click.Choice(tuple(ALL_BACKENDS.keys())),
-              **CLICK(Args.BACKEND))
-@click.option('--concretization',
-              type=click.Choice(("src", "sat", "none")),
-              **CLICK(Args.CONCRETIZATION))
+@click.option('--backend', **CLICK(Args.BACKEND, type=backends_type))
+@click.option('--concretization', **CLICK(Args.CONCRETIZATION))
+@click.option('--bv/--no-bv', **CLICK(Args.BV))
+@click.option('--cores', **CLICK(Args.CORES))
 @click.option('--debug', **CLICK(Args.DEBUG, is_flag=True))
 @click.option('--fair/--no-fair', **CLICK(Args.FAIR))
-@click.option('--bv/--no-bv', **CLICK(Args.BV))
-@click.option('--simulate', **CLICK(Args.SIMULATE, type=int))
+@click.option('--from', **CLICK(Args.CORES_FROM))
+@click.option('--keep-files', **CLICK(Args.KEEP_FILES, is_flag=True))
+@click.option('--no-properties', **CLICK(Args.NO_PROPERTIES, is_flag=True))
+@click.option('--property', **CLICK(Args.PROPERTY))
+@click.option('--rnd-seed', **CLICK(Args.RND_SEED))
 @click.option('--show', **CLICK(Args.SHOW, is_flag=True))
-@click.option('--steps', **CLICK(Args.STEPS, type=int))
+@click.option('--simulate', **CLICK(Args.SIMULATE))
+@click.option('--steps', **CLICK(Args.STEPS))
 @click.option('--sync/--no-sync', **CLICK(Args.SYNC))
-@click.option('--timeout', **CLICK(Args.TIMEOUT, type=int))
-@click.option('--cores', **CLICK(Args.CORES, type=int))
-@click.option('--from', **CLICK(Args.CORES_FROM, type=int))
-@click.option('--to', **CLICK(Args.CORES_TO, type=int))
+@click.option('--timeout', **CLICK(Args.TIMEOUT))
+@click.option('--to', **CLICK(Args.CORES_TO))
 @click.option('--verbose', **CLICK(Args.VERBOSE, is_flag=True))
-@click.option('--no-properties', **CLICK(Args.NO_PROPERTIES, is_flag=True))
-@click.option('--property', **CLICK(Args.PROPERTY))
-@click.option('--keep-files', **CLICK(Args.KEEP_FILES, is_flag=True))
-@click.option('--translate-cex',
-              **CLICK(Args.TRANSLATE_CEX, type=__existing))
-@click.option('--include',
-              multiple=True, type=__existing,
-              **CLICK(Args.INCLUDE))
+@click.option('--translate-cex', **CLICK(Args.TRANSLATE_CEX))
+@click.option('--include', multiple=True, **CLICK(Args.INCLUDE))
 def main(file, **kwargs):
     cli = CliArgs(file, kwargs)
     backend_arg, simulate, show = (