Adding String Support (#38)

* grammar updates and converting string to boolean in ir

* debugging globally defined strings

* bug: StructInstances can also be in DefStatements

* fixed syntax issue in testdata (swaps2)

* strings as bool in smt

* first pass at compound string rules

* fixing tests

* working through some bugs with compound strings and found a bug in smt generation of prefixes

* imports weren't passing global variables up to the parent spec

* stuck in a real nasty place on ands/ors

* still very much a mess but fixed the tests at least

* forgot to add Prefix to branch tagging

* updating README.md

README.md

@@ -29,7 +29,10 @@ The development Fault is documented in the series "Marianne Writes a Programming
 - [audio](https://anchor.fm/mwapl)
 - [transcripts](https://dev.to/bellmar/series/9711)
 
-### Current Status (4/26/2023)
+### Current Status (5/24/2023)
+Introducing strings to Fault, plus fixing some bugs in the behavior of imports. Strings in Fault behave like booleans and allow easily readable rules to be defined for the model checker to solve. They are not treated as immutable but haven't yet figured out how I want to syntax to change their state to look yet.
+
+#### (4/26/2023)
 Adding support for indexes (ie accessing historical values in the model) there are some edge cases around branches that need to be worked through.
 
 #### (4/13/2023)

execute/execute.go

@@ -97,16 +97,17 @@ func (mc *ModelChecker) LoadMeta(frks []forks.Fork) {
 func (mc *ModelChecker) run(command string, actions []string) (string, error) {
 	cmd := exec.Command(mc.solver[command].Command,
 		mc.solver[command].Arguments...)
-
 	cmd.Stdin = strings.NewReader(fmt.Sprint(mc.SMT, strings.Join(actions, "\n")))
 
 	var out bytes.Buffer
+	var stderr bytes.Buffer
 	cmd.Stdout = &out
+	cmd.Stderr = &stderr
 
 	err := cmd.Run()
 
 	if err != nil {
-		return "", err
+		return "", fmt.Errorf(fmt.Sprint(err) + ": " + stderr.String())
 	}
 	return strings.TrimSpace(out.String()), err
 }

grammar/FaultParser.g4

@@ -9,7 +9,7 @@ options {
 */
 
 sysSpec
-    : sysClause importDecl* globalDecl* componentDecl* (assertion | assumption)? startBlock? forStmt?
+    : sysClause importDecl* globalDecl* componentDecl* (assertion | assumption | stringDecl)? startBlock? forStmt?
     ;
 
 sysClause
@@ -64,6 +64,7 @@ declaration
     | structDecl
     | assertion
     | assumption
+    | stringDecl
     ;
 
 comparison
@@ -83,6 +84,20 @@ constSpec
     : identList ('=' constants)?
     ;
 
+stringDecl
+    : IDENT '=' string_ eos
+    | IDENT '=' compoundString eos
+    | IDENT '=' compoundString eos
+    ;
+
+compoundString
+    : operandName
+    | '!' operandName
+    | '(' compoundString ')'
+    | compoundString '&&' compoundString
+    | compoundString '||' compoundString
+    ;
+
 identList
     : operandName (',' operandName)*
     ;

listener/listener.go

@@ -1218,6 +1218,66 @@ func (l *FaultListener) ExitFloat_(c *parser.Float_Context) {
 	})
 }
 
+func (l *FaultListener) ExitCompoundString(c *parser.CompoundStringContext) {
+	if c.GetChildCount() < 2 {
+		return //Single operand, no actions
+	}
+
+	if pre, ok := c.GetChild(0).(antlr.TerminalNode); ok && pre.GetText() == "!" {
+		token := util.GenerateToken("IDENT", "IDENT", c.GetStart(), c.GetStop())
+		exp := l.pop()
+		e := &ast.PrefixExpression{
+			Token:    token,
+			Operator: "-",
+			Right:    exp.(ast.Expression),
+		}
+		l.push(e)
+		return
+	}
+
+	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),
+		}
+		l.push(e)
+	}
+}
+
+func (l *FaultListener) ExitStringDecl(c *parser.StringDeclContext) {
+	token := util.GenerateToken("GLOBAL", "GLOBAL", c.GetStart(), c.GetStop())
+
+	val := l.pop()
+	token2 := util.GenerateToken("IDENT", "IDENT", c.GetStart(), c.GetStop())
+
+	ident := &ast.Identifier{
+		Token: token2,
+		Value: c.IDENT().GetText(),
+		Spec:  l.currSpec,
+	}
+	switch val.(type) {
+	case *ast.StringLiteral:
+		l.push(&ast.DefStatement{Token: token, Name: ident, Value: val.(ast.Expression)})
+	case *ast.InfixExpression:
+		token2 := util.GenerateToken("COMPOUND_STRING", "COMPOUND_STRING", c.GetStart(), c.GetStop())
+		val.(*ast.InfixExpression).Token = token2
+		l.push(&ast.DefStatement{Token: token, Name: ident, Value: val.(ast.Expression)})
+	case *ast.PrefixExpression:
+		token2 := util.GenerateToken("COMPOUND_STRING", "COMPOUND_STRING", c.GetStart(), c.GetStop())
+		val.(*ast.PrefixExpression).Token = token2
+		l.push(&ast.DefStatement{Token: token, Name: ident, Value: val.(ast.Expression)})
+	default:
+		panic(fmt.Sprintf("top of the stack is not a string got %T: line %d col %d", val, c.GetStart().GetLine(), c.GetStart().GetColumn()))
+	}
+}
+
 func (l *FaultListener) ExitString_(c *parser.String_Context) {
 	token := util.GenerateToken("STRING", "STRING", c.GetStart(), c.GetStop())
 

llvm/alloc.go

@@ -70,6 +70,20 @@ func (c *Compiler) allocVariable(id []string, val value.Value, pos []int) {
 		alloc = c.contextBlock.NewAlloca(irtypes.I1)
 		alloc.SetName(name)
 		store = c.contextBlock.NewStore(v, alloc)
+	case *ir.InstAnd:
+		alloc = c.contextBlock.NewAlloca(irtypes.I1)
+		alloc.SetName(name)
+		if v.Type() == nil {
+			v.Typ = irtypes.I1
+		}
+		store = c.contextBlock.NewStore(v, alloc)
+	case *ir.InstOr:
+		alloc = c.contextBlock.NewAlloca(irtypes.I1)
+		alloc.SetName(name)
+		if v.Type() == nil {
+			v.Typ = irtypes.I1
+		}
+		store = c.contextBlock.NewStore(v, alloc)
 	case *ir.Func:
 		return
 	default:
@@ -115,6 +129,14 @@ func (c *Compiler) globalVariable(id []string, val value.Value, pos []int) {
 	case *ir.InstFCmp:
 		c.allocVariable(id, val, pos)
 	case *ir.Func:
+	case *ir.InstAnd:
+		placeholder := constant.NewAnd(v.X.(constant.Expression), v.Y.(constant.Expression))
+		alloc := c.module.NewGlobalDef(name, placeholder)
+		c.storeGlobal(name, alloc)
+	case *ir.InstOr:
+		placeholder := constant.NewOr(v.X.(constant.Expression), v.Y.(constant.Expression))
+		alloc := c.module.NewGlobalDef(name, placeholder)
+		c.storeGlobal(name, alloc)
 	default:
 		panic(fmt.Sprintf("unknown variable type %T line: %d col: %d", v, pos[0], pos[1]))
 	}