Skip to content

Commit

Permalink
breaking swaps out into their own thing.
Browse files Browse the repository at this point in the history
  • Loading branch information
mbellotti committed Mar 24, 2023
1 parent 6ad8c0a commit 10cfdf6
Show file tree
Hide file tree
Showing 9 changed files with 285 additions and 31 deletions.
9 changes: 9 additions & 0 deletions llvm/llvm_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ import (
"fault/listener"
"fault/parser"
"fault/preprocess"
"fault/swaps"
"fault/types"
"fmt"
"io"
Expand Down Expand Up @@ -744,6 +745,10 @@ func prepTest(test string) (string, error) {
if err != nil {
return "", err
}

sw := swaps.NewPrecompiler(ty)
tree = sw.Swap(tree)

compiler := NewCompiler()
compiler.LoadMeta(pre.Specs, l.Uncertains, l.Unknowns, true)
err = compiler.Compile(tree)
Expand Down Expand Up @@ -772,6 +777,10 @@ func prepTestSys(test string) (string, error) {
if err != nil {
return "", err
}

sw := swaps.NewPrecompiler(ty)
tree = sw.Swap(tree)

compiler := NewCompiler()
compiler.LoadMeta(pre.Specs, l.Uncertains, l.Unknowns, true)
err = compiler.Compile(tree)
Expand Down
4 changes: 4 additions & 0 deletions main.go
Original file line number Diff line number Diff line change
Expand Up @@ -10,6 +10,7 @@ import (
"fault/reachability"
"fault/smt"
smtvar "fault/smt/variables"
"fault/swaps"
"fault/types"
"fault/util"
"fault/visualize"
Expand Down Expand Up @@ -64,6 +65,9 @@ func parse(data string, path string, file string, filetype string, reach bool, v
log.Fatalf("typechecker failed: %s", err)
}

sw := swaps.NewPrecompiler(ty)
tree = sw.Swap(tree)

var visual string
if visu {
vis := visualize.NewVisual(tree)
Expand Down
5 changes: 5 additions & 0 deletions reachability/reachability_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -4,6 +4,7 @@ import (
"fault/listener"
"fault/parser"
"fault/preprocess"
"fault/swaps"
"fault/types"
"testing"

Expand Down Expand Up @@ -237,6 +238,10 @@ func prepTestSys(test string) (bool, []string) {
if err != nil {
panic(err)
}

sw := swaps.NewPrecompiler(ty)
tree = sw.Swap(tree)

tracer := NewTracer()
tracer.walk(tree)
return tracer.check()
Expand Down
13 changes: 11 additions & 2 deletions smt/generator_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -5,6 +5,7 @@ import (
"fault/llvm"
"fault/parser"
"fault/preprocess"
"fault/swaps"
"fault/types"
"fault/util"
"fmt"
Expand Down Expand Up @@ -471,15 +472,15 @@ func TestTestData(t *testing.T) {
"testdata/bathtub2.fspec",
"testdata/booleans.fspec",
"testdata/unknowns.fspec",
"testdata/swaps.fspec",
"testdata/swaps/swaps.fspec",
}
smt2s := []string{
"testdata/bathtub.smt2",
"testdata/simple.smt2",
"testdata/bathtub2.smt2",
"testdata/booleans.smt2",
"testdata/unknowns.smt2",
"testdata/swaps.smt2",
"testdata/swaps/swaps.smt2",
}
for i, s := range specs {
data, err := os.ReadFile(s)
Expand Down Expand Up @@ -642,6 +643,10 @@ func prepTest(path string, test string) (string, error) {
if err != nil {
return "", err
}

sw := swaps.NewPrecompiler(ty)
tree = sw.Swap(tree)

compiler := llvm.NewCompiler()
compiler.LoadMeta(ty.SpecStructs, l.Uncertains, l.Unknowns, true)
err = compiler.Compile(tree)
Expand Down Expand Up @@ -678,6 +683,10 @@ func prepTestSys(filepath string, test string, imports bool) (string, error) {
if err != nil {
return "", err
}

sw := swaps.NewPrecompiler(ty)
tree = sw.Swap(tree)

compiler := llvm.NewCompiler()
compiler.LoadMeta(ty.SpecStructs, l.Uncertains, l.Unknowns, true)
err = compiler.Compile(tree)
Expand Down
20 changes: 20 additions & 0 deletions smt/testdata/swaps/swaps1.fspec
Original file line number Diff line number Diff line change
@@ -0,0 +1,20 @@
spec swaps;

def s1 = stock{
v: 10,
};

def f1 = flow{
target: new s1,
fn: func{
target.v <- 2;
},
};

for 2 run {
f2 = new f1;
s2 = new s1;
f2.target = s2;
s2.v = 20;
f2.fn;
}
8 changes: 8 additions & 0 deletions smt/testdata/swaps/swaps1.smt2
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
(set-logic QF_NRA)(declare-fun swaps_s2_v_0 () Real)
(declare-fun swaps_f2_target_v_0 () Real)
(declare-fun swaps_f2_target_v_1 () Real)
(declare-fun swaps_f2_target_v_2 () Real)
(assert (= swaps_s2_v_0 20.0))
(assert (= swaps_f2_target_v_0 20.0))
(assert (= swaps_f2_target_v_1 (+ swaps_f2_target_v_0 2.0)))
(assert (= swaps_f2_target_v_2 (+ swaps_f2_target_v_1 2.0)))
191 changes: 191 additions & 0 deletions swaps/swaps.go
Original file line number Diff line number Diff line change
@@ -0,0 +1,191 @@
package swaps

import (
"fault/ast"
"fault/types"
"fault/util"
"fmt"

"github.com/barkimedes/go-deepcopy"
)

type Precompiler struct {
checker *types.Checker
}

func NewPrecompiler(check *types.Checker) *Precompiler {
return &Precompiler{
checker: check,
}
}

func (c *Precompiler) Swap(n *ast.Spec) *ast.Spec {
s := c.walk(n)
return s.(*ast.Spec)
}

func (c *Precompiler) walk(n ast.Node) ast.Node {
var err error
switch node := n.(type) {
case *ast.StructInstance:
node, err = c.swapValues(node)
if err != nil {
panic(err)
}
return node
case *ast.Spec:
var st []ast.Statement
for _, v := range node.Statements {
snode := c.walk(v)
st = append(st, snode.(ast.Statement))
}
node.Statements = st
return node
case *ast.SpecDeclStatement:
return node
case *ast.SysDeclStatement:
return node
case *ast.ImportStatement:
snode := c.walk(node.Tree)
node.Tree = snode.(*ast.Spec)
return node
case *ast.ConstantStatement:
return node
case *ast.Identifier:
return node
case *ast.DefStatement:
return node
case *ast.StockLiteral:
return node
case *ast.FlowLiteral:
return node
case *ast.ComponentLiteral:
return node
case *ast.AssertionStatement:
return node
case *ast.ForStatement:
var st []ast.Statement
for _, v := range node.Body.Statements {
snode := c.walk(v)
st = append(st, snode.(ast.Statement))
}
node.Body.Statements = st
return node
case *ast.StartStatement:
return node
case *ast.FunctionLiteral:
return node
case *ast.BlockStatement:
if node == nil {
return node
}
for i := 0; i < len(node.Statements); i++ {
if e, ok := node.Statements[i].(*ast.ExpressionStatement); ok {
snode := c.walk(e.Expression)
node.Statements[i].(*ast.ExpressionStatement).Expression = snode.(ast.Expression)
}
}
return node
case *ast.BuiltIn:
return node
case *ast.IntegerLiteral:
return node
case *ast.FloatLiteral:
return node
case *ast.Boolean:
return node
case *ast.StringLiteral:
return node
case *ast.ParameterCall:
return node
case *ast.ExpressionStatement:
snode := c.walk(node.Expression)
node.Expression = snode.(ast.Expression)
return node
case *ast.Natural:
return node
case *ast.Uncertain:
return node
case *ast.Unknown:
return node
case *ast.PrefixExpression:
return node
case *ast.InfixExpression:
return node
case *ast.This:
return node
case *ast.Clock:
return node
case *ast.Nil:
return node
case *ast.ParallelFunctions:
return node
case *ast.InitExpression:
return node
case *ast.IfExpression:
if node == nil {
return node
}
//Not sure to allow this
con := c.walk(node.Consequence)
alt := c.walk(node.Alternative)
elif := c.walk(node.Elif)
node.Consequence = con.(*ast.BlockStatement)
node.Alternative = alt.(*ast.BlockStatement)
node.Elif = elif.(*ast.IfExpression)
return node
case *ast.IndexExpression:
return node
case *ast.InvariantClause:
return node
default:
panic(fmt.Errorf("unimplemented: %s type %T", node, node))
}
}

func (c *Precompiler) swapValues(base *ast.StructInstance) (*ast.StructInstance, error) {
for _, s := range base.Swaps {
infix := s.(*ast.InfixExpression)
rawid := infix.Left.(ast.Nameable).RawId()
key := rawid[len(rawid)-1]
val, err := c.checker.Reference(infix.Right)
if err != nil {
return base, err
}

// Because part of what we're doing here is renaming
// these nodes. We need to do a deep copy to separate
// the swapped nodes from their original reference values
copyVal, err := deepcopy.Anything(val)
if err != nil {
return base, err
}

val = copyVal.(ast.Node)

switch v := val.(type) {
case *ast.StructInstance:
v.Name = key
val = v
}

base.Properties[key].Value = val
base = c.swapDeepNames(base)

}
return base, nil
}

func (c *Precompiler) swapDeepNames(val *ast.StructInstance) *ast.StructInstance {
rawid := val.RawId()
err := c.checker.SpecStructs[rawid[0]].Update(rawid, util.ExtractBranches(val.Properties))
if err != nil {
panic(fmt.Sprintf("failed to update spec record on swap %s: %s", val.String(), err))
}

node, err := c.checker.Preprocesser.Partial(rawid[0], val)
if err != nil {
panic(fmt.Sprintf("failed to update process ids on swap %s: %s", val.String(), err))
}
return node.(*ast.StructInstance)
}

0 comments on commit 10cfdf6

Please sign in to comment.