Skip to content

Commit

Permalink
maybe got all the bugs out of assert outputs
Browse files Browse the repository at this point in the history
  • Loading branch information
@mbellotti
mbellotti committed Aug 25, 2023
1 parent 723ceaa commit 17f6ea8
Show file tree
Hide file tree
Showing 6 changed files with 274 additions and 46 deletions.
2 changes: 1 addition & 1 deletion ast/ast.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -326,7 +326,7 @@ func (as *AssertionStatement) String() string {
}
func (as *AssertionStatement) EvLogString() string {
var out bytes.Buffer
if !as.Violated {
if as.Violated {
out.WriteString("FAILED ")
} else {
out.WriteString("OK ")
Expand Down
207 changes: 180 additions & 27 deletions execute/execute.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,13 +5,15 @@ import (
"errors"
"fault/execute/parser"
"fault/smt/forks"
"fault/smt/log"
resultlog "fault/smt/log"
"fault/smt/rules"
"fault/smt/variables"
"fault/util"
"fmt"
"os"
"os/exec"
"strconv"
"strings"

"github.com/antlr/antlr4/runtime/Go/antlr/v4"
Expand Down Expand Up @@ -157,30 +159,59 @@ func (mc *ModelChecker) Eval(a *resultlog.Assert) bool {
case "not":
return mc.EvalAmbiguous(a)
case ">":
left := a.Left.GetFloat()
right := a.Right.GetFloat()
left := mc.ConvertClause(a.Left)
right := mc.ConvertClause(a.Right)

res := left > right
mc.Log.StoreEval(a, res)
return res
case ">=":
left := a.Left.GetFloat()
right := a.Right.GetFloat()
left := mc.ConvertClause(a.Left)
right := mc.ConvertClause(a.Right)

res := left >= right
mc.Log.StoreEval(a, res)
return res
case "<":
left := a.Left.GetFloat()
right := a.Right.GetFloat()
left := mc.ConvertClause(a.Left)
right := mc.ConvertClause(a.Right)

res := left < right
mc.Log.StoreEval(a, res)
return res
case "<=":
left := a.Left.GetFloat()
right := a.Right.GetFloat()
left := mc.ConvertClause(a.Left)
right := mc.ConvertClause(a.Right)

res := left <= right
mc.Log.StoreEval(a, res)
return res
case "and":
if a.Left.Type() == "MULTI" {
//Make sure the subclauses are handled first
if ch, ok2 := mc.Log.AssertChains[a.Left.String()]; ok2 {
if len(ch.Chain) > 0 {
chain := make(map[string]*rules.AssertChain)
chain[a.Left.String()] = ch
mc.CheckAsserts(chain)
} else {
i := mc.LookupClause(a.Left.String())
if i < 0 {
panic(fmt.Errorf("cannot find clause for %s", a.Left.String()))
}
mc.Eval(mc.Log.Asserts[i])
}

// Now handle the main clause
res := mc.EvalAmbiguous(a)
mc.Log.StoreEval(a, res)
return res
} else {
panic(fmt.Errorf("cannot find clause for %s", a.Left.String()))
}
}

// Or just try the normal way :)
left, err := mc.EvalClause(a.Left)
if err != nil {
panic(err)
Expand All @@ -192,7 +223,32 @@ func (mc *ModelChecker) Eval(a *resultlog.Assert) bool {
res := left && right
mc.Log.StoreEval(a, res)
return res

case "or":
if a.Left.Type() == "MULTI" {
//Make sure the subclauses are handled first
if ch, ok2 := mc.Log.AssertChains[a.Left.String()]; ok2 {
if len(ch.Chain) > 0 {
chain := make(map[string]*rules.AssertChain)
chain[a.Left.String()] = ch
mc.CheckAsserts(chain)
} else {
i := mc.LookupClause(a.Left.String())
if i < 0 {
panic(fmt.Errorf("cannot find clause for %s", a.Left.String()))
}
mc.Eval(mc.Log.Asserts[i])
}

// Now handle the main clause
res := mc.EvalAmbiguous(a)
mc.Log.StoreEval(a, res)
return res
} else {
panic(fmt.Errorf("cannot find clause for %s", a.Left.String()))
}
}

left, err := mc.EvalClause(a.Left)
if err != nil {
panic(err)
Expand All @@ -210,7 +266,7 @@ func (mc *ModelChecker) Eval(a *resultlog.Assert) bool {
}

func (mc *ModelChecker) EvalAmbiguous(a *resultlog.Assert) bool {
if a.Left.Type() != a.Right.Type() {
if a.Left.Type() != a.Right.Type() && a.Left.Type() != "MULTI" {
panic(fmt.Sprintf("improperly formatted assertion clause %s got type left %s and type right %s", a.String(), a.Left.Type(), a.Right.Type()))
}

Expand All @@ -233,16 +289,91 @@ func (mc *ModelChecker) EvalAmbiguous(a *resultlog.Assert) bool {
res = a.Left.GetBool() != a.Right.GetBool()
}
case "STRING":
if a.Op == "=" {
left := mc.ResultValues[a.Left.GetString()]
right := mc.ResultValues[a.Right.GetString()]
res = left == right
}
if a.Op == "=" || a.Op == "not" {
var left string
var right string
var ok bool
clauseL := a.Left.GetString()
clauseR := a.Right.GetString()
if left, ok = mc.ResultValues[clauseL]; !ok {
if leftres, ok := mc.Log.AssertClauses[clauseL]; ok {
left = fmt.Sprintf("%v", leftres)
} else if leftClause, ok2 := mc.Log.AssertChains[clauseL]; ok2 {
lc := make(map[string]*rules.AssertChain)
lc[clauseL] = leftClause
mc.CheckAsserts(lc)
leftres := mc.Log.AssertClauses[clauseL]
left = fmt.Sprintf("%v", leftres)
} else {
panic(fmt.Sprintf("Cannot find clause %s", clauseL))
}
}

if a.Op == "not" {
left := mc.ResultValues[a.Left.GetString()]
right := mc.ResultValues[a.Right.GetString()]
res = left != right
if right, ok = mc.ResultValues[clauseR]; !ok {
if rightres, ok := mc.Log.AssertClauses[clauseR]; ok {
right = fmt.Sprintf("%v", rightres)
} else if rightClause, ok2 := mc.Log.AssertChains[clauseR]; ok2 {
rc := make(map[string]*rules.AssertChain)
rc[clauseR] = rightClause
mc.CheckAsserts(rc)
rightres := mc.Log.AssertClauses[clauseR]
right = fmt.Sprintf("%v", rightres)
} else {
panic(fmt.Sprintf("Cannot find clause %s", clauseR))
}
}

if a.Op == "not" {
res = left != right
} else {
res = left == right
}
}
case "MULTI":
if a.Op == "and" { // ANDs every clause must be true
var ok bool
for _, v := range a.Left.(*log.MultiClause).Value {
if res, ok = mc.Log.AssertClauses[v]; ok {
if !res {
break
}
} else {
c := make(map[string]*rules.AssertChain)
c[v] = mc.Log.AssertChains[v]
c[v].Chain = []int{mc.LookupClause(v)}
mc.CheckAsserts(c)
if res, ok = mc.Log.AssertClauses[v]; ok {
if !res {
break
}
} else {
panic(fmt.Sprintf("missing clause %s", v))
}
}
}
res = true
} else { //ORs only one need be true
for _, v := range a.Left.(*log.MultiClause).Value {
if r, ok := mc.Log.AssertClauses[v]; ok {
if r {
res = true
break
}
} else {
c := make(map[string]*rules.AssertChain)
c[v] = mc.Log.AssertChains[v]
c[v].Chain = []int{mc.LookupClause(v)}
mc.CheckAsserts(c)
if res, ok = mc.Log.AssertClauses[v]; ok {
if !res {
break
}
} else {
panic(fmt.Sprintf("missing clause %s", v))
}
}
}
res = false
}
}
mc.Log.StoreEval(a, res)
Expand All @@ -258,22 +389,44 @@ func (mc *ModelChecker) EvalClause(c resultlog.Clause) (bool, error) {
return false, nil // where Left clause will be x y z and Right clause will be ""
}

if cl, ok := mc.Log.AssertClauses[c.GetString()]; ok {
return cl, nil
}
if ch, ok2 := mc.Log.AssertChains[c.GetString()]; ok2 {
chain := make(map[string]*rules.AssertChain)
chain[c.GetString()] = ch
mc.CheckAsserts(chain)
return mc.Log.AssertClauses[c.GetString()], nil
ret, ok := mc.Log.AssertClauses[c.GetString()]
if !ok {
return false, fmt.Errorf("assertion clause %s not found", c.GetString())
}
return ret, nil

return false, fmt.Errorf("assertion clause %s not found", c.GetString())
default:
return false, fmt.Errorf("illegal assertion clause %s typed %s", c.GetString(), c.Type())
}
}

func (mc *ModelChecker) ConvertClause(a resultlog.Clause) float64 {
var val float64
var err error
switch a.Type() {
case "INT":
val = float64(a.GetInt())
case "FLOAT":
val = a.GetFloat()
case "STRING":
temp := mc.ResultValues[a.String()]
val, err = strconv.ParseFloat(temp, 64)
if err != nil {
panic(err)
}
}
return val
}

func (mc *ModelChecker) LookupClause(clause string) int {
for i, a := range mc.Log.Asserts {
if a.String() == clause {
return i
}
}
return -1
}

func (mc *ModelChecker) stateAssessment(dist distuv.Normal, states Scenario) Scenario {
var weighted Scenario
switch s := states.(type) {
Expand Down
2 changes: 1 addition & 1 deletion execute/format.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -191,7 +191,7 @@ func (mc *ModelChecker) dontBackTrack(clauses map[string]bool, subclause string)
// Formatter may iterate through assert clauses in any order, don't backtrack
// through subclauses we've already evaluated

for clause, _ := range clauses {
for clause := range clauses {
if len(subclause) > len(clause) { //Can't possibly be a subclause
return true
}
Expand Down

0 comments on commit 17f6ea8

Please sign in to comment.