Skip to content

Commit

Permalink
Bellmar/whens thens (#24)
Browse files Browse the repository at this point in the history 
* tightening up the functions around VarRounds

* breaking out assert/assume generation into smaller functions

* renaming parse functions that don't involve parsing to create XXX rule functions

* moving rules to their own subpackage

* moving variable data over to own package and starting generator

* moving fork logic to its own package

* cleaning up and consolidating old test files

* updating command line interface to be consistent across Docker and main.go

* removing a lot of dead code
  • Loading branch information
@mbellotti
mbellotti committed Feb 24, 2023
1 parent 2b993de commit f13fec5
Show file tree
Hide file tree
Showing 3 changed files with 21 additions and 398 deletions.
264 changes: 0 additions & 264 deletions smt/asserts.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,6 @@ import (
"fault/smt/rules"
"fault/util"
"fmt"
"sort"
"strconv"
"strings"
)
Expand Down Expand Up @@ -392,58 +391,6 @@ func invalidBase(base string) bool {
return false
}

func (g *Generator) generateAsserts(exp ast.Expression, comp string, constr ast.Expression, stmt *ast.AssertionStatement) []*rules.Assrt {
var ident []string
var assrt []*rules.Assrt
switch v := exp.(type) {
case *ast.InfixExpression:
ident = g.findIdent(v)
for _, id := range ident {
assrt = append(assrt, g.packageAssert(id, comp, v, stmt))
}
return assrt
case *ast.PrefixExpression:
ident = g.findIdent(v)
for _, id := range ident {
assrt = append(assrt, g.packageAssert(id, comp, v, stmt))
}
return assrt
case *ast.Identifier:
ident = g.findIdent(v)
for _, id := range ident {
assrt = append(assrt, g.packageAssert(id, comp, constr, stmt))
}
return assrt
case *ast.ParameterCall:
ident = g.findIdent(v)
for _, id := range ident {
assrt = append(assrt, g.packageAssert(id, comp, constr, stmt))
}
return assrt
case *ast.AssertVar:
for _, inst := range v.Instances {
assrt = append(assrt, g.packageAssert(inst, comp, constr, stmt))
}
return assrt
case *ast.IndexExpression:
ident = g.findIdent(v)
for _, id := range ident {
assrt = append(assrt, g.packageAssert(id, comp, constr, stmt))
}
return assrt
case *ast.IntegerLiteral:
return assrt
case *ast.FloatLiteral:
return assrt
case *ast.StringLiteral:
return assrt
case *ast.Boolean:
return assrt
default:
panic(fmt.Sprintf("poorly formatted assert statement got=%T", exp))
}
}

func (g *Generator) parseInvariant(ex ast.Expression) rules.Rule {
switch e := ex.(type) {
case *ast.InvariantClause:
Expand Down Expand Up @@ -553,221 +500,10 @@ func (g *Generator) parseInvariant(ex ast.Expression) rules.Rule {
return nil
}

type thenStates struct {
roundClauses []string
values [][][]string
}

func (g *Generator) generateThenRules(inv *rules.Invariant) []string {
when := g.whenInfixNode(inv.Left)
//then := g.thenInfixNode(inv.Right)
fmt.Println(when)
//fmt.Println(then)
return []string{}
}

// check rounds for any matching variable names

// Generate all permutations of variables in the assert,
// in the round, in between variable state change

func (g *Generator) whenInfixNode(ru rules.Rule) map[string]*thenStates {
ret := make(map[string]*thenStates)
switch r := ru.(type) {
case *rules.Invariant:
left := g.whenInfixNode(r.Left)
for k, v := range left {
ret[k] = v
}

right := g.whenInfixNode(r.Right)
for k, v := range right {
ret[k] = v
}

return ret
case *rules.Wrap:
roundClause, values := g.whenNode(r)
ret[r.Value] = &thenStates{
roundClauses: roundClause,
values: values,
}
return ret
}
return ret
}

func (g *Generator) whenNode(when *rules.Wrap) ([]string, [][][]string) {
var roundClauses []string
var values [][][]string
base := when.Value
rounds := g.lookupVarRounds(when.Value, when.State)
for _, r := range rounds {
roundClauses = append(roundClauses, fmt.Sprintf("(= %s_%d %s)", base, r[0], "true"))
values = append(values, g.RoundVars[r[1]][r[2]:])
}
return roundClauses, values
}

func (g *Generator) packageAssert(ident string, comp string, expr ast.Expression, stmt *ast.AssertionStatement) *rules.Assrt {
var temporalFilter string
var temporalN int

temporalFilter = stmt.TemporalFilter
temporalN = stmt.TemporalN

s, a, c := captureState(ident)
w := &rules.Wrap{Value: ident,
State: s,
All: a,
Constant: c,
}
return &rules.Assrt{
Variable: w,
Conjunction: comp,
Assertion: g.parseInvariant(expr),
TemporalFilter: temporalFilter,
TemporalN: temporalN}
}

func (g *Generator) convertIndexExpr(idx *ast.IndexExpression) string {
return strings.Join([]string{idx.Left.String(), idx.Index.String()}, "_")
}

func (g *Generator) findIdent(n ast.Node) []string {
switch v := n.(type) {
case *ast.InfixExpression:
return g.findIdent(v.Left)
case *ast.PrefixExpression:
return g.findIdent(v.Right)
case *ast.IndexExpression:
s := g.convertIndexExpr(v)
return []string{s}
case *ast.Identifier:
return []string{v.Value}
case *ast.ParameterCall:
return []string{strings.Join(v.Value, "_")}
case *ast.AssertVar:
return v.Instances
default:
pos := n.Position()
panic(fmt.Sprintf("improperly formatted assert or assume line: %d, col: %d", pos[0], pos[1]))
}
}

func (g *Generator) generateAssertRules(ru rules.Rule, t string, tn int) []string {
// assert x == true;
// negated: x != true;
// (assert (or (= x0 false) (= x1 false) (= x2 false)))

// assert x > 5 && x < 2;
// negated: x <= 5 || x >= 2
// (assert (or (<= x0 5) (<= x1 5) (<= x2 5) (>= x0 2) (>= x1 2) (>= x2 2)))

// assert x > 5 || x < 2;
// negated: x <= 5 && x >= 2
// (assert (and (or (<= x0 5) (<= x1 5) (<= x2 5))
// (or (>= x0 2) (>= x1 2) (>= x2 2))))

//assert x > y
// negated: x <= y
// What states overlap in the same round? :/
// Actually does this matter?
// (assert (or (<= x0 y0) (<= x1 y1) (<= x2 y2)))
var i *rules.Invariant
switch r := ru.(type) {
case *rules.Assrt:
return g.generateAssertRules(r.Assertion, t, tn)
case *rules.Invariant:
if r.Operator == "then" {
return g.generateThenRules(r)
}
i = r
case *rules.Wrap:
return g.wrapPerm(r)
case *rules.WrapGroup:
var wg []string
for _, v := range r.Wraps {
wg = append(wg, g.wrapPerm(v)...)
}
return wg
default:
panic(fmt.Sprintf("Improperly formatted assertion %s", r.String()))
}

var left, right []string
switch l := i.Left.(type) {
case *rules.Invariant:
left = g.generateAssertRules(l, t, tn)
case *rules.Wrap:
left = g.wrapPerm(l)
default:
left = nil
}

switch r := i.Right.(type) {
case *rules.Invariant:
right = g.generateAssertRules(r, t, tn)
case *rules.Wrap:
right = g.wrapPerm(r)
default:
right = nil
}

if left == nil { // Typically (not (some rule))
var ret []string
for _, r := range right {
ret = append(ret, fmt.Sprintf("(%s %s)", i.Operator, r))
}
return ret
}

return expandAssertStateGraph(left, right, i.Operator, t, tn)
}

func (g *Generator) filterOutTempStates(v string, i int16) bool {
for _, opt := range g.forks {
choices := opt[v]
for _, c := range choices {
if len(c.Values) == 1 {
return false
}

c.Values = c.Values[1:] //First value is not temp
n := len(c.Values)
t := sort.Search(n, func(k int) bool { return c.Values[k] == i })
if t == n { //If no match in Values slice Search returns n since it cannot be confused with an index
return false
}

if c.Values[t] == i {
return true
}
}
}
return false
}

func (g *Generator) wrapPerm(w *rules.Wrap) []string {
if w.Constant {
return []string{w.Value}
} else if w.State != "" {
state := fmt.Sprint(w.Value, "_", w.State)
return []string{state}
}
if w.All {
var states []string
end := g.variables.SSA[w.Value]
for i := 0; i < int(end+1); i++ {
if !g.filterOutTempStates(w.Value, int16(i)) {
states = append(states, fmt.Sprint(w.Value, "_", i))
}
}
return states
}
panic(fmt.Sprintf("Inproperly formatted metadata for value %s in assert", w.Value))
}

func expandAssertStateGraph(list1 []string, list2 []string, op string, temporalFilter string, temporalN int) []string {
var x [][]string
c := util.Cartesian(list1, list2)
Expand Down

0 comments on commit f13fec5

Please sign in to comment.