Skip to content

Commit

Permalink
Bellmar/doc example bugs (#25)
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

* wrapping errors in more specific messages to mitigate the exit status 1 vagueness

* x -> stock should not be allowed
  • Loading branch information
mbellotti committed Feb 27, 2023
1 parent f13fec5 commit 80d9556
Show file tree
Hide file tree
Showing 4 changed files with 33 additions and 71 deletions.
74 changes: 16 additions & 58 deletions listener/listener.go
Original file line number Diff line number Diff line change
Expand Up @@ -477,77 +477,35 @@ func (l *FaultListener) ExitFaultAssign(c *parser.FaultAssignContext) {
operator := c.GetChild(1).(antlr.TerminalNode).GetText()
token := util.GenerateToken("ASSIGN", operator, c.GetStart(), c.GetStop())

var receiver ast.Expression
var sender ast.Expression
var valChange ast.Expression

right := l.pop()
left := l.pop()
if operator == "->" {
switch right.(type) {
case *ast.ParameterCall: // This is an in flow a -> param
receiver = right.(ast.Expression)
default: // This is an outflow para -> a
token2 := util.GenerateToken("MINUS", "-", c.GetStart(), c.GetStop())

sender = &ast.InfixExpression{
Token: token2,
Left: left.(ast.Expression),
Operator: "-",
Right: right.(ast.Expression)}
}
if receiver == nil {
receiver = left.(ast.Expression)
} else {
token2 := util.GenerateToken("MINUS", "-", c.GetStart(), c.GetStop())

sender = &ast.InfixExpression{
Token: token2,
Left: right.(ast.Expression),
Operator: "-",
Right: left.(ast.Expression)}
}

if sender == nil {
panic(fmt.Sprintf("malformed flow assignment: line %d col %d type left %T type right %T", c.GetStart().GetLine(), c.GetStart().GetColumn(), left, right))
}
token2 := util.GenerateToken("MINUS", "-", c.GetStart(), c.GetStop())
valChange = &ast.InfixExpression{
Token: token2,
Left: left.(ast.Expression),
Operator: "-",
Right: right.(ast.Expression)}
} else if operator == "<-" {
switch right.(type) {
case *ast.ParameterCall: // a <- param
receiver = right.(ast.Expression)
default: // para <- a
token2 := util.GenerateToken("ADD", "+", c.GetStart(), c.GetStop())

sender = &ast.InfixExpression{
Token: token2,
Left: left.(ast.Expression),
Operator: "+",
Right: right.(ast.Expression)}
}
if receiver == nil {
receiver = left.(ast.Expression)
} else {
token2 := util.GenerateToken("ADD", "+", c.GetStart(), c.GetStop())
token2 := util.GenerateToken("ADD", "+", c.GetStart(), c.GetStop())

sender = &ast.InfixExpression{
Token: token2,
Left: right.(ast.Expression),
Operator: "+",
Right: left.(ast.Expression)}
}

if sender == nil {
panic(fmt.Sprintf("malformed flow assignment: line %d col %d type left %T type right %T", c.GetStart().GetLine(), c.GetStart().GetColumn(), left, right))
}
valChange = &ast.InfixExpression{
Token: token2,
Left: left.(ast.Expression),
Operator: "+",
Right: right.(ast.Expression)}
} else {
panic(fmt.Sprintf("Invalid operator %s in expression", operator))
}

l.push(
&ast.InfixExpression{
Token: token,
Left: receiver,
Operator: "<-", // "->" converted automatically by swapping order
Right: sender,
Left: left.(ast.Expression),
Operator: "<-",
Right: valChange,
})

}
Expand Down
14 changes: 7 additions & 7 deletions llvm/llvm_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -70,13 +70,13 @@ func TestRunBlock(t *testing.T) {
def foo = flow{
buzz: new bar,
fizz: func{
a + buzz.a -> buzz.b;
buzz.b <- a + buzz.a;
},
fizz2: func{
buzz.a - b -> buzz.b;
buzz.b <- buzz.a - b;
},
fizz3: func{
buzz.b + b -> buzz.a;
buzz.a <- buzz.b + b;
},
};
Expand Down Expand Up @@ -132,7 +132,7 @@ func TestRunBlock(t *testing.T) {
%1 = load double, double* @test1_a
%2 = load double, double* %test1_test_buzz_a
%3 = fadd double %1, %2
%4 = fsub double %0, %3
%4 = fadd double %0, %3
store double %4, double* %test1_test_buzz_b
ret void
}
Expand All @@ -143,7 +143,7 @@ func TestRunBlock(t *testing.T) {
%1 = load double, double* %test1_test_buzz_a
%2 = load double, double* @test1_b
%3 = fsub double %1, %2
%4 = fsub double %0, %3
%4 = fadd double %0, %3
store double %4, double* %test1_test_buzz_b
ret void
}
Expand All @@ -154,7 +154,7 @@ func TestRunBlock(t *testing.T) {
%1 = load double, double* %test1_test_buzz_b
%2 = load double, double* @test1_b
%3 = fadd double %1, %2
%4 = fsub double %0, %3
%4 = fadd double %0, %3
store double %4, double* %test1_test_buzz_a
ret void
}
Expand Down Expand Up @@ -778,7 +778,7 @@ func prepTestSys(test string) (string, error) {
if err != nil {
return "", err
}
fmt.Println(compiler.GetIR())
//fmt.Println(compiler.GetIR())
return compiler.GetIR(), err
}

Expand Down
8 changes: 4 additions & 4 deletions main.go
Original file line number Diff line number Diff line change
Expand Up @@ -56,7 +56,7 @@ func parse(data string, path string, file string, filetype string, reach bool, v
ty := types.NewTypeChecker(pre.Specs)
_, err := ty.Check(tree)
if err != nil {
log.Fatal(err)
log.Fatalf("typechecker failed: %s", err)
}

var visual string
Expand All @@ -78,7 +78,7 @@ func ll(lstnr *listener.FaultListener, ty *types.Checker) *llvm.Compiler {
compiler.LoadMeta(ty.SpecStructs, lstnr.Uncertains, lstnr.Unknowns)
err := compiler.Compile(lstnr.AST)
if err != nil {
log.Fatal(err)
log.Fatalf("LLVM IR generation failed: %s", err)
}
return compiler
}
Expand All @@ -95,15 +95,15 @@ func probability(smt string, uncertains map[string][]float64, unknowns []string,
ex.LoadModel(smt, uncertains, unknowns, results)
ok, err := ex.Check()
if err != nil {
log.Fatal(err)
log.Fatalf("model checker has failed: %s", err)
}
if !ok {
fmt.Println("Fault could not find a failure case.")
return ex, nil
}
scenario, err := ex.Solve()
if err != nil {
log.Fatal(err)
log.Fatalf("error found fetching solution from solver: %s", err)
}
data := ex.Filter(scenario)
return ex, data
Expand Down
8 changes: 6 additions & 2 deletions types/types_test.go
Original file line number Diff line number Diff line change
Expand Up @@ -97,6 +97,10 @@ func TestStructTypeError(t *testing.T) {

actual := "stock is the store of values, stock test1_fizz should be a flow"

if err == nil {
t.Fatalf("Type checking failed to catch invalid expression. Error is nil")
}

if err.Error() != actual {
t.Fatalf("Type checking failed to catch invalid expression. got=%s", err)
}
Expand Down Expand Up @@ -129,8 +133,8 @@ func TestInstanceError(t *testing.T) {
func TestComplex(t *testing.T) {
test := `spec test1;
def test = stock{
x: func{(2.1*8)+2.3/(5-2);}
}
x: func{(2.1*8)+2.3/(5-2);},
};
`
checker, err := prepTest(test)

Expand Down

0 comments on commit 80d9556

Please sign in to comment.