Skip to content

Commit 3300905

Browse files
committed
Fix direction of rmem parse sigils
* means ok, : means not. Also made the tests a bit more DRY.
1 parent f445ff2 commit 3300905

File tree

6 files changed

+57
-12
lines changed

6 files changed

+57
-12
lines changed

internal/serviceimpl/backend/herdstyle/parser/parser_test.go

Lines changed: 26 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -11,8 +11,10 @@ import (
1111
"io/ioutil"
1212
"os"
1313
"path/filepath"
14+
"strings"
1415
"testing"
1516

17+
"github.com/1set/gut/yos"
1618
"github.com/MattWindsor91/c4t/internal/serviceimpl/backend/herdstyle/rmem"
1719

1820
"github.com/stretchr/testify/require"
@@ -63,21 +65,37 @@ func TestParse_error(t *testing.T) {
6365
func TestParse_valid(t *testing.T) {
6466
t.Parallel()
6567

66-
cases := map[string]parser.Impl{
67-
"herd-ok-small": herd.Herd{},
68-
"rmem-ok-unsat-partial": rmem.Rmem{},
69-
}
68+
fs, err := yos.ListMatch(filepath.Join("testdata", "valid"), yos.ListIncludeFile, "*.json")
69+
require.NoError(t, err, "testdata listing shouldn't fail")
70+
71+
for _, f := range fs {
72+
path := f.Path
73+
pprefix := strings.TrimSuffix(path, ".json")
74+
name := filepath.Base(pprefix)
7075

71-
for name, c := range cases {
72-
name, c := name, c
7376
t.Run(name, func(t *testing.T) {
7477
t.Parallel()
7578

76-
f, err := os.Open(filepath.Join("testdata", "valid", name+".txt"))
79+
pfields := strings.SplitN(name, "-", 2)
80+
require.NotEmpty(t, pfields, "malformed test name, should be 'type-*.json'")
81+
82+
var c parser.Impl
83+
switch pfields[0] {
84+
case "herd":
85+
c = herd.Herd{}
86+
case "litmus":
87+
c = litmus.Litmus{}
88+
case "rmem":
89+
c = rmem.Rmem{}
90+
default:
91+
require.Failf(t, "unsupported parser subtype", "got %q", pfields[0])
92+
}
93+
94+
f, err := os.Open(pprefix + ".txt")
7795
require.NoError(t, err, "missing input file")
7896
defer func() { _ = f.Close() }()
7997

80-
out, err := ioutil.ReadFile(filepath.Join("testdata", "valid", name+".json"))
98+
out, err := ioutil.ReadFile(path)
8199
require.NoError(t, err, "missing output file")
82100

83101
o := new(obs.Obs)

internal/serviceimpl/backend/herdstyle/parser/testdata/valid/rmem-ok-unsat-partial.json renamed to internal/serviceimpl/backend/herdstyle/parser/testdata/valid/rmem-no-partial.json

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,7 @@
2929
"t0r0": "0"
3030
}
3131
],
32-
"witnesses": [
32+
"counter_examples": [
3333
{
3434
"y": "0",
3535
"x": "1",
@@ -43,7 +43,7 @@
4343
"t0r0": "0"
4444
}
4545
],
46-
"counter_examples": [
46+
"witnesses": [
4747
{
4848
"y": "1",
4949
"x": "1",
Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
{
2+
"flags": [
3+
"sat"
4+
],
5+
"witnesses": [
6+
{
7+
"t0r0": "1",
8+
"x": "1"
9+
}
10+
],
11+
"states": [
12+
{
13+
"t0r0": "1",
14+
"x": "1"
15+
}
16+
]
17+
}
Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
Test test_0 Required
2+
Memory-writes=
3+
States 1
4+
2 *>x=1; t0r0=1; via "0;0;0;0"
5+
Unhandled exceptions 0
6+
Ok
7+
Condition forall (x=1 /\ t0r0=1)
8+
Hash=f4ff57c0c324471586adc4e4cab40264
9+
Observation test_0 Always 1 0
10+
Runtime: 0.179883 sec

internal/serviceimpl/backend/herdstyle/rmem/parser.go

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -22,9 +22,9 @@ func (Rmem) ParseStateLine(_ parser.TestType, fields []string) (*parser.StateLin
2222
// Rmem's state line syntax is similar to that of Litmus's, but with a few gotchas:
2323
//
2424
// - Asterisks always represent witnesses, not 'interesting' cases; this means we always parse as if the test type
25-
// is 'required';
25+
// is 'allowed';
2626
// - State lines contain a 'via "XYZ"' line, which we need to scrub.
27-
return litmus.Litmus{}.ParseStateLine(parser.Required, stripVia(fields))
27+
return litmus.Litmus{}.ParseStateLine(parser.Allowed, stripVia(fields))
2828
}
2929

3030
// ParsePreTestLine checks the pre-Test line in fields to check whether it states this is a partial observation.

0 commit comments

Comments
 (0)