working through some bugs with compound strings and found a bug in sm…

…t generation of prefixes

grammar/FaultParser.g4

@@ -93,6 +93,7 @@ stringDecl
 compoundString
     : operandName
     | '!' operandName
+    | '(' compoundString ')'
     | compoundString '&&' compoundString
     | compoundString '||' compoundString
     ;

listener/listener.go

@@ -1235,18 +1235,20 @@ func (l *FaultListener) ExitCompoundString(c *parser.CompoundStringContext) {
 		return
 	}
 
-	operator := c.GetChild(1).(antlr.TerminalNode).GetText()
-	token := util.GenerateToken(string(ast.OPS[operator]), operator, c.GetStart(), c.GetStop())
+	if op, ok := c.GetChild(1).(antlr.TerminalNode); ok {
+		operator := op.GetText()
+		token := util.GenerateToken(string(ast.OPS[operator]), operator, c.GetStart(), c.GetStop())
 
-	rght := l.pop()
-	lft := l.pop()
-	e := &ast.InfixExpression{
-		Token:    token,
-		Left:     lft.(ast.Expression),
-		Operator: operator,
-		Right:    rght.(ast.Expression),
+		rght := l.pop()
+		lft := l.pop()
+		e := &ast.InfixExpression{
+			Token:    token,
+			Left:     lft.(ast.Expression),
+			Operator: operator,
+			Right:    rght.(ast.Expression),
+		}
+		l.push(e)
 	}
-	l.push(e)
 }
 
 func (l *FaultListener) ExitStringDecl(c *parser.StringDeclContext) {

llvm/compiler.go

@@ -7,6 +7,7 @@ import (
 	"fault/preprocess"
 	"fault/util"
 	"fmt"
+	"math/rand"
 	"runtime/debug"
 	"strings"
 
@@ -162,6 +163,14 @@ func (c *Compiler) validate(specfile *ast.Spec) {
 			c.IsValid = true
 			return
 		}
+
+		if d, ok := n.(*ast.DefStatement); ok {
+			if _, str := d.Value.(*ast.StringLiteral); str {
+				c.IsValid = true
+				return
+			}
+		}
+
 	}
 }
 
@@ -1064,6 +1073,23 @@ func (c *Compiler) compileCompoundNode(n ast.Node) *ir.Global {
 		name := r.Ident()
 		name = fmt.Sprintf("%s_neg", util.FormatIdent(name))
 		return c.module.NewGlobalDef(name, constant.NewFNeg(r))
+	case *ast.InfixExpression:
+		r := c.compileCompoundNode(v.Right)
+		l := c.compileCompoundNode(v.Left)
+		rname := r.Ident()
+		lname := l.Ident()
+		name := fmt.Sprintf("%s_%s", util.FormatIdent(lname), util.FormatIdent(rname))
+		if _, ok := c.GetGlobal(name); ok { //avoiding conflicts when compound rules overlap
+			name = fmt.Sprintf("%s_%d", name, rand.Int())
+		}
+		var infix constant.Constant
+		switch v.Operator {
+		case "&&":
+			infix = constant.NewAnd(l, r)
+		case "||":
+			infix = constant.NewOr(l, r)
+		}
+		return c.module.NewGlobalDef(name, infix)
 	default:
 		r := c.compileValue(v)
 		name := r.Ident()
@@ -1564,6 +1590,15 @@ func (c *Compiler) validOperator(node *ast.InfixExpression, boolsAllowed bool) b
 	return true
 }
 
+func (c *Compiler) GetGlobal(name string) (*ir.Global, bool) {
+	for _, gl := range c.module.Globals {
+		if util.FormatIdent(gl.Ident()) == name {
+			return gl, true
+		}
+	}
+	return nil, false
+}
+
 func negate(e ast.Expression) ast.Expression {
 	//Negate the expression so that the solver attempts to disprove it
 	switch n := e.(type) {

smt/asserts.go

@@ -141,9 +141,24 @@ func (g *Generator) parseInvariantNode(exp ast.Expression, stateRange bool) *rul
 			operator = smtlibOperators(e.Operator)
 		}
 
-		if r, ok := right.(*rules.States); ok {
+		switch r := right.(type) {
+		case *rules.Wrap:
+			var numstr = r.State
+			if r.Constant {
+				numstr = "0"
+			}
+			if r.All {
+				numstr = ""
+			}
+			vr := g.varRounds(r.Value, numstr)
+			s := &rules.States{Base: r.Value,
+				States:   vr,
+				Constant: true,
+			}
+			return g.mergeInvariantPrefix([]*rules.States{s}, operator)
+		case *rules.States:
 			return g.mergeInvariantPrefix([]*rules.States{r}, operator)
-		} else {
+		default:
 			return g.mergeInvariantPrefix(right.(*rules.StateGroup).Wraps, operator)
 		}
 
@@ -171,8 +186,10 @@ func (g *Generator) mergeInvariantPrefix(right []*rules.States, operator string)
 	for _, r := range right {
 		states := make(map[int][]string)
 		for i := 0; i <= g.Rounds; i++ {
-			if s, ok := r.States[i]; ok {
-				states[i] = append(states[i], fmt.Sprintf("(%s %s)", operator, s))
+			if st, ok := r.States[i]; ok {
+				for _, s := range st {
+					states[i] = append(states[i], fmt.Sprintf("(%s %s)", operator, s))
+				}
 			}
 		}
 		r.States = states

smt/generator.go

@@ -1313,7 +1313,7 @@ func (g *Generator) constantRule(id string, c constant.Constant) string {
 		g.addVarToRound(id, 0)
 		id = g.variables.AdvanceSSA(id)
 		rule := g.parseConstExpr(val)
-		v := g.writeRule(rule)
+		v := rule.Assertless()
 		return g.writeInitRule(id, ty, v)
 	default:
 		ty := g.variables.LookupType(id, val)

smt/generator_test.go

@@ -431,7 +431,7 @@ func TestTemporalSys2(t *testing.T) {
 
 func TestTestData(t *testing.T) {
 	specs := []string{
-		"testdata/bathtub.fspec",
+		/*"testdata/bathtub.fspec",
 		"testdata/simple.fspec",
 		"testdata/bathtub2.fspec",
 		"testdata/booleans.fspec",
@@ -440,10 +440,11 @@ func TestTestData(t *testing.T) {
 		"testdata/swaps/swaps1.fspec",
 		"testdata/swaps/swaps2.fspec",
 		"testdata/indexes.fspec",
-		"testdata/strings.fspec",
+		"testdata/strings.fspec",*/
+		"testdata/strings2.fspec",
 	}
 	smt2s := []string{
-		"testdata/bathtub.smt2",
+		/*"testdata/bathtub.smt2",
 		"testdata/simple.smt2",
 		"testdata/bathtub2.smt2",
 		"testdata/booleans.smt2",
@@ -452,7 +453,8 @@ func TestTestData(t *testing.T) {
 		"testdata/swaps/swaps1.smt2",
 		"testdata/swaps/swaps2.smt2",
 		"testdata/indexes.smt2",
-		"testdata/strings.smt2",
+		"testdata/strings.smt2",*/
+		"testdata/strings2.smt2",
 	}
 	for i, s := range specs {
 		data, err := os.ReadFile(s)

smt/rules/rules.go

@@ -11,6 +11,7 @@ import (
 type Rule interface {
 	ruleNode()
 	String() string
+	Assertless() string
 }
 
 type Ands struct {
@@ -27,6 +28,13 @@ func (a *Ands) String() string {
 	}
 	return out.String()
 }
+func (a *Ands) Assertless() string {
+	var ands string
+	for _, asrt := range a.X {
+		ands = fmt.Sprintf("%s %s", ands, asrt.Assertless())
+	}
+	return fmt.Sprintf("(and %s)", ands)
+}
 func (a *Ands) Tag(k1 string, k2 string) {
 	a.tag = &branch{
 		branch: k1,
@@ -38,7 +46,7 @@ type States struct {
 	Rule
 	Terminal bool
 	Base     string
-	States   map[int][]string //
+	States   map[int][]string
 	Constant bool
 	tag      *branch
 }
@@ -47,6 +55,9 @@ func (s *States) ruleNode() {}
 func (s *States) String() string {
 	return s.Base
 }
+func (s *States) Assertless() string {
+	return ""
+}
 func (s *States) Tag(k1 string, k2 string) {
 	s.tag = &branch{
 		branch: k1,
@@ -68,6 +79,9 @@ func (a *Assrt) ruleNode() {}
 func (a *Assrt) String() string {
 	return a.Variable.String() + a.Conjunction + a.Assertion.String()
 }
+func (a *Assrt) Assertless() string {
+	return ""
+}
 func (a *Assrt) Tag(k1 string, k2 string) {
 	a.tag = &branch{
 		branch: k1,
@@ -93,6 +107,9 @@ func (c *Choices) String() string {
 	}
 	return out.String()
 }
+func (c *Choices) Assertless() string {
+	return ""
+}
 func (c *Choices) Tag(k1 string, k2 string) {
 	c.tag = &branch{
 		branch: k1,
@@ -113,6 +130,9 @@ func (i *Infix) ruleNode() {}
 func (i *Infix) String() string {
 	return fmt.Sprintf("%s %s %s", i.X.String(), i.Op, i.Y.String())
 }
+func (i *Infix) Assertless() string {
+	return fmt.Sprintf("(%s %s %s)", i.Op, i.X.Assertless(), i.Y.Assertless())
+}
 func (i *Infix) Tag(k1 string, k2 string) {
 	i.tag = &branch{
 		branch: k1,
@@ -132,6 +152,9 @@ func (pr *Prefix) ruleNode() {}
 func (pr *Prefix) String() string {
 	return fmt.Sprintf("%s %s", pr.Op, pr.X.String())
 }
+func (pr *Prefix) Assertless() string {
+	return fmt.Sprintf("(%s %s)", pr.Op, pr.X)
+}
 func (pr *Prefix) Tag(k1 string, k2 string) {
 	pr.tag = &branch{
 		branch: k1,
@@ -151,6 +174,18 @@ func (it *Ite) ruleNode() {}
 func (it *Ite) String() string {
 	return fmt.Sprintf("if %s then %s else %s", it.Cond.String(), it.T, it.F)
 }
+func (it *Ite) Assertless() string {
+	var t, f string
+	for _, tr := range it.T {
+		t = fmt.Sprintf("%s %s", t, tr.Assertless())
+	}
+
+	for _, fa := range it.F {
+		t = fmt.Sprintf("%s %s", f, fa.Assertless())
+	}
+	return fmt.Sprintf("(ite (%s) (%s) (%s))", it.Cond.Assertless(), t, f)
+}
+
 func (ite *Ite) Tag(k1 string, k2 string) {
 	ite.tag = &branch{
 		branch: k1,
@@ -173,6 +208,9 @@ func (i *Invariant) String() string {
 	}
 	return fmt.Sprint(i.Left.String(), i.Operator, i.Right.String())
 }
+func (i *Invariant) Assertless() string {
+	return fmt.Sprintf("(%s %s %s)", i.Operator, i.Left.Assertless(), i.Right.Assertless())
+}
 func (i *Invariant) Tag(k1 string, k2 string) {
 	i.tag = &branch{
 		branch: k1,
@@ -197,6 +235,9 @@ func (p *Phi) String() string {
 	}
 	return out.String()
 }
+func (p *Phi) Assertless() string {
+	return ""
+}
 func (p *Phi) Tag(k1 string, k2 string) {
 	p.tag = &branch{
 		branch: k1,
@@ -224,6 +265,9 @@ func (sc *StateChange) String() string {
 	}
 	return out.String()
 }
+func (sc *StateChange) Assertless() string {
+	return ""
+}
 func (sc *StateChange) Tag(k1 string, k2 string) {
 	sc.tag = &branch{
 		branch: k1,
@@ -244,6 +288,9 @@ func (w *Wrap) ruleNode() {}
 func (w *Wrap) String() string {
 	return w.Value
 }
+func (w *Wrap) Assertless() string {
+	return w.String()
+}
 func (w *Wrap) Tag(k1 string, k2 string) {
 	w.tag = &branch{
 		branch: k1,
@@ -274,6 +321,9 @@ func (sg *StateGroup) String() string {
 	}
 	return out.String()
 }
+func (sg *StateGroup) Assertless() string {
+	return ""
+}
 func (sg *StateGroup) Tag(k1 string, k2 string) {
 	sg.tag = &branch{
 		branch: k1,
@@ -295,6 +345,9 @@ func (wg *WrapGroup) String() string {
 	}
 	return out.String()
 }
+func (wg *WrapGroup) Assertless() string {
+	return ""
+}
 func (wg *WrapGroup) Tag(k1 string, k2 string) {
 	wg.tag = &branch{
 		branch: k1,
@@ -312,6 +365,9 @@ func (vw *Vwrap) ruleNode() {}
 func (vw *Vwrap) String() string {
 	return vw.Value.String()
 }
+func (vw *Vwrap) Assertless() string {
+	return ""
+}
 func (vw *Vwrap) Tag(k1 string, k2 string) {
 	vw.tag = &branch{
 		branch: k1,

smt/testdata/strings2.fspec

@@ -0,0 +1,9 @@
+spec test;
+str1 = "is a fish";
+str2 = "tastes delicious with ginger";
+str3 = "native to North America";
+str4 = "walks on four legs";
+str5 = "has a tail";
+str6 = "is blue";
+str7 = (str1 && str2) || (str3 && str4);
+str8 = str6 || str5 && str1; 

smt/testdata/strings2.smt2

@@ -0,0 +1,17 @@
+(set-logic QF_NRA)
+(declare-fun test_str1_0 () Bool)
+(declare-fun test_str2_0 () Bool)
+(declare-fun test_str3_0 () Bool)
+(declare-fun test_str4_0 () Bool)
+(declare-fun test_str5_0 () Bool)
+(declare-fun test_str6_0 () Bool)
+(declare-fun test_str3_test_str4_0 () Bool)
+(declare-fun test_str1_test_str2_0 () Bool)
+(declare-fun test_str7_0 () Bool)
+(declare-fun test_str5_test_str1_0 () Bool)
+(declare-fun test_str8_0 () Bool)
+(assert (= test_str3_test_str4_0 (and test_str3_0 test_str4_0)))
+(assert (= test_str1_test_str2_0 (and test_str1_0 test_str2_0)))
+(assert (= test_str7_0 (or test_str3_test_str4_0 test_str1_test_str2_0)))
+(assert (= test_str5_test_str1_0 (and test_str5_0test_str1_0)))
+(assert (= test_str8_0 (or test_str5_test_str1_0 test_str6_0)))