basic assertions

grammar/FaultParser.g4

@@ -9,7 +9,7 @@ options {
 */
 
 sysSpec
-    : sysClause importDecl* globalDecl* componentDecl* startBlock* (assertion | assumption)? forStmt?
+    : sysClause importDecl* globalDecl* componentDecl+ (assertion | assumption)? startBlock forStmt?
     ;
 
 sysClause

smt/asserts.go

@@ -85,13 +85,18 @@ func (g *Generator) generateAsserts(exp ast.Expression, comp string, constr ast.
 func (g *Generator) parseInvariant(ex ast.Expression) rule {
 	switch e := ex.(type) {
 	case *ast.InvariantClause:
-		if e.Operator == "then" {
-			return g.parseStageInvar(e)
-		}
 
 		left := g.parseInvariant(e.Left)
 		right := g.parseInvariant(e.Right)
 
+		if e.Operator == "then" {
+			return &invariant{
+				left:     left,
+				operator: "then",
+				right:    right,
+			}
+		}
+
 		i := &invariant{
 			left:     left,
 			operator: smtlibOperators(e.Operator),
@@ -175,14 +180,35 @@ func (g *Generator) parseInvariant(ex ast.Expression) rule {
 	return nil
 }
 
-func (g *Generator) parseStageInvar(inv *ast.InvariantClause) rule {
-	left := g.parseInvariant(inv.Left)
-	right := g.parseInvariant(inv.Right)
+func (g *Generator) generateThenRules(inv *invariant) []string {
+	var rounds [][]int
+	var base string
+	switch when := inv.left.(type) {
+	case *wrap:
+		base = when.value
+		rounds = g.lookupVarRounds(when.value, when.state)
+	}
 
-	fmt.Println(left)
-	fmt.Println(right)
+	var rules []string
+	switch then := inv.right.(type) {
+	case *wrap:
+		for _, r := range rounds {
+			values := g.RoundVars[r[1]][r[2]:]
+			var or []string
+			for _, v := range values {
+				if v[0] == then.value {
+					vname := strings.Join(v, "_")
+					or = append(or, fmt.Sprintf("(= %s %s)", vname, "true"))
+				}
+			}
+			wclause := fmt.Sprintf("%s_%d", base, r[0])
+			tclause := fmt.Sprintf("(or %s)", strings.Join(or, " "))
+
+			rules = append(rules, fmt.Sprintf("(and %s %s)", wclause, tclause))
 
-	return &assrt{}
+		}
+	}
+	return rules
 }
 
 func (g *Generator) packageAssert(ident string, comp string, expr ast.Expression, stmt ast.Statement) *assrt {
@@ -261,6 +287,9 @@ func (g *Generator) generateAssertRules(ru rule, t string, tn int) []string {
 	case *assrt:
 		return g.generateAssertRules(r.assertion, t, tn)
 	case *invariant:
+		if r.operator == "then" {
+			return g.generateThenRules(r)
+		}
 		i = r
 	case *wrap:
 		return g.wrapPerm(r)

smt/forks_writer.go

@@ -267,6 +267,7 @@ func (g *Generator) capParallel() []rule {
 	var rules []rule
 	for k, v := range fork {
 		id := g.variables.advanceSSA(k)
+		g.addVarToRound(k, int(g.variables.ssa[k]))
 
 		var nums []int16
 		for _, c := range v {
@@ -333,6 +334,7 @@ func (g *Generator) capCond(b string, phis map[string]int16) ([]rule, map[string
 			id = g.variables.advanceSSA(k)
 			g.declareVar(id, g.variables.lookupType(k, nil))
 			_, i := g.variables.getVarBase(id)
+			g.addVarToRound(k, i)
 			phis[k] = int16(i)
 		} else {
 			id = fmt.Sprintf("%s_%d", k, phi)

smt/rules_types.go

@@ -266,6 +266,7 @@ func (g *Generator) constantRule(id string, c constant.Constant) string {
 	case *constant.Float:
 		ty := g.variables.lookupType(id, val)
 		id = g.variables.advanceSSA(id)
+		g.addVarToRound(id, int(g.variables.ssa[id]))
 		if g.isASolvable(id) {
 			g.declareVar(id, ty)
 		} else {
@@ -301,6 +302,7 @@ func (g *Generator) storeRule(inst *ir.InstStore) []rule {
 				g.variables.storeLastState(base, n+1)
 			}
 			id := g.variables.advanceSSA(base)
+			g.addVarToRound(base, int(n+1))
 			v := g.variables.formatValue(val)
 			if !g.variables.isBolean(v) && !g.variables.isNumeric(v) {
 				v = g.variables.formatIdent(v)
@@ -321,6 +323,7 @@ func (g *Generator) storeRule(inst *ir.InstStore) []rule {
 					g.variables.storeLastState(base, n+1)
 				}
 				id := g.variables.advanceSSA(base)
+				g.addVarToRound(base, int(n+1))
 				g.AddNewVarChange(base, id, prev)
 				wid := &wrap{value: id}
 				if g.variables.isBolean(r.y.String()) {
@@ -340,6 +343,7 @@ func (g *Generator) storeRule(inst *ir.InstStore) []rule {
 				}
 				ty := g.variables.lookupType(base, nil)
 				id := g.variables.advanceSSA(base)
+				g.addVarToRound(base, int(n+1))
 				g.AddNewVarChange(base, id, prev)
 				wid := &wrap{value: id}
 				rules = append(rules, &infix{x: wid, ty: ty, y: r})
@@ -356,6 +360,7 @@ func (g *Generator) storeRule(inst *ir.InstStore) []rule {
 		} else {
 			g.variables.storeLastState(base, n+1)
 		}
+		g.addVarToRound(base, int(n+1))
 		id := g.variables.advanceSSA(base)
 		g.AddNewVarChange(base, id, prev)
 		rules = append(rules, g.parseRule(id, inst.Src.Ident(), ty, ""))

smt/smt.go

@@ -4,6 +4,7 @@ import (
 	"bytes"
 	"fault/ast"
 	"fmt"
+	"strconv"
 	"strings"
 
 	"github.com/llir/llvm/asm"
@@ -21,7 +22,7 @@ type Generator struct {
 	functions  map[string]*ir.Func
 	rawAsserts []*ast.AssertionStatement
 	rawAssumes []*ast.AssumptionStatement
-	rawRules [][]rule
+	rawRules   [][]rule
 
 	// Generated SMT
 	inits     []string
@@ -40,10 +41,9 @@ type Generator struct {
 	parallelRunStart bool      //Flag, make sure all branches with parallel runs begin from the same point
 	returnVoid       *PhiState //Flag, escape parseFunc before moving to next block
 
-	currentRound int
-	Rounds  [][]string
-	RVarLookup map[string][]int 
-	Results map[string][]*VarChange
+	RoundVars  [][][]string
+	RVarLookup map[string][][]int
+	Results    map[string][]*VarChange
 }
 
 func NewGenerator() *Generator {
@@ -57,7 +57,7 @@ func NewGenerator() *Generator {
 		inPhiState:      NewPhiState(),
 		returnVoid:      NewPhiState(),
 		Results:         make(map[string][]*VarChange),
-		RVarLookup: make(map[string][]int), 
+		RVarLookup:      make(map[string][][]int),
 	}
 }
 
@@ -78,8 +78,38 @@ func (g *Generator) Run(llopt string) {
 }
 
 func (g *Generator) newRound() {
-	g.currentRound++
-	g.Rounds = append(g.Rounds, []string{})
+	g.RoundVars = append(g.RoundVars, [][]string{})
+}
+
+func (g *Generator) addVarToRound(base string, num int) {
+	idx := len(g.RoundVars) - 1
+	if idx == -1 {
+		idx = 0
+		g.RoundVars = [][][]string{{{base, fmt.Sprint(num)}}}
+	} else {
+		g.RoundVars[idx] = append(g.RoundVars[idx], []string{base, fmt.Sprint(num)})
+	}
+
+	idx2 := len(g.RoundVars[idx]) - 1
+	g.RVarLookup[base] = append(g.RVarLookup[base], []int{num, idx, idx2})
+}
+
+func (g *Generator) lookupVarRounds(base string, num string) [][]int {
+	if num == "" {
+		return g.RVarLookup[base]
+	}
+
+	state, err := strconv.Atoi(num)
+	if err != nil {
+		panic(err)
+	}
+
+	for _, b := range g.RVarLookup[base] {
+		if b[0] == state {
+			return [][]int{b}
+		}
+	}
+	panic(fmt.Errorf("state %s of variable %s is missing", num, base))
 }
 
 func (g *Generator) GetForks() []Fork {

smt/smt_parse.go

@@ -441,6 +441,7 @@ func (g *Generator) parseBuiltIn(call *ir.InstCall, complex bool) []rule {
 	} else {
 		g.variables.storeLastState(base, n+1)
 	}
+	g.addVarToRound(base, int(n+1))
 	newState = g.variables.advanceSSA(base)
 	g.AddNewVarChange(base, newState, prev)
 
@@ -462,6 +463,7 @@ func (g *Generator) parseBuiltIn(call *ir.InstCall, complex bool) []rule {
 		g.variables.storeLastState(base2, n2+1)
 	}
 
+	g.addVarToRound(base2, int(n2+1))
 	currentState := g.variables.advanceSSA(base2)
 	g.AddNewVarChange(base2, currentState, prev2)
 	if complex {

smt/temporal_logic_test.go

@@ -271,46 +271,46 @@ func TestTemporal2(t *testing.T) {
 	}
 }
 
-// func TestTemporalSys(t *testing.T) {
-
-// 	test := `system test1;
-// 		component a = states{
-// 			foo: func{
-// 				advance(b.bar);
-// 			},
-// 			zoo: func{
-// 				advance(this.foo);
-// 			},
-// 		};
-
-// 		component b = states{
-// 			buzz: func{
-// 				advance(a.foo);
-// 			},
-// 			bar: func{
-// 				stay();
-// 			},
-// 		};
-
-// 		assert when a.zoo then !b.bar;
-
-// 		start {
-// 			b: buzz,
-// 			a: zoo,
-// 		};
-// 	`
-// 	expecting := `
-// 	`
-
-// 	smt, err := prepTestSys("", test, false)
-
-// 	if err != nil {
-// 		t.Fatalf("compilation failed on valid spec. got=%s", err)
-// 	}
-
-// 	err = compareResults("TemporalSys", smt, string(expecting))
-
-// 	if err != nil {
-// 		t.Fatalf(err.Error())
-// 	}
-// }
+func TestTemporalSys(t *testing.T) {
+
+	test := `system test1;
+		component a = states{
+			foo: func{
+				advance(b.bar);
+			},
+			zoo: func{
+				advance(this.foo);
+			},
+		};
+
+		component b = states{
+			buzz: func{
+				advance(a.foo);
+			},
+			bar: func{
+				stay();
+			},
+		};
+
+		assert when a.zoo then !b.bar;
+
+		start{
+			b: buzz,
+			a: zoo,
+		};
+		`
+	expecting := `
+	`
+
+	smt, err := prepTestSys("", test, false)
+
+	if err != nil {
+		t.Fatalf("compilation failed on valid spec. got=%s", err)
+	}
+
+	err = compareResults("TemporalSys", smt, string(expecting))
+
+	if err != nil {
+		t.Fatalf(err.Error())
+	}
+}

smt/variables_writer.go

@@ -334,6 +334,7 @@ func (g *Generator) fetchIdent(id string, r rule) rule {
 			} else {
 				g.variables.storeLastState(id, n+1)
 			}
+			g.addVarToRound(id, int(n+1))
 			id = g.variables.advanceSSA(v.Ident())
 			wid := &wrap{value: id}
 			return wid