fixing some small bugs including returns on after blocks

listener/listener.go

@@ -29,8 +29,9 @@ type FaultListener struct {
 	Unknowns   []string
 }
 
-func NewListener(testing bool, skipRun bool) *FaultListener {
+func NewListener(path string, testing bool, skipRun bool) *FaultListener {
 	return &FaultListener{
+		Path:       path,
 		testing:    testing,
 		skipRun:    skipRun,
 		Uncertains: make(map[string][]float64),

listener/listener_test.go

@@ -1635,32 +1635,34 @@ func TestSysStart(t *testing.T) {
 }
 
 func prepTest(test string, flags map[string]bool) (*FaultListener, *ast.Spec) {
+	path := ""
 	is := antlr.NewInputStream(test)
 	lexer := parser.NewFaultLexer(is)
 	stream := antlr.NewCommonTokenStream(lexer, antlr.TokenDefaultChannel)
 
 	p := parser.NewFaultParser(stream)
 	var listener *FaultListener
 	if flags != nil && flags["skipRun"] {
-		listener = NewListener(true, true)
+		listener = NewListener(path, true, true)
 	} else {
-		listener = NewListener(true, false)
+		listener = NewListener(path, true, false)
 	}
 	antlr.ParseTreeWalkerDefault.Walk(listener, p.Spec())
 	return listener, listener.AST
 }
 
 func prepSysTest(test string, flags map[string]bool) (*FaultListener, *ast.Spec) {
+	path := ""
 	is := antlr.NewInputStream(test)
 	lexer := parser.NewFaultLexer(is)
 	stream := antlr.NewCommonTokenStream(lexer, antlr.TokenDefaultChannel)
 
 	p := parser.NewFaultParser(stream)
 	var listener *FaultListener
 	if flags != nil && flags["skipRun"] {
-		listener = NewListener(true, true)
+		listener = NewListener(path, true, true)
 	} else {
-		listener = NewListener(true, false)
+		listener = NewListener(path, true, false)
 	}
 	antlr.ParseTreeWalkerDefault.Walk(listener, p.SysSpec())
 	return listener, listener.AST

llvm/compiler.go

@@ -809,6 +809,8 @@ func (c *Compiler) compileIf(n *ast.IfExpression) {
 	// set after block to jump to the after block
 	if len(c.contextCondAfter) > 0 {
 		afterBlock.NewBr(c.contextCondAfter[len(c.contextCondAfter)-1])
+	} else {
+		afterBlock.NewRet(nil)
 	}
 }
 

llvm/llvm_test.go

@@ -788,12 +788,13 @@ func stripAndEscape(str string) string {
 }
 
 func prepTest(test string) (string, error) {
+	path := ""
 	is := antlr.NewInputStream(test)
 	lexer := parser.NewFaultLexer(is)
 	stream := antlr.NewCommonTokenStream(lexer, antlr.TokenDefaultChannel)
 
 	p := parser.NewFaultParser(stream)
-	l := listener.NewListener(true, false)
+	l := listener.NewListener(path, true, false)
 	antlr.ParseTreeWalkerDefault.Walk(l, p.Spec())
 	ty := &types.Checker{}
 	err := ty.Check(l.AST)
@@ -811,12 +812,13 @@ func prepTest(test string) (string, error) {
 }
 
 func prepTestSys(test string) (string, error) {
+	path := ""
 	is := antlr.NewInputStream(test)
 	lexer := parser.NewFaultLexer(is)
 	stream := antlr.NewCommonTokenStream(lexer, antlr.TokenDefaultChannel)
 
 	p := parser.NewFaultParser(stream)
-	l := listener.NewListener(true, false)
+	l := listener.NewListener(path, true, false)
 	antlr.ParseTreeWalkerDefault.Walk(l, p.SysSpec())
 	ty := &types.Checker{}
 	err := ty.Check(l.AST)

llvm/lr_asserts_test.go

@@ -151,12 +151,13 @@ func compareAsserts(t *testing.T, e ast.Expression, i int) {
 // END AWFUL TEST, NOTHING TO SEE HERE... MOVE ALONG ;)
 
 func prepAssertTest(test string) (*Compiler, error) {
+	path := ""
 	is := antlr.NewInputStream(test)
 	lexer := parser.NewFaultLexer(is)
 	stream := antlr.NewCommonTokenStream(lexer, antlr.TokenDefaultChannel)
 
 	p := parser.NewFaultParser(stream)
-	l := listener.NewListener(true, false)
+	l := listener.NewListener(path, true, false)
 	antlr.ParseTreeWalkerDefault.Walk(l, p.Spec())
 	ty := &types.Checker{}
 	err := ty.Check(l.AST)

main.go

@@ -36,8 +36,7 @@ func parse(data string, path string, file string, filetype string) (*listener.Fa
 	p.AddErrorListener(&listener.FaultErrorListener{Filename: file})
 
 	// Finally parse the expression
-	lstnr := listener.NewListener(false, false)
-	lstnr.Path = path
+	lstnr := listener.NewListener(path, false, false)
 	switch filetype {
 	case "fspec":
 		antlr.ParseTreeWalkerDefault.Walk(lstnr, p.Spec())

smt/asserts_test.go

@@ -40,7 +40,7 @@ func TestSimpleAssert(t *testing.T) {
 	(assert (or (<= test1_t_foo_value_0 0) (<= test1_t_foo_value_1 0)(<= test1_t_foo_value_2 0)(<= test1_t_foo_value_3 0)(<= test1_t_foo_value_4 0)(<= test1_t_foo_value_5 0)))
 `
 
-	smt, err := prepTest(test)
+	smt, err := prepTest("", test)
 
 	if err != nil {
 		t.Fatalf("compilation failed on valid spec. got=%s", err)
@@ -99,7 +99,7 @@ func TestCompoundAssert(t *testing.T) {
 	(> test1_t_foo_value_4 10)
 	(> test1_t_foo_value_5 10)))`
 
-	smt, err := prepTest(test)
+	smt, err := prepTest("", test)
 
 	if err != nil {
 		t.Fatalf("compilation failed on valid spec. got=%s", err)
@@ -152,7 +152,7 @@ func TestAssertInfix(t *testing.T) {
 	(<= test1_t_foo_value_4 0)
 	(<= test1_t_foo_value_5 0)))`
 
-	smt, err := prepTest(test)
+	smt, err := prepTest("", test)
 
 	if err != nil {
 		t.Fatalf("compilation failed on valid spec. got=%s", err)
@@ -209,7 +209,7 @@ func TestMultiVar(t *testing.T) {
 	(<= test1_t_foo_value_5 test1_t_fuzz_0)))
 	`
 
-	smt, err := prepTest(test)
+	smt, err := prepTest("", test)
 
 	if err != nil {
 		t.Fatalf("compilation failed on valid spec. got=%s", err)
@@ -258,7 +258,7 @@ func TestSimpleAssume(t *testing.T) {
 	(assert (and (> test1_t_foo_value_0 0) (> test1_t_foo_value_1 0)(> test1_t_foo_value_2 0)(> test1_t_foo_value_3 0)(> test1_t_foo_value_4 0)(> test1_t_foo_value_5 0)))
 `
 
-	smt, err := prepTest(test)
+	smt, err := prepTest("", test)
 
 	if err != nil {
 		t.Fatalf("compilation failed on valid spec. got=%s", err)
@@ -307,7 +307,7 @@ func TestSpecificStateAssume(t *testing.T) {
 	(assert (> test1_t_foo_value_1 0))
 `
 
-	smt, err := prepTest(test)
+	smt, err := prepTest("", test)
 
 	if err != nil {
 		t.Fatalf("compilation failed on valid spec. got=%s", err)

smt/smt_integration_test.go

@@ -5,8 +5,11 @@ import (
 	"fault/llvm"
 	"fault/parser"
 	"fault/types"
+	"fault/util"
 	"fmt"
 	"os"
+	gopath "path"
+	"strconv"
 	"strings"
 	"testing"
 	"unicode"
@@ -19,13 +22,13 @@ func TestTestData(t *testing.T) {
 		"testdata/simple.fspec",
 		"testdata/bathtub2.fspec",
 		"testdata/booleans.fspec",
-		//"testdata/unknowns.fspec",
+		"testdata/unknowns.fspec",
 	}
 	smt2s := []string{"testdata/bathtub.smt2",
 		"testdata/simple.smt2",
 		"testdata/bathtub2.smt2",
 		"testdata/booleans.smt2",
-		//"testdata/unknowns.smt2",
+		"testdata/unknowns.smt2",
 	}
 	for i, s := range specs {
 		data, err := os.ReadFile(s)
@@ -36,7 +39,7 @@ func TestTestData(t *testing.T) {
 		if err != nil {
 			panic(fmt.Sprintf("compiled spec %s is not valid", smt2s[i]))
 		}
-		smt, err := prepTest(string(data))
+		smt, err := prepTest(s, string(data))
 
 		if err != nil {
 			t.Fatalf("compilation failed on valid spec %s. got=%s", s, err)
@@ -50,6 +53,38 @@ func TestTestData(t *testing.T) {
 	}
 }
 
+func TestSys(t *testing.T) {
+	specs := [][]string{
+		/*{"testdata/statechart.fsystem", "1"},*/
+	}
+	smt2s := []string{
+		/*"testdata/statechart.smt2",*/
+	}
+	for i, s := range specs {
+		data, err := os.ReadFile(s[0])
+		if err != nil {
+			panic(fmt.Sprintf("spec %s is not valid", s[0]))
+		}
+		imports, _ := strconv.ParseBool(s[1])
+
+		expecting, err := os.ReadFile(smt2s[i])
+		if err != nil {
+			panic(fmt.Sprintf("compiled spec %s is not valid", smt2s[i]))
+		}
+		smt, err := prepTestSys(s[0], string(data), imports)
+
+		if err != nil {
+			t.Fatalf("compilation failed on valid spec %s. got=%s", s[0], err)
+		}
+
+		err = compareResults(s[0], smt, string(expecting))
+
+		if err != nil {
+			t.Fatalf(err.Error())
+		}
+	}
+}
+
 func TestIndividual(t *testing.T) {
 
 	data, err := os.ReadFile("testdata/unknowns.fspec")
@@ -60,7 +95,7 @@ func TestIndividual(t *testing.T) {
 	if err != nil {
 		panic(fmt.Sprintf("compiled spec %s is not valid", "testdata/unknowns.smt2"))
 	}
-	smt, err := prepTest(string(data))
+	smt, err := prepTest("testdata/unknowns.fspec", string(data))
 
 	if err != nil {
 		t.Fatalf("compilation failed on valid spec testdata/unknowns.fspec. got=%s", err)
@@ -83,7 +118,7 @@ func TestMultiCond(t *testing.T) {
 	if err != nil {
 		panic(fmt.Sprintf("compiled spec %s is not valid", "testdata/multicond.smt2"))
 	}
-	smt, err := prepTest(string(data))
+	smt, err := prepTest("testdata/multicond.fspec", string(data))
 
 	if err != nil {
 		t.Fatalf("compilation failed on valid spec testdata/multicond.fspec. got=%s", err)
@@ -136,13 +171,13 @@ func stripAndEscape(str string) string {
 	return output.String()
 }
 
-func prepTest(test string) (string, error) {
+func prepTest(path string, test string) (string, error) {
 	is := antlr.NewInputStream(test)
 	lexer := parser.NewFaultLexer(is)
 	stream := antlr.NewCommonTokenStream(lexer, antlr.TokenDefaultChannel)
 
 	p := parser.NewFaultParser(stream)
-	l := listener.NewListener(true, false)
+	l := listener.NewListener(path, true, false)
 	antlr.ParseTreeWalkerDefault.Walk(l, p.Spec())
 	ty := &types.Checker{}
 	err := ty.Check(l.AST)
@@ -162,6 +197,35 @@ func prepTest(test string) (string, error) {
 	return generator.SMT(), nil
 }
 
+func prepTestSys(filepath string, test string, imports bool) (string, error) {
+	filepath = util.Filepath(filepath)
+	path := gopath.Dir(filepath)
+
+	is := antlr.NewInputStream(test)
+	lexer := parser.NewFaultLexer(is)
+	stream := antlr.NewCommonTokenStream(lexer, antlr.TokenDefaultChannel)
+
+	p := parser.NewFaultParser(stream)
+	l := listener.NewListener(path, !imports, false) //imports being true means testing is false :)
+	antlr.ParseTreeWalkerDefault.Walk(l, p.SysSpec())
+	ty := &types.Checker{}
+	err := ty.Check(l.AST)
+	if err != nil {
+		return "", err
+	}
+	compiler := llvm.NewCompiler()
+	compiler.LoadMeta(ty.SpecStructs, l.Uncertains, l.Unknowns)
+	err = compiler.Compile(l.AST)
+	if err != nil {
+		return "", err
+	}
+	generator := NewGenerator()
+	generator.LoadMeta(compiler.Uncertains, compiler.Unknowns, compiler.Asserts, compiler.Assumes)
+	generator.Run(compiler.GetIR())
+	//fmt.Println(generator.SMT())
+	return generator.SMT(), nil
+}
+
 func notStrictlyOrdered(want string, got string) bool {
 	// Fixing cases where lines of SMT end up in slightly
 	// different orders. Only runs when shallow string

smt/temporal_logic_test.go

@@ -40,7 +40,7 @@ func TestEventually(t *testing.T) {
 	(assert (or (> test1_t_foo_value_0 0) (> test1_t_foo_value_1 0)(> test1_t_foo_value_2 0)(> test1_t_foo_value_3 0)(> test1_t_foo_value_4 0)(> test1_t_foo_value_5 0)))
 `
 
-	smt, err := prepTest(test)
+	smt, err := prepTest("", test)
 
 	if err != nil {
 		t.Fatalf("compilation failed on valid spec. got=%s", err)
@@ -96,7 +96,7 @@ func TestEventuallyAlways(t *testing.T) {
 		))
 `
 
-	smt, err := prepTest(test)
+	smt, err := prepTest("", test)
 
 	if err != nil {
 		t.Fatalf("compilation failed on valid spec. got=%s", err)
@@ -152,7 +152,7 @@ func TestEventuallyAlways2(t *testing.T) {
 		))
 `
 
-	smt, err := prepTest(test)
+	smt, err := prepTest("", test)
 
 	if err != nil {
 		t.Fatalf("compilation failed on valid spec. got=%s", err)
@@ -200,7 +200,7 @@ func TestTemporal(t *testing.T) {
 	(assert (or (and (<= test1_t_foo_value_0 0) (<= test1_t_foo_value_1 0)) (and (<= test1_t_foo_value_0 0) (<= test1_t_foo_value_2 0)) (and (<= test1_t_foo_value_0 0) (<= test1_t_foo_value_3 0)) (and (<= test1_t_foo_value_0 0) (<= test1_t_foo_value_4 0)) (and (<= test1_t_foo_value_0 0) (<= test1_t_foo_value_5 0)) (and (<= test1_t_foo_value_1 0) (<= test1_t_foo_value_2 0)) (and (<= test1_t_foo_value_1 0) (<= test1_t_foo_value_3 0)) (and (<= test1_t_foo_value_1 0) (<= test1_t_foo_value_4 0)) (and (<= test1_t_foo_value_1 0) (<= test1_t_foo_value_5 0)) (and (<= test1_t_foo_value_2 0) (<= test1_t_foo_value_3 0)) (and (<= test1_t_foo_value_2 0) (<= test1_t_foo_value_4 0)) (and (<= test1_t_foo_value_2 0) (<= test1_t_foo_value_5 0)) (and (<= test1_t_foo_value_3 0) (<= test1_t_foo_value_4 0)) (and (<= test1_t_foo_value_3 0) (<= test1_t_foo_value_5 0)) (and (<= test1_t_foo_value_4 0) (<= test1_t_foo_value_5 0))))
 	`
 
-	smt, err := prepTest(test)
+	smt, err := prepTest("", test)
 
 	if err != nil {
 		t.Fatalf("compilation failed on valid spec. got=%s", err)
@@ -267,7 +267,7 @@ func TestTemporal2(t *testing.T) {
 	//	panic(fmt.Sprintf("compiled spec %s is not valid", "testdata/temporal2.smt2"))
 	//}
 
-	smt, err := prepTest(test)
+	smt, err := prepTest("", test)
 
 	if err != nil {
 		t.Fatalf("compilation failed on valid spec. got=%s", err)

smt/testdata/statechart.fsystem

@@ -2,22 +2,22 @@ system statechart;
 
 import "simple.fspec";
 
-global flow = new simple.fl;
+global fl = new simple.fl;
 
 component drain = states{
     initial: func{
-        if !flow.active {
-            flow.active = true;
+        if !fl.active {
+            fl.active = true;
             advance(this.open);
         }
     },
     open: func{
-        if flow.vault.value < 0 {
+        if fl.vault.value < 0 {
             advance(this.close);
         }
     },
     close: func{
-        flow.active = false;
+        fl.active = false;
     },
 };
 
@@ -27,6 +27,6 @@ start {
 
 for 5 run {
     if !drain.close{
-        flow.fn;
+        fl.fn;
     }
 }