Skip to content

Commit

Permalink
renaming parse functions that don't involve parsing to create XXX rul…
Browse files Browse the repository at this point in the history 
…e functions
  • Loading branch information
@mbellotti
mbellotti committed Feb 21, 2023
1 parent 6143cc8 commit 33e3729
Show file tree
Hide file tree
Showing 3 changed files with 32 additions and 32 deletions.
10 changes: 5 additions & 5 deletions smt/parse_unit_test.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ func TestTagRules(t *testing.T) {
}
}

func TestParseCond(t *testing.T) {
func TestcreateCondRule(t *testing.T) {
g := NewGenerator()
cond := &infix{
x: &wrap{
Expand All @@ -68,10 +68,10 @@ func TestParseCond(t *testing.T) {
},
op: ">",
}
inst := g.parseCond(cond)
inst := g.createCondRule(cond)

if inst.(*infix).y.(*wrap).value != "y" {
t.Fatalf("parseCond returns the wrong value. got=%s", inst.(*infix).String())
t.Fatalf("createCondRule returns the wrong value. got=%s", inst.(*infix).String())
}

cond2 := &infix{
Expand All @@ -85,10 +85,10 @@ func TestParseCond(t *testing.T) {
},
op: "true",
}
inst2 := g.parseCond(cond2)
inst2 := g.createCondRule(cond2)

if inst2.(*infix).y.(*wrap).value != "True" {
t.Fatalf("parseCond returns the wrong value. got=%s", inst2.(*infix).String())
t.Fatalf("createCondRule returns the wrong value. got=%s", inst2.(*infix).String())
}
}

Expand Down
12 changes: 6 additions & 6 deletions smt/rules_types.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -241,7 +241,7 @@ type stateGroup struct {
tag *branch
}

func NewStateGroup () *stateGroup {
func NewStateGroup() *stateGroup {
sg := &stateGroup{}
sg.bases = util.NewStrSet()
return sg
Expand Down Expand Up @@ -363,7 +363,7 @@ func (g *Generator) storeRule(inst *ir.InstStore) []rule {
v = fmt.Sprintf("%s_%d", v, n)
}
g.AddNewVarChange(base, id, prev)
rules = append(rules, g.parseRule(id, v, ty, ""))
rules = append(rules, g.createRule(id, v, ty, ""))
} else if ref, ok := g.variables.ref[refname]; ok {
switch r := ref.(type) {
case *infix:
Expand Down Expand Up @@ -417,7 +417,7 @@ func (g *Generator) storeRule(inst *ir.InstStore) []rule {
id := g.variables.advanceSSA(base)
g.addVarToRound(base, int(g.variables.ssa[base]))
g.AddNewVarChange(base, id, prev)
rules = append(rules, g.parseRule(id, inst.Src.Ident(), ty, ""))
rules = append(rules, g.createRule(id, inst.Src.Ident(), ty, ""))
}
return rules
}
Expand All @@ -430,7 +430,7 @@ func (g *Generator) xorRule(inst *ir.InstXor) rule {
x = g.variables.convertIdent(g.currentFunction, x)
xRule = &wrap{value: x}
}
return g.parseMultiCond(id, xRule, &wrap{}, "not")
return g.createMultiCondRule(id, xRule, &wrap{}, "not")
}

func (g *Generator) andRule(inst *ir.InstAnd) rule {
Expand All @@ -449,7 +449,7 @@ func (g *Generator) andRule(inst *ir.InstAnd) rule {
y = g.variables.convertIdent(g.currentFunction, y)
yRule = &wrap{value: y}
}
return g.parseMultiCond(id, xRule, yRule, "and")
return g.createMultiCondRule(id, xRule, yRule, "and")
}

func (g *Generator) orRule(inst *ir.InstOr) rule {
Expand All @@ -467,7 +467,7 @@ func (g *Generator) orRule(inst *ir.InstOr) rule {
y = g.variables.convertIdent(g.currentFunction, y)
yRule = &wrap{value: y}
}
return g.parseMultiCond(id, xRule, yRule, "or")
return g.createMultiCondRule(id, xRule, yRule, "or")
}

func (g *Generator) stateRules(key string, sc *stateChange) rule {
Expand Down
42 changes: 21 additions & 21 deletions smt/smt_parse.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -176,34 +176,34 @@ func (g *Generator) parseInstruct(block *ir.Block) []rule {
}
case *ir.InstFAdd:
var r rule
r = g.parseInfix(inst.Ident(),
r = g.createInfixRule(inst.Ident(),
inst.X.Ident(), inst.Y.Ident(), "+")
g.tempRule(inst, r)
case *ir.InstFSub:
var r rule
r = g.parseInfix(inst.Ident(),
r = g.createInfixRule(inst.Ident(),
inst.X.Ident(), inst.Y.Ident(), "-")
g.tempRule(inst, r)
case *ir.InstFMul:
var r rule
r = g.parseInfix(inst.Ident(),
r = g.createInfixRule(inst.Ident(),
inst.X.Ident(), inst.Y.Ident(), "*")
g.tempRule(inst, r)
case *ir.InstFDiv:
var r rule
r = g.parseInfix(inst.Ident(),
r = g.createInfixRule(inst.Ident(),
inst.X.Ident(), inst.Y.Ident(), "/")
g.tempRule(inst, r)
case *ir.InstFRem:
//Cannot be implemented because SMT solvers do poorly with modulo
case *ir.InstFCmp:
var r rule
op, y := g.parseCompare(inst.Pred.String())
op, y := g.createCompareRule(inst.Pred.String())
if op == "true" || op == "false" {
r = g.parseInfix(inst.Ident(),
r = g.createInfixRule(inst.Ident(),
inst.X.Ident(), y.(*wrap).value, op)
} else {
r = g.parseInfix(inst.Ident(),
r = g.createInfixRule(inst.Ident(),
inst.X.Ident(), inst.Y.Ident(), op)
}

Expand All @@ -219,12 +219,12 @@ func (g *Generator) parseInstruct(block *ir.Block) []rule {
rules = append(rules, r)
case *ir.InstICmp:
var r rule
op, y := g.parseCompare(inst.Pred.String())
op, y := g.createCompareRule(inst.Pred.String())
if op == "true" || op == "false" {
r = g.parseInfix(inst.Ident(),
r = g.createInfixRule(inst.Ident(),
inst.X.Ident(), y.(*wrap).value, op)
} else {
r = g.parseInfix(inst.Ident(),
r = g.createInfixRule(inst.Ident(),
inst.X.Ident(), inst.Y.Ident(), op)
}

Expand Down Expand Up @@ -443,7 +443,7 @@ func (g *Generator) parseBuiltIn(call *ir.InstCall, complex bool) []rule {
if complex {
g.declareVar(newState, "Bool")
}
r1 := g.parseRule(newState, "true", "Bool", "=")
r1 := g.createRule(newState, "true", "Bool", "=")

if g.currentFunction[len(g.currentFunction)-7:] != "__state" {
panic("calling advance from outside the state chart")
Expand All @@ -464,7 +464,7 @@ func (g *Generator) parseBuiltIn(call *ir.InstCall, complex bool) []rule {
if complex {
g.declareVar(currentState, "Bool")
}
r2 := g.parseRule(currentState, "false", "Bool", "=")
r2 := g.createRule(currentState, "false", "Bool", "=")
return []rule{r1, r2}
}

Expand All @@ -482,27 +482,27 @@ func (g *Generator) isBranchClosed(t []rule, f []rule) bool {
return false
}

func (g *Generator) parseRule(id string, val string, ty string, op string) rule {
func (g *Generator) createRule(id string, val string, ty string, op string) rule {
wid := &wrap{value: id}
wval := &wrap{value: val}
return &infix{x: wid, ty: ty, y: wval, op: op}
}

func (g *Generator) parseInfix(id string, x string, y string, op string) rule {
func (g *Generator) createInfixRule(id string, x string, y string, op string) rule {
x = g.convertInfixVar(x)
y = g.convertInfixVar(y)

refname := fmt.Sprintf("%s-%s", g.currentFunction, id)
g.variables.ref[refname] = g.parseRule(x, y, "", op)
g.variables.ref[refname] = g.createRule(x, y, "", op)
return g.variables.ref[refname]
}

func (g *Generator) parseCond(cond rule) rule {
func (g *Generator) createCondRule(cond rule) rule {
switch inst := cond.(type) {
case *wrap:
return inst
case *infix:
op, y := g.parseCompare(inst.op)
op, y := g.createCompareRule(inst.op)
inst.op = op
if op == "true" || op == "false" {
inst.y = y
Expand All @@ -513,15 +513,15 @@ func (g *Generator) parseCond(cond rule) rule {
}
}

func (g *Generator) parseMultiCond(id string, x rule, y rule, op string) rule {
func (g *Generator) createMultiCondRule(id string, x rule, y rule, op string) rule {
refname := fmt.Sprintf("%s-%s", g.currentFunction, id)
g.variables.ref[refname] = &infix{x: x, ty: "Bool", y: y, op: op}
return g.variables.ref[refname]
}

func (g *Generator) parseCompare(op string) (string, rule) {
func (g *Generator) createCompareRule(op string) (string, rule) {
var y *wrap
op = g.parseCompareOp(op)
op = g.compareRuleOp(op)
switch op {
case "false":
y = &wrap{value: "False"}
Expand All @@ -531,7 +531,7 @@ func (g *Generator) parseCompare(op string) (string, rule) {
return op, y
}

func (g *Generator) parseCompareOp(op string) string {
func (g *Generator) compareRuleOp(op string) string {
switch op {
case "false":
return "false"
Expand Down

0 comments on commit 33e3729

Please sign in to comment.