Skip to content

Commit

Permalink
finally figuring out how to make swaps/aliases work, this is so messy…
Browse files Browse the repository at this point in the history 
… and gross
  • Loading branch information
@mbellotti
mbellotti committed Apr 14, 2023
1 parent b458874 commit a286761
Show file tree
Hide file tree
Showing 12 changed files with 156 additions and 96 deletions.
1 change: 1 addition & 0 deletions ast/ast.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -338,6 +338,7 @@ type InvariantClause struct {
Left Expression
Operator string
Right Expression
SyncedState bool
InferredType *Type
}

Expand Down
69 changes: 53 additions & 16 deletions listener/listener.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -14,6 +14,7 @@ import (
"strings"

"github.com/antlr/antlr4/runtime/Go/antlr/v4"
"github.com/barkimedes/go-deepcopy"
)

type FaultListener struct {
Expand All @@ -30,6 +31,8 @@ type FaultListener struct {
Uncertains map[string][]float64
Unknowns []string
StructsPropertyOrder map[string][]string
instances map[string]*ast.Instance
swaps map[string][]ast.Node
}

func NewListener(path string, testing bool, skipRun bool) *FaultListener {
Expand All @@ -39,6 +42,8 @@ func NewListener(path string, testing bool, skipRun bool) *FaultListener {
skipRun: skipRun,
Uncertains: make(map[string][]float64),
StructsPropertyOrder: make(map[string][]string),
instances: make(map[string]*ast.Instance),
swaps: make(map[string][]ast.Node),
}
}

Expand Down Expand Up @@ -104,6 +109,7 @@ func (l *FaultListener) ExitSpec(c *parser.SpecContext) {
for _, v := range l.stack {
spec.Statements = append(spec.Statements, v.(ast.Statement))
}
l.addSwaps()
l.AST = spec
}

Expand Down Expand Up @@ -657,26 +663,27 @@ func (l *FaultListener) ExitParamCall(c *parser.ParamCallContext) {
}

func (l *FaultListener) ExitInitBlock(c *parser.InitBlockContext) {
var swaps, orphanSwaps []ast.Node
//var swaps, orphanSwaps []ast.Node
var swaps []ast.Node
token := util.GenerateToken("FUNCTION", "FUNCTION", c.GetStart(), c.GetStop())

sl := &ast.BlockStatement{
Token: token,
}
orphanSwaps = l.getSwaps()
swaps = l.getSwaps()

steps := c.AllInitStep()
for i := len(steps) - 1; i >= 0; i-- {
ex := l.pop()

if sw, ok := ex.(*ast.InfixExpression); ok && sw.TokenLiteral() == "SWAP" {
i++
orphanSwaps = append(orphanSwaps, sw)
swaps = append(swaps, sw)
continue
}

if t, ok := ex.(*ast.Instance); ok {
swaps, orphanSwaps = l.filterSwaps(t.Name, orphanSwaps)
//swaps, orphanSwaps = l.filterSwaps(t.Name, orphanSwaps)
t.Swaps = append(t.Swaps, swaps...)

token2 := ex.GetToken()
Expand Down Expand Up @@ -762,14 +769,15 @@ func (l *FaultListener) ExitStateBlock(c *parser.StateBlockContext) {
}

func (l *FaultListener) ExitRunInit(c *parser.RunInitContext) {
var swaps, orphanSwaps []ast.Node
//var swaps, orphanSwaps []ast.Node
var swaps []ast.Node
txt := c.AllIDENT()
var right string

token2 := util.GenerateToken("IDENT", "IDENT", c.GetStart(), c.GetStop())

// Check for swaps
orphanSwaps = l.getSwaps()
swaps = l.getSwaps()

ident := &ast.Identifier{Token: token2}
switch len(txt) {
Expand Down Expand Up @@ -799,16 +807,18 @@ func (l *FaultListener) ExitRunInit(c *parser.RunInitContext) {
key := strings.Join([]string{ident.Spec, ident.Value}, "_")
order := l.StructsPropertyOrder[key]

swaps, orphanSwaps = l.filterSwaps(right, orphanSwaps)
//swaps, orphanSwaps = l.filterSwaps(right, orphanSwaps)
inst := &ast.Instance{
Value: ident,
Name: right,
Order: order,
}

l.pushN(orphanSwaps)
l.push(
&ast.Instance{
Value: ident,
Name: right,
Order: order,
Swaps: swaps,
})
l.instances[right] = inst
l.sortSwaps(swaps)

//l.pushN(orphanSwaps)
l.push(inst)
}

func (l *FaultListener) ExitRunSwap(c *parser.SwapContext) {
Expand Down Expand Up @@ -1590,6 +1600,7 @@ func (l *FaultListener) ExitSysSpec(c *parser.SysSpecContext) {
for _, v := range l.stack {
spec.Statements = append(spec.Statements, v.(ast.Statement))
}
l.addSwaps()
l.AST = spec
}

Expand Down Expand Up @@ -1681,7 +1692,9 @@ func (l *FaultListener) ExitGlobalDecl(c *parser.GlobalDeclContext) {
key := strings.Join([]string{importSpec, importStruct}, "_")
order := l.StructsPropertyOrder[key]
parent.Order = order
parent.Swaps = swaps

l.instances[parent.Name] = parent
l.sortSwaps(swaps)
}

l.push(&ast.DefStatement{
Expand Down Expand Up @@ -1875,6 +1888,30 @@ func (l *FaultListener) packageCallsAsRunSteps(node ast.Node) ast.Node {
}
}

func (l *FaultListener) sortSwaps(swaps []ast.Node) {
for _, s := range swaps {
if node, ok := s.(*ast.InfixExpression).Left.(*ast.ParameterCall); ok {
if _, ok2 := l.swaps[node.Value[0]]; !ok2 {
l.swaps[node.Value[0]] = []ast.Node{}
}
l.swaps[node.Value[0]] = append(l.swaps[node.Value[0]], s)
}
}
}

func (l *FaultListener) addSwaps() {
for key, inst := range l.instances {
if sw, ok := l.swaps[key]; ok {
c, err := deepcopy.Anything(sw)
if err != nil {
panic(err)
}
inst.Swaps = c.([]ast.Node)
l.swaps[key] = []ast.Node{}
}
}
}

func (l *FaultListener) builtInType(b *ast.BuiltIn) string {
return b.Function
}
1 change: 1 addition & 0 deletions llvm/alloc.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@ func (c *Compiler) updateVariableStateName(id []string) string {

func (c *Compiler) allocVariable(id []string, val value.Value, pos []int) {
name := strings.Join(id, "_")

var alloc *ir.InstAlloca
var store *ir.InstStore

Expand Down
79 changes: 48 additions & 31 deletions llvm/compiler.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -75,6 +75,7 @@ type Compiler struct {
Unknowns []string
Components map[string]*StateFunc
ComponentOrder []string
Alias map[string]string
}

func NewCompiler() *Compiler {
Expand Down Expand Up @@ -104,21 +105,22 @@ func NewCompiler() *Compiler {
return c
}

func Execute(tree *ast.Spec, specRec map[string]*preprocess.SpecRecord, uncertains map[string][]float64, unknowns []string, testing bool) *Compiler {
func Execute(tree *ast.Spec, specRec map[string]*preprocess.SpecRecord, uncertains map[string][]float64, unknowns []string, aliases map[string]string, testing bool) *Compiler {
compiler := NewCompiler()
compiler.LoadMeta(specRec, uncertains, unknowns, testing)
compiler.LoadMeta(specRec, uncertains, unknowns, aliases, testing)
err := compiler.Compile(tree)
if err != nil {
panic(err)
}
return compiler
}

func (c *Compiler) LoadMeta(structs map[string]*preprocess.SpecRecord, uncertains map[string][]float64, unknowns []string, test bool) {
func (c *Compiler) LoadMeta(structs map[string]*preprocess.SpecRecord, uncertains map[string][]float64, unknowns []string, aliases map[string]string, test bool) {
c.specStructs = structs
c.Unknowns = unknowns
c.Uncertains = uncertains
c.isTesting = test
c.Alias = aliases
}

func (c *Compiler) Compile(root ast.Node) (err error) {
Expand Down Expand Up @@ -326,7 +328,7 @@ func (c *Compiler) compileStruct(def *ast.DefStatement) {
c.compileInstance(instance)
c.contextFuncName = context

rawid := instance.RawId()
rawid := c.AliasToBaseRaw(instance.RawId())
s := c.specStructs[rawid[0]]
ty, _ := s.GetStructType(rawid)
n := strings.Join(rawid[1:], "_")
Expand Down Expand Up @@ -510,7 +512,7 @@ func (c *Compiler) compileComponent(node *ast.ComponentLiteral) {

func (c *Compiler) compileParameterCall(pc *ast.ParameterCall) value.Value {
var err error
id := pc.RawId()
id := c.AliasToBaseRaw(pc.RawId())
spec := c.specStructs[id[0]]
ty, _ := spec.GetStructType(id[0:2]) //Removing the key
st := id[len(id)-2] //The struct is the second to last item
Expand Down Expand Up @@ -710,9 +712,9 @@ func (c *Compiler) compileInfix(node *ast.InfixExpression) value.Value {
if _, ok := node.Right.(*ast.Instance); !ok { // If declaring a new instance don't save
switch n := node.Left.(type) {
case *ast.Identifier:
id = n.RawId()
id = c.AliasToBaseRaw(n.RawId())
case *ast.ParameterCall:
id = n.RawId()
id = c.AliasToBaseRaw(n.RawId())
}

s = c.specs[id[0]]
Expand Down Expand Up @@ -747,7 +749,7 @@ func (c *Compiler) compileInfix(node *ast.InfixExpression) value.Value {
}

pos := n.Position()
id = n.RawId()
id = c.AliasToBaseRaw(n.RawId())

s = c.specs[id[0]]

Expand Down Expand Up @@ -911,7 +913,7 @@ func (c *Compiler) compileInfix(node *ast.InfixExpression) value.Value {
func (c *Compiler) compileInfixNode(node ast.Node) value.Value {
switch v := node.(type) {
case *ast.ParameterCall:
id := v.Id()
id := c.AliasToBaseRaw(v.Id())
return c.lookupIdent(id, node.Position())
case *ast.This:
id := v.Id()
Expand Down Expand Up @@ -1130,7 +1132,7 @@ func (c *Compiler) convertAssertVariables(ex ast.Expression) ast.Expression {
e.Right = c.convertAssertVariables(e.Right)
return e
case *ast.Identifier:
id := e.RawId()
id := c.AliasToBaseRaw(e.RawId())
pos := e.Position()
vname := strings.Join(id, "_")

Expand All @@ -1148,7 +1150,7 @@ func (c *Compiler) convertAssertVariables(ex ast.Expression) ast.Expression {
Instances: instas,
}
case *ast.ParameterCall:
id := e.RawId()
id := c.AliasToBaseRaw(e.RawId())
pos := e.Position()
vname := strings.Join(id, "_")

Expand Down Expand Up @@ -1281,26 +1283,18 @@ func (c *Compiler) processStruct(node *ast.StructInstance) map[string]string {
id = pv.Id()
funcs = append(funcs, id)
default:
if n, ok := pv.(*ast.Unknown); ok {
if c.IsAlias(pv.(ast.Nameable).IdString()) {
continue
}

if _, ok := pv.(*ast.Unknown); ok {
isUnknown = true
id = n.Id()
} else if uncertain, ok2 := pv.(*ast.Uncertain); ok2 {
isUncertain = []float64{uncertain.Mean, uncertain.Sigma}
id = uncertain.Id()
} else if n, ok := pv.(*ast.IntegerLiteral); ok {
id = n.Id()
} else if n, ok := pv.(*ast.FloatLiteral); ok {
id = n.Id()
} else if n, ok := pv.(*ast.Boolean); ok {
id = n.Id()
} else if n, ok := pv.(*ast.StringLiteral); ok {
id = n.Id()
} else if n, ok := pv.(*ast.Identifier); ok {
id = n.Id()
} else if n, ok := pv.(*ast.ParameterCall); ok {
id = n.Id()
}

id = pv.(ast.Nameable).Id()

val := c.compileValue(pv)
s = c.specs[id[0]]
s.DefineSpecVar(id, val)
Expand Down Expand Up @@ -1365,7 +1359,7 @@ func (c *Compiler) generateParameters(id []string, data map[string]ast.Node, com
p = append(p, ip...)
case *ast.StructProperty:
if _, ok := n.Value.(*ast.FunctionLiteral); !ok {
rawid := n.Value.(ast.Nameable).RawId()
rawid := c.AliasToBaseRaw(n.Value.(ast.Nameable).RawId())
s = c.specs[rawid[0]]
vname := strings.Join(rawid, "_")
ty := s.GetPointerType(vname)
Expand All @@ -1378,19 +1372,19 @@ func (c *Compiler) generateParameters(id []string, data map[string]ast.Node, com
p = append(p, ir.NewParam(vname, I1P))
}
case *ast.IntegerLiteral:
rawid := n.RawId()
rawid := c.AliasToBaseRaw(n.RawId())
vname := strings.Join(rawid, "_")
p = append(p, ir.NewParam(vname, DoubleP))
case *ast.FloatLiteral:
rawid := n.RawId()
rawid := c.AliasToBaseRaw(n.RawId())
vname := strings.Join(rawid, "_")
p = append(p, ir.NewParam(vname, DoubleP))
case *ast.Boolean:
rawid := n.RawId()
rawid := c.AliasToBaseRaw(n.RawId())
vname := strings.Join(rawid, "_")
p = append(p, ir.NewParam(vname, I1P))
default:
rawid := n.(ast.Nameable).RawId()
rawid := c.AliasToBaseRaw(n.(ast.Nameable).RawId())
s = c.specs[rawid[0]]
vname := strings.Join(rawid, "_")
ty := s.GetPointerType(vname)
Expand Down Expand Up @@ -1451,6 +1445,29 @@ func (c *Compiler) isConstant(rawid []string) bool {
return err == nil
}

func (c *Compiler) IsAlias(alias string) bool {
if _, ok := c.Alias[alias]; ok {
return true
}
return false
}

func (c *Compiler) AliasToBase(alias string) string {
if b, ok := c.Alias[alias]; ok {
return c.AliasToBase(b)
}
return alias
}

func (c *Compiler) AliasToBaseRaw(rawid []string) []string {
alias := strings.Join(rawid, "_")
if b, ok := c.Alias[alias]; ok {
r := strings.Split(b, "_")
return c.AliasToBaseRaw(r)
}
return rawid
}

func (c *Compiler) isVarSet(rawid []string) bool {
var err error
s := c.specStructs[rawid[0]]
Expand Down
4 changes: 2 additions & 2 deletions llvm/llvm_test.go
View file
Original file line number Diff line number Diff line change
Expand Up @@ -340,7 +340,7 @@ func TestUnknowns(t *testing.T) {
func TestParamReset(t *testing.T) {
structs := make(map[string]*preprocess.SpecRecord)
c := NewCompiler()
c.LoadMeta(structs, make(map[string][]float64), []string{}, true)
c.LoadMeta(structs, make(map[string][]float64), []string{}, make(map[string]string), true)
s := NewCompiledSpec("test")
c.currentSpec = "test"
c.specs["test"] = s
Expand Down Expand Up @@ -733,7 +733,7 @@ func prepTest(test string, specType bool) (string, error) {
sw := swaps.NewPrecompiler(ty)
tree := sw.Swap(ty.Checked)
compiler := NewCompiler()
compiler.LoadMeta(ty.SpecStructs, l.Uncertains, l.Unknowns, true)
compiler.LoadMeta(ty.SpecStructs, l.Uncertains, l.Unknowns, sw.Alias, true)
err := compiler.Compile(tree)
if err != nil {
return "", err
Expand Down

0 comments on commit a286761

Please sign in to comment.