fault tests failing

[phanrahan]

test_simple_alu.py .......F                                              [100%]

=================================== FAILURES ===================================
_________________ test_simple_alu_assume_guarantee[cosa-None] __________________

target = 'cosa', strategy = None

    @pytest.mark.parametrize("target,strategy", [("verilator", "rejection"),
                                                 ("verilator", "smt"),
                                                 ("cosa", None)])
    def test_simple_alu_assume_guarantee(target, strategy):
        tester = fault.SymbolicTester(SimpleALU, SimpleALU.CLK, num_tests=100,
                                      random_strategy=strategy)
        tester.circuit.CLK = 0
        tester.circuit.config_en = 1
        tester.circuit.config_data = 0
        tester.step(2)
        tester.circuit.config_en = 0
        tester.step(2)
        if target == "verilator":
            # NOTE: Currently the cosa backend does not support the expect action
            tester.circuit.config_reg.Q.expect(0)
        tester.circuit.a.assume(lambda a: a < BitVector[16](32768))
        tester.circuit.b.assume(lambda b: b < BitVector[16](32768))
        # tester.circuit.b.assume(lambda b: b >= BitVector[16](32768))
    
        tester.circuit.c.guarantee(lambda a, b, c: (c >= a) and (c >= b))
        kwargs = {}
        if target == "verilator":
            kwargs["flags"] = ["-Wno-fatal"]
            kwargs["magma_opts"] = {"verilator_debug": True}
        elif target == "cosa":
            kwargs["magma_opts"] = {"passes": ["rungenerators", "flatten",
                                               "cullgraph"]}
        os.system("rm -r build/*")
>       tester.compile_and_run(target, directory="build", **kwargs)

test_simple_alu.py:93: 
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 
../fault/tester/staged_tester.py:279: in compile_and_run
    self._compile_and_run(target=target, **kwargs)
../fault/tester/staged_tester.py:264: in _compile_and_run
    self.run(target)
../fault/tester/symbolic_tester.py:103: in run
    self.targets[target].run(self.actions)
_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _ 

self = <fault.cosa_target.CoSATarget object at 0xb1ab0ee10>
actions = [Poke(SimpleALU.CLK, Bit(False)), Poke(SimpleALU.config_en, Bit(True)), Poke(SimpleALU.config_data, 0), Step(SimpleALU.CLK, steps=2), Poke(SimpleALU.config_en, Bit(False)), Step(SimpleALU.CLK, steps=2), ...]

    def run(self, actions):
        problem_file = self.directory / Path(f"{self.circuit_name}_problem.txt")
        ets_file = self.directory / Path(f"{self.circuit_name}.ets")
        src, ets = self.generate_code(actions)
        with open(problem_file, "w") as f:
            f.write(src)
        with open(ets_file, "w") as f:
            f.write(ets)
        assert not os.system(
>           f"CoSA --problem {problem_file} --solver-name {self.solver}")
E       AssertionError

../fault/cosa_target.py:205: AssertionError
----------------------------- Captured stdout call -----------------------------
Parsing file "build/SimpleALU.json"... DONE
Parsing file "build/SimpleALU.ets"... 
----------------------------- Captured stderr call -----------------------------
/Users/hanrahan/git/coreir/src/passes/transform/rungenerators.cpp:10 In Run Generators
/Users/hanrahan/git/coreir/src/passes/transform/rungenerators.cpp:26 Done running generators
/Users/hanrahan/git/coreir/src/binary/coreir.cpp:188 Running Runningvpasses
/Users/hanrahan/git/coreir/src/passes/transform/rungenerators.cpp:10 In Run Generators
/Users/hanrahan/git/coreir/src/passes/transform/rungenerators.cpp:26 Done running generators
/Users/hanrahan/git/coreir/src/binary/coreir.cpp:197 Running vpasses
/Users/hanrahan/git/coreir/src/binary/coreir.cpp:238 Modified?: No
/Users/hanrahan/git/coreir/src/passes/transform/rungenerators.cpp:10 In Run Generators
/Users/hanrahan/git/coreir/src/passes/transform/rungenerators.cpp:26 Done running generators
/Users/hanrahan/git/coreir/src/passes/transform/rungenerators.cpp:10 In Run Generators
/Users/hanrahan/git/coreir/src/passes/transform/rungenerators.cpp:26 Done running generators
/Users/hanrahan/miniconda3/lib/python3.7/site-packages/pysmt/walkers/generic.py:43: DeprecationWarning: Using or importing the ABCs from 'collections' instead of from 'collections.abc' is deprecated since Python 3.3,and in 3.9 it will stop working
  if len(nodetypes) == 1 and isinstance(nodetypes[0], collections.Iterable):
Traceback (most recent call last):
  File "/Users/hanrahan/miniconda3/bin/CoSA", line 11, in <module>
    load_entry_point('CoSA', 'console_scripts', 'CoSA')()
  File "/Users/hanrahan/git/CoSA/cosa/shell.py", line 210, in main
    sys.exit(run_problems(problems_config))
  File "/Users/hanrahan/git/CoSA/cosa/shell.py", line 166, in run_problems
    psol.solve_problems(problems_config)
  File "/Users/hanrahan/git/CoSA/cosa/analyzers/dispatcher.py", line 368, in solve_problems
    modifier)
  File "/Users/hanrahan/git/CoSA/cosa/analyzers/dispatcher.py", line 321, in parse_model
    (hts_a, inv_a, ltl_a) = parser.parse_file(filepath, general_config, flags)
  File "/Users/hanrahan/git/CoSA/cosa/encoders/explicit_transition_system.py", line 86, in parse_file
    return self.parse_string(f.read())
  File "/Users/hanrahan/git/CoSA/cosa/encoders/explicit_transition_system.py", line 97, in parse_string
    pline = self.parser.parseString(line, parseAll=True)
  File "/Users/hanrahan/miniconda3/lib/python3.7/site-packages/pyparsing.py", line 1947, in parseString
    raise exc
  File "/Users/hanrahan/miniconda3/lib/python3.7/site-packages/pyparsing.py", line 1941, in parseString
    se._parse(instring, loc)
  File "/Users/hanrahan/miniconda3/lib/python3.7/site-packages/pyparsing.py", line 1677, in _parseNoCache
    loc, tokens = self.parseImpl(instring, preloc, doActions)
  File "/Users/hanrahan/miniconda3/lib/python3.7/site-packages/pyparsing.py", line 4052, in parseImpl
    loc, exprtokens = e._parse(instring, loc, doActions)
  File "/Users/hanrahan/miniconda3/lib/python3.7/site-packages/pyparsing.py", line 1681, in _parseNoCache
    loc, tokens = self.parseImpl(instring, preloc, doActions)
  File "/Users/hanrahan/miniconda3/lib/python3.7/site-packages/pyparsing.py", line 3798, in parseImpl
    raise ParseException(instring, loc, self.errmsg, self)
pyparsing.ParseException: Expected end of text, found 'i'  (at char 15), (line:1, col:16)
========================= 1 failed, 7 passed in 10.19s =========================

[leonardt]

I suspect this may be an issue with an incompatible CoSA version, can you see what version you have installed?

❯ pip show cosa
Name: CoSA
Version: 0.4

[leonardt]

Bump, @phanrahan can you provide the CoSA version you're using? It looks like you have a local installation, so you can also provide the git commit hash