diff --git a/.gitignore b/.gitignore new file mode 100644 index 0000000..2b2f4d3 --- /dev/null +++ b/.gitignore @@ -0,0 +1,23 @@ +.vscode +*.exe +*.out +*.wca +*.csv +*.out.json +*.out.govar +*.swp + +*.xml +main/main + +easy-rte-c +easy-rte-parser + +#ignore built examples +example_* + +#ignore stuff in the example dirs unless it ends in *.erte or *main.c or md +example/*/* +!*.erv +!*main.c +!*.md diff --git a/LICENSE b/LICENSE new file mode 100644 index 0000000..9fed467 --- /dev/null +++ b/LICENSE @@ -0,0 +1,21 @@ +MIT License + +Copyright (c) 2017 Hammond Pearce (kiwih) + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff --git a/Makefile b/Makefile new file mode 100644 index 0000000..7015589 --- /dev/null +++ b/Makefile @@ -0,0 +1,84 @@ +.PHONY: default c_mon verilog_mon $(PROJECT) c_build +.PRECIOUS: %.xml + +# run this makefile with the following options +# make [c_mon] [c_build] [run_(c/e)bmc] PROJECT=XXXXX FILE=YYYYY +# PROJECT = name of project directory +# FILE = name of file within project directory (default = PROJECT, e.g. example/ab5/ab5.whatever) +# +# c_mon: make a C monitor for the project +# c_build: compile the C monitor with a main file (this will need to be provided manually) +# run_cbmc: check the compiled C monitor to ensure correctness +# +# make [verilog_mon] [run_ebmc] PROJECT=XXXXX +# verilog_mon: make a Verilog monitor for the project +# run_ebmc: check the compiled Verilog monitor to ensure correctness + +FILE ?= $(PROJECT) +PARSEARGS ?= + +default: easy-rv-c easy-rv-parser + +#convert C build instruction to C target +c_mon: $(PROJECT) + +#convert verilog build instruction to verilog target +verilog_mon: $(PROJECT)_V + +easy-rv-c: rvc/* rvdef/* + go get github.com/PRETgroup/stcompilerlib + go build -o easy-rv-c -i ./rvc/main + +easy-rv-parser: rvparser/* rvdef/* + go get github.com/PRETgroup/stcompilerlib + go build -o easy-rv-parser -i ./rvparser/main + +run_cbmc: default + cbmc example/$(PROJECT)/cbmc_main_$(PROJECT).c example/$(PROJECT)/F_$(PROJECT).c + +run_ebmc: default + #$(foreach file,$(wildcard example/$(PROJECT)/*.sv), time --format="took %E" ebmc $(file) --k-induction --trace --top F_combinatorialVerilog_$(word 3,$(subst _, ,$(basename $(notdir $(file)))));) + time --format="took %E" ebmc example/$(PROJECT)/test_F_$(FILE).sv --k-induction --trace --module F_combinatorialVerilog_$(FILE) + #ebmc $^ --k-induction --trace + +#convert $(PROJECT) into the C binary name +$(PROJECT): ./example/$(PROJECT)/$(FILE).c + +#generate the C sources from the erv files +%.c: %.xml + ./easy-rv-c -i $^ -o example/$(PROJECT) + +#convert $(PROJECT)_V into the verilog names +$(PROJECT)_V: ./example/$(PROJECT)/$(FILE).sv + +#generate the xml from the erv files +%.xml: %.erv + ./easy-rv-parser $(PARSEARGS) -i $^ -o $@ + +#generate the Verilog sources from the xml files +%.sv: %.xml + ./easy-rv-c -i $^ -o example/$(PROJECT) -l=verilog + +#Bonus: C compilation: convert $(PROJECT) into the C binary name +c_build: example_$(PROJECT) + +#generate the C binary from the C sources +example_$(PROJECT): example/$(PROJECT)/$(PROJECT)_main.c example/$(PROJECT)/F_$(PROJECT).c + gcc example/$(PROJECT)/$(PROJECT)_main.c example/$(PROJECT)/F_$(PROJECT).c -o example_$(PROJECT) + +#Bonus: C assembly +c_asm: example/$(PROJECT)/F_$(PROJECT).c + gcc -S example/$(PROJECT)/F_$(PROJECT).c -o example/$(PROJECT)/F_$(PROJECT).s + +clean: clean_examples + rm -f easy-rv-c + rm -f easy-rv-parser + go get -u github.com/PRETgroup/stcompilerlib + +clean_examples: + rm -f example_* + rm -f ./example/*/F_* + rm -f ./example/*/*.h + rm -f ./example/*/*.v + rm -f ./example/*/*.sv + rm -f ./example/*/*.xml \ No newline at end of file diff --git a/README.md b/README.md new file mode 100644 index 0000000..c694928 --- /dev/null +++ b/README.md @@ -0,0 +1,170 @@ +# easy-rv + +## About +This project provides an easy-to-use implementation of _Runtime Verification_, based on formal semantics. + +This project presents a more generalised any-type monitoring system, which can be used with any C project. +_easy-rv_ was ported from [easy-rte](https://github.com/PRETgroup/easy-rte), which implemented a similar semantics for runtime enforcement. + +## What is Runtime Verification? + +Runtime Verification is a type of Run-time Assurance (RA) which focuses on formal semantics for monitoring the behaviour of systems. +As a system executes, the monitor observes according to formal policies. +In each instant (a.k.a. tick/reaction), the monitor will output one of `{currently true, currently false, true, false}`, to indicate the status of the system. +This project aims to join the growing chorus calling for the use of Runtime Assurance mechanisms for use within the real-world cyber-physical systems domain. Using Runtime Verification, we can monitor the behaviour of _unpredictable_ and _untrustworthy_ processes, ensuring that they any violation of desired policies is detected. + +## How does Runtime Verification work? + +Runtime Verification works by placing a special observer execution module _between_ your plant and your controller. + +``` ++-------+ +------------+ +| | ---inputs---> | | +| Plant | | Controller | +| | <--outputs--- | | ++-------+ +------------+ +``` +becomes +``` + Policies + \/ + +---------+ + | | + | Monitor | + | | + +---------+ + | + | ++-------+ /| +------------+ +| | ---inputs---> | | +| Plant | / | Controller | +| | <--outputs--- | | ++-------+ +------------+ +``` + +In our case, we can compile our policies to either *C* or *Verilog* code. + +The C monitors are designed to be composed with your software in a system such as a microcontroller or an Arduino. + +However, software monitors cannot by their nature monitor the behaviour of the hardware that they run upon. +So, in this case you may want to build your monitor to Verilog, and then compose your microcontroller with custom hardware (such as on an FPGA or ASIC) to ensure system correctness. + +## Build instructions + +Download and install the latest version of [Go](https://golang.org/doc/install). + +Then, download this repository, and run `make` or `make default`, which will generate the tools. + +* The ab5 example can be generated using `make c_mon PROJECT=ab5`. +* You can also generate Verilog monitors by using `make verilog_mon PROJECT=ab5`, for example. The Verilog monitors are a little trickier to use, and require I/O connections to be provided to them. They do not embed a function call to the controller inside. +* If you are interested in using the model checkers: + * Obtain CBMC (C model checker) by running `sudo apt install cbmc`. Website here: https://www.cprover.org/cbmc/ + * Obtain EBMC (Verilog model checker) by going to website https://www.cprover.org/ebmc/ + +## A note on Easy-rv language + +Easy-rv is based on Structured Text (ST) operators and syntax. When making guards, ensure that you adhere to the following operators: + +| Operator | Code | +| -------------- | ----------- | +| Assignment | `:=` | +| Equality | `=` | +| Inequality | `<>` | +| Addition | `+` | +| Subtraction | `-` | +| Multiplication | `*` | +| Division | `/` | +| Not | `!` or NOT | +| And | `&&` or AND | +| Or | `\|\|` or OR | +| Brackets | `(` and `)` | + +## Example of Use (AB5) + +Imagine a function which inputs boolean `A` and outputs boolean `B`. +In _easy-rv_, we present this function with the following _erv_ syntax: +``` +monitor ab5; +interface of ab5 { + bool A; //in this case, A goes from PLANT to CONTROLLER + bool B; //in this case, B goes from CONTROLLER to PLANT +} +``` + +This is equivalent to the following C code, which is autogenerated, so that the function ab5Function_run can be provided by the user: +```c +//IO of the monitor ab5Function +typedef struct { + bool A; +} io_ab5_t; + + +void ab5_run(io_ab5_t io); +``` + +Let's now give our function the following I/O properties: +1. A and B alternate starting with an A. +2. B should be true within 5 ticks after an occurance of A. +3. A and B can only happen simultaneously in the first instant, or after any B. This indicates the end of a run. + +We can present this as the following _easy-rv_ policy format: +``` +policy AB5 of ab5 { + internals { + dtimer_t v; + } + + states { + + //first state is initial, and represents "We're waiting for an A" + s0 accepting { + //if we receive neither A nor B, do nothing + -> s0 on (!A and !B): v := 0; + + //if we receive an A only, head to state s1 + -> s1 on (A and !B): v := 0; + + //if we receive a !A and B then VIOLATION + -> violation on (!A and B); + + //if we receive both A and B then done + -> done on (A and B); + } + + //s1 is "we're waiting for a B, and it needs to get here within 5 ticks" + s1 rejecting { + //if we receive nothing, and we aren't over-time, then we do nothing + -> s1 on (!A and !B and v < 5); + + //if we receive a B only, head to state s0 + -> s0 on (!A and B); + + //if we go overtime, or we receive another A, then VIOLATION + -> violation on ((v >= 5) or (A and B) or (A and !B)); + -> violation on (v >= 5) recover B := 1; + -> violation on (A and B) or (A and !B); + } + + done accepting trap; + + violation rejecting trap; + } +} +``` + +As can be seen, this can be thought of as a simple mealy finite state machine, which provides the rules for correct operation. + +We may now compile this system to executable code. + +With _easy-rv_, this process is completed automatically in two steps. Firstly, we convert the _erv_ file into an equivalent policy XML file (which makes it easier to understand, and allows portability between tools). +* `./easy-rv-parser -i example/ab5 -o example/ab5` + +Then, we convert this policy XML file into executable code, which is written in C. +* `./easy-rv-c -i example/ab5 -o example/ab5` + +Now, we can provide a `main.c` file which has our controller and plant interface code in it, and then compile the project together. + +This entire example is provided in the `/example/ab5` folder of this repository, including an example top level file, and can be built from the root directory using `make c_mon PROJECT=ab5`. + +To compile it together with the example main file, run `make c_mon c_build PROJECT=ab5` + diff --git a/example/ab5/ab5.erv b/example/ab5/ab5.erv new file mode 100644 index 0000000..aaa9479 --- /dev/null +++ b/example/ab5/ab5.erv @@ -0,0 +1,47 @@ +monitor ab5; +interface of ab5 { + bool A; + bool B; +} + +policy AB5 of ab5 { + internals { + dtimer_t v; + } + + states { + + //first state is initial, and represents "We're waiting for an A" + s0 accepting { + //if we receive neither A nor B, do nothing + -> s0 on (!A and !B): v := 0; + + //if we receive an A only, head to state s1 + -> s1 on (A and !B): v := 0; + + //if we receive a !A and B then VIOLATION + -> violation on (!A and B); + + //if we receive both A and B then done + -> done on (A and B); + } + + //s1 is "we're waiting for a B, and it needs to get here within 5 ticks" + s1 rejecting { + //if we receive nothing, and we aren't over-time, then we do nothing + -> s1 on (!A and !B and v < 5); + + //if we receive a B only, head to state s0 + -> s0 on (!A and B); + + //if we go overtime, or we receive another A, then VIOLATION + -> violation on ((v >= 5) or (A and B) or (A and !B)); + -> violation on (v >= 5) recover B := 1; + -> violation on (A and B) or (A and !B); + } + + done accepting trap; + + violation rejecting trap; + } +} diff --git a/example/ab5/ab5_main.c b/example/ab5/ab5_main.c new file mode 100644 index 0000000..fdd3a2d --- /dev/null +++ b/example/ab5/ab5_main.c @@ -0,0 +1,33 @@ +#include "F_ab5.h" +#include +#include + +void print_data(uint32_t count, inputs_ab5_t inputs, outputs_ab5_t outputs) { + printf("Tick %7d: A:%d, B:%d\r\n", count, inputs.A, outputs.B); +} + +int main() { + enforcervars_ab5_t enf; + inputs_ab5_t inputs; + outputs_ab5_t outputs; + + ab5_init_all_vars(&enf, &inputs, &outputs); + + uint32_t count = 0; + while(count++ < 30) { + if(count % 10 == 0) { + inputs.A = true; + } else { + inputs.A = false; + } + + ab5_run_via_enforcer(&enf, &inputs, &outputs); + + print_data(count, inputs, outputs); + } +} + +void ab5_run(inputs_ab5_t *inputs, outputs_ab5_t *outputs) { + //do nothing +} + diff --git a/example/ab5seconds/ab5seconds_main.c b/example/ab5seconds/ab5seconds_main.c new file mode 100644 index 0000000..14bdb36 --- /dev/null +++ b/example/ab5seconds/ab5seconds_main.c @@ -0,0 +1,32 @@ +#include "F_ab5seconds.h" +#include + +void print_data(uint32_t count, inputs_ab5seconds_t inputs, outputs_ab5seconds_t outputs) { + printf("Tick %7d: A:%d, B:%d\r\n", count, inputs.A, outputs.B); +} + +int main() { + enforcervars_ab5seconds_t enf; + inputs_ab5seconds_t inputs; + outputs_ab5seconds_t outputs; + + ab5seconds_init_all_vars(&enf, &inputs, &outputs); + + uint32_t count = 0; + while(count++ < 50) { + if(count % 10 == 0) { + inputs.A = true; + } else { + inputs.A = false; + } + + ab5seconds_run_via_enforcer(&enf, &inputs, &outputs); + + print_data(count, inputs, outputs); + } +} + +void ab5seconds_run(inputs_ab5seconds_t *inputs, outputs_ab5seconds_t *outputs) { + //do nothing +} + diff --git a/example/pacemaker/README.md b/example/pacemaker/README.md new file mode 100644 index 0000000..45e5c84 --- /dev/null +++ b/example/pacemaker/README.md @@ -0,0 +1,29 @@ +# pacemaker examples + +Actual times: + +| timer | ms | +| ----- | ---:| +| AVI | 300 | +| AEI | 800 | +| PVARP | 50 | +| VRP | 150 | +| LRI | 950 | +| URI | 900 | + +//P1: AP and VP cannot happen simultaneously. +//P2: VS or VP must be true within AVI after an atrial event AS or AP. +//P3: AS or AP must be true within AEI after a ventricular event VS or VP. +//P4: After a ventricular event VS or VP, another ventricular event can happen only after URI. +//P5: After a ventricular event VS or VP, another ventricular event should happen within LRI. + +AS/AP --AVI--> VS/VP --AEI--> AS/AP --AVI--> VS/VP + +AEI + AVI is maximum time between VS/VP and VS/VP +LRI is also maximum time between VS/VP and VS/VP + +According to expert, +URI and LRI should be less than AVI+AEI, i.e. +AVI + AEI < URI +AVI + AEI < LRI + diff --git a/rvc/compiler.go b/rvc/compiler.go new file mode 100644 index 0000000..32fe639 --- /dev/null +++ b/rvc/compiler.go @@ -0,0 +1,105 @@ +package rtec + +import ( + "bytes" + "encoding/xml" + "errors" + "fmt" + "strings" + "text/template" + + "github.com/PRETgroup/easy-rte/rtedef" +) + +//Converter is the struct we use to store all functions for conversion (and what we operate from) +type Converter struct { + Funcs []rtedef.EnforcedFunction + Language string + templates *template.Template +} + +//New returns a new instance of a Converter based on the provided language +func New(language string) (*Converter, error) { + switch strings.ToLower(language) { + case "c": + return &Converter{Funcs: make([]rtedef.EnforcedFunction, 0), Language: "c", templates: cTemplates}, nil + case "vhdl": + fmt.Println("WARNING: VHDL compilation support is currently not working due to problems with the VHDL type system. Try Verilog instead.") + return &Converter{Funcs: make([]rtedef.EnforcedFunction, 0), Language: "vhdl", templates: vhdlTemplates}, nil + case "verilog": + return &Converter{Funcs: make([]rtedef.EnforcedFunction, 0), Language: "verilog", templates: verilogTemplates}, nil + default: + return nil, errors.New("Language " + language + " is not supported") + } +} + +//AddFunction should be called for each Function in the project +func (c *Converter) AddFunction(functionbytes []byte) error { + FB := rtedef.EnforcedFunction{} + if err := xml.Unmarshal(functionbytes, &FB); err != nil { + return errors.New("Couldn't unmarshal EnforcedFunction xml: " + err.Error()) + } + + c.Funcs = append(c.Funcs, FB) + + return nil +} + +//OutputFile is used when returning the converted data from the iec61499 +type OutputFile struct { + Name string + Extension string + Contents []byte +} + +//TemplateData is the structure used to hold data being passed into the templating engine +type TemplateData struct { + FunctionIndex int + Functions []rtedef.EnforcedFunction +} + +//ConvertAll converts iec61499 xml (stored as []FB) into vhdl []byte for each block (becomes []VHDLOutput struct) +//Returns nil error on success +func (c *Converter) ConvertAll() ([]OutputFile, error) { + finishedConversions := make([]OutputFile, 0, len(c.Funcs)) + + type templateInfo struct { + Prefix string + Name string + Extension string + } + + var templates []templateInfo + + //convert all functions + if c.Language == "c" { + templates = []templateInfo{ + {"F_", "functionC", "c"}, + {"F_", "functionH", "h"}, + {"cbmc_main_", "mainCBMCC", "c"}, + } + } + if c.Language == "vhdl" { + templates = []templateInfo{ + {"F_", "functionVhdl", "vhdl"}, + } + } + if c.Language == "verilog" { + templates = []templateInfo{ + {"test_F_", "functionVerilog", "sv"}, + } + } + for _, template := range templates { + for i := 0; i < len(c.Funcs); i++ { + + output := &bytes.Buffer{} + if err := c.templates.ExecuteTemplate(output, template.Name, TemplateData{FunctionIndex: i, Functions: c.Funcs}); err != nil { + return nil, errors.New("Couldn't format template (fb) of" + c.Funcs[i].Name + ": " + err.Error()) + } + + finishedConversions = append(finishedConversions, OutputFile{Name: template.Prefix + c.Funcs[i].Name, Extension: template.Extension, Contents: output.Bytes()}) + } + } + + return finishedConversions, nil +} diff --git a/rvc/main/main.go b/rvc/main/main.go new file mode 100644 index 0000000..34581b5 --- /dev/null +++ b/rvc/main/main.go @@ -0,0 +1,108 @@ +package main + +import ( + "flag" + "fmt" + "io/ioutil" + "os" + "strings" + + "github.com/PRETgroup/easy-rte/rtec" +) + +var ( + inFileName = flag.String("i", "", "Specifies the name of the source xml file to be compiled.") + outLocation = flag.String("o", "", "Specifies the name of the directory to put output files. If blank, uses current directory") + language = flag.String("l", "c", "The output language") +) + +func main() { + flag.Parse() + + *outLocation = strings.TrimSuffix(*outLocation, "/") + *outLocation = strings.TrimSuffix(*outLocation, "\\") + + if *inFileName == "" { + fmt.Println("You need to specify a file or directory name to compile! Check out -help for options") + return + + } + + // fileInfo, err := os.Stat(*inFileName) + // if err != nil { + // fmt.Println("Error reading file statistics:", err.Error()) + // return + // } + + conv, err := rtec.New(*language) + if err != nil { + fmt.Println("Error creating converter:", err.Error()) + return + } + + //var xmlFileNames []string + + // if fileInfo.IsDir() { + // fmt.Println("Running in Dir mode") + // files, err := ioutil.ReadDir(*inFileName) + // if err != nil { + // log.Fatal(err) + // } + + // for _, file := range files { + // //only read the .fbt and .res files + // name := file.Name() + // nameComponents := strings.Split(name, ".") + // extension := nameComponents[len(nameComponents)-1] + // if extension == "xml" { + // xmlFileNames = append(xmlFileNames, name) + // } + // } + // } else { + // fmt.Println("Running in Single mode") + // xmlFileNames = append(xmlFileNames, *inFileName) + // } + + // for _, name := range xmlFileNames { + // sourceFile, err := ioutil.ReadFile(fmt.Sprintf("%s%c%s", *inFileName, os.PathSeparator, name)) + // if err != nil { + // fmt.Printf("Error reading file '%s' for conversion: %s\n", name, err.Error()) + // return + // } + + // err = conv.AddFunction(sourceFile) + // if err != nil { + // fmt.Printf("Error during adding file '%s' for conversion: %s\n", name, err.Error()) + // return + // } + // } + + sourceFile, err := ioutil.ReadFile(*inFileName) + if err != nil { + fmt.Printf("Error reading file '%s' for conversion: %s\n", *inFileName, err.Error()) + return + } + + err = conv.AddFunction(sourceFile) + if err != nil { + fmt.Printf("Error during adding file '%s' for conversion: %s\n", *inFileName, err.Error()) + return + } + + outputs, err := conv.ConvertAll() + if err != nil { + fmt.Println("Error during conversion:", err.Error()) + return + } + + for _, output := range outputs { + fmt.Printf("Writing %s.%s\n", output.Name, output.Extension) + + err = ioutil.WriteFile(fmt.Sprintf("%s%c%s.%s", *outLocation, os.PathSeparator, output.Name, output.Extension), output.Contents, 0644) + if err != nil { + fmt.Println("Error during file write:", err.Error()) + return + } + } + +} diff --git a/rvc/rteVerilogTemplate.go b/rvc/rteVerilogTemplate.go new file mode 100644 index 0000000..3a0b400 --- /dev/null +++ b/rvc/rteVerilogTemplate.go @@ -0,0 +1,340 @@ +package rtec + +import ( + "text/template" + + "github.com/PRETgroup/goFB/goFB/stconverter" +) + +const rteVerilogTemplate = `{{define "_policyIn"}}{{$block := .}}{{$pbfPolicies := getAllPolicyEnfInfo $block}} + //input policies + {{range $polI, $pol := $block.Policies}}{{$pfbEnf := index $pbfPolicies $polI}} + {{if not $pfbEnf}}//{{$pol.Name}} is broken! + {{else}}{{/* this is where the policy comes in */}}//INPUT POLICY {{$pol.Name}} BEGIN + case({{$block.Name}}_policy_{{$pol.Name}}_state) + {{range $sti, $st := $pol.States}}` + "`" + `POLICY_STATE_{{$block.Name}}_{{$pol.Name}}_{{$st.Name}}: begin + {{range $tri, $tr := $pfbEnf.InputPolicy.GetViolationTransitions}}{{if eq $tr.Source $st.Name}}{{/* + */}} + if ({{$cond := getVerilogECCTransitionCondition $block (compileExpression $tr.STGuard)}}{{$cond.IfCond}}) begin + //transition {{$tr.Source}} -> {{$tr.Destination}} on {{$tr.Condition}} + //select a transition to solve the problem + {{$solution := $pfbEnf.SolveViolationTransition $tr true}} + {{if $solution.Comment}}//{{$solution.Comment}}{{end}} + {{range $soleI, $sole := $solution.Expressions}}{{$sol := getVerilogECCTransitionCondition $block (compileExpression $sole)}}{{$sol.IfCond}}; + {{end}} + end{{end}}{{end}} + end + {{end}} + endcase + {{end}} + //INPUT POLICY {{$pol.Name}} END + {{end}} +{{end}} + +{{define "_policyOut"}}{{$block := .}}{{$pbfPolicies := getAllPolicyEnfInfo $block}} + //output policies + {{range $polI, $pol := $block.Policies}}{{$pfbEnf := index $pbfPolicies $polI}} + {{if not $pfbEnf}}//{{$pol.Name}} is broken! + {{else}}{{/* this is where the policy comes in */}}//OUTPUT POLICY {{$pol.Name}} BEGIN + + case({{$block.Name}}_policy_{{$pol.Name}}_state) + {{range $sti, $st := $pol.States}}` + "`" + `POLICY_STATE_{{$block.Name}}_{{$pol.Name}}_{{$st.Name}}: begin + {{range $tri, $tr := $pfbEnf.OutputPolicy.GetViolationTransitions}}{{if eq $tr.Source $st.Name}}{{/* + */}} + if ({{$cond := getVerilogECCTransitionCondition $block (compileExpression $tr.STGuard)}}{{$cond.IfCond}}) begin + //transition {{$tr.Source}} -> {{$tr.Destination}} on {{$tr.Condition}} + //select a transition to solve the problem + {{$solution := $pfbEnf.SolveViolationTransition $tr false}} + {{if $solution.Comment}}//{{$solution.Comment}}{{end}} + {{range $soleI, $sole := $solution.Expressions}}{{$sol := getVerilogECCTransitionCondition $block (compileExpression $sole)}}{{$sol.IfCond}}; + {{end}} + end {{end}}{{end}} + end + {{end}} + endcase + + transTaken_{{$block.Name}}_policy_{{$pol.Name}} = 0; + //select transition to advance state + case({{$block.Name}}_policy_{{$pol.Name}}_state) + {{range $sti, $st := $pol.States}}` + "`" + `POLICY_STATE_{{$block.Name}}_{{$pol.Name}}_{{$st.Name}}: begin + {{range $tri, $tr := $pfbEnf.OutputPolicy.GetTransitionsForSource $st.Name}}{{/* + */}} + {{if $tri}}else {{end}}if ({{$cond := getVerilogECCTransitionCondition $block (compileExpression $tr.STGuard)}}{{$cond.IfCond}}) begin + //transition {{$tr.Source}} -> {{$tr.Destination}} on {{$tr.Condition}} + {{$block.Name}}_policy_{{$pol.Name}}_state = ` + "`" + `POLICY_STATE_{{$block.Name}}_{{$pol.Name}}_{{$tr.Destination}}; + //set expressions + {{range $exi, $ex := $tr.Expressions}} + {{$ex.VarName}} = {{$ex.Value}};{{end}} + transTaken_{{$block.Name}}_policy_{{$pol.Name}} = 1; + end {{end}} else begin + //only possible in a violation + {{$block.Name}}_policy_{{$pol.Name}}_state = ` + "`" + `POLICY_STATE_{{$block.Name}}_{{$pol.Name}}_violation; + transTaken_{{$block.Name}}_policy_{{$pol.Name}} = 1; + end + end + {{end}} + default begin + //if we are here, we're in the violation state + //the violation state permanently stays in violation + {{$block.Name}}_policy_{{$pol.Name}}_state = ` + "`" + `POLICY_STATE_{{$block.Name}}_{{$pol.Name}}_violation; + transTaken_{{$block.Name}}_policy_{{$pol.Name}} = 1; + end + endcase + {{end}} + //OUTPUT POLICY {{$pol.Name}} END + {{end}} +{{end}} + +{{define "functionVerilog"}}{{$block := index .Functions .FunctionIndex}}{{$blocks := .Functions}}{{$pbfPolicies := getAllPolicyEnfInfo $block}} +//This file should be called F_{{$block.Name}}.sv +//This is autogenerated code. Edit by hand at your peril! + +//To check this file using EBMC, run the following command: +//$ ebmc F_{{$block.Name}}.sv + +//For each policy, we need define types for the state machines +{{range $polI, $pol := $block.Policies}} +{{if len $pol.States}}{{range $index, $state := $pol.States}} +` + "`" + `define POLICY_STATE_{{$block.Name}}_{{$pol.Name}}_{{$state}} {{$index}}{{end}}{{else}}POLICY_STATE_{{$block.Name}}_{{$pol.Name}}_unknown 0{{end}} +` + "`" + `define POLICY_STATE_{{$block.Name}}_{{$pol.Name}}_violation {{if len $pol.States}}{{len $pol.States}}{{else}}1{{end}} +{{end}} + +module F_combinatorialVerilog_{{$block.Name}} ( + //inputs (plant to controller){{range $index, $var := $block.InputVars}} + input wire {{getVerilogWidthArrayForType $var.Type}} {{$var.Name}}_ptc_in, + output wire {{getVerilogWidthArrayForType $var.Type}} {{$var.Name}}_ptc_out, + {{end}} + //outputs (controller to plant){{range $index, $var := $block.OutputVars}} + input wire {{getVerilogWidthArrayForType $var.Type}} {{$var.Name}}_ctp_in, + output wire {{getVerilogWidthArrayForType $var.Type}} {{$var.Name}}_ctp_out, + {{end}} + + {{range $polI, $pol := $block.Policies}}//internal vars for EBMC to overload + {{range $vari, $var := $pol.InternalVars}}{{if not $var.Constant}}input wire {{getVerilogWidthArrayForType $var.Type}} {{$var.Name}}_in, + output wire {{getVerilogWidthArrayForType $var.Type}} {{$var.Name}}_out, + {{end}}{{end}}{{end}} + + //state input var + {{range $polI, $pol := $block.Policies}}{{if $polI}}, + {{end}}input wire {{getVerilogWidthArray (add (len $pol.States) 1)}} {{$block.Name}}_policy_{{$pol.Name}}_state_in, + output wire {{getVerilogWidthArray (add (len $pol.States) 1)}} {{$block.Name}}_policy_{{$pol.Name}}_state_out + {{end}} + +); + +{{range $index, $var := $block.InputVars}} +{{getVerilogType $var.Type}} {{$var.Name}} {{if $var.InitialValue}}/* = {{$var.InitialValue}}*/{{end}}; +{{end}}{{range $index, $var := $block.OutputVars}} +{{getVerilogType $var.Type}} {{$var.Name}} {{if $var.InitialValue}}/* = {{$var.InitialValue}}*/{{end}}; +{{end}}{{range $polI, $pol := $block.Policies}} +{{$pfbEnf := index $pbfPolicies $polI}}{{if not $pfbEnf}}//Policy is broken!{{else}}//internal vars +{{range $vari, $var := $pfbEnf.OutputPolicy.InternalVars}}{{if $var.Constant}}wire {{getVerilogWidthArrayForType $var.Type}} {{$var.Name}} = {{$var.InitialValue}}{{else}}{{getVerilogType $var.Type}} {{$var.Name}}{{if $var.InitialValue}}/* = {{$var.InitialValue}}*/{{end}}{{end}}; +{{end}}{{end}}{{end}} + +//For each policy, we need a reg for the state machine +{{range $polI, $pol := $block.Policies}}reg {{getVerilogWidthArray (add (len $pol.States) 1)}} {{$block.Name}}_policy_{{$pol.Name}}_state; +reg transTaken_{{$block.Name}}_policy_{{$pol.Name}}; //EBMC liveness check register flag (will be optimised away in normal compiles) +{{end}} + +always @* begin + + {{range $index, $var := $block.InputVars}} + {{$var.Name}} = {{$var.Name}}_ptc_in; + {{end}} + + {{range $index, $var := $block.OutputVars}} + {{$var.Name}} = {{$var.Name}}_ctp_in; + {{end}} + + //capture state/time inputs + {{range $polI, $pol := $block.Policies}} + {{$block.Name}}_policy_{{$pol.Name}}_state = {{$block.Name}}_policy_{{$pol.Name}}_state_in; + {{$pfbEnf := index $pbfPolicies $polI}}{{if not $pfbEnf}}//Policy is broken!{{else}}//internal vars + {{range $vari, $var := $pfbEnf.OutputPolicy.InternalVars}}{{if not $var.Constant}}{{$var.Name}} = {{$var.Name}}_in{{if $var.IsDTimer}} + 1{{end}};{{end}} + {{end}}{{end}}{{end}} + + + {{if $block.Policies}}{{template "_policyIn" $block}}{{end}} + {{if $block.Policies}}{{template "_policyOut" $block}}{{end}} +end + +{{range $index, $var := $block.InputVars}} +assign {{$var.Name}}_ptc_out = {{$var.Name}}; +{{end}} + +{{range $index, $var := $block.OutputVars}} +assign {{$var.Name}}_ctp_out = {{$var.Name}}; +{{end}} + +//emit state/time inputs +{{range $polI, $pol := $block.Policies}} +assign {{$block.Name}}_policy_{{$pol.Name}}_state_out = {{$block.Name}}_policy_{{$pol.Name}}_state; +{{$pfbEnf := index $pbfPolicies $polI}}{{if not $pfbEnf}}//Policy is broken!{{else}}//internal vars +{{range $vari, $var := $pfbEnf.OutputPolicy.InternalVars}}{{if not $var.Constant}}assign {{$var.Name}}_out = {{$var.Name}};{{end}} +{{end}}{{end}}{{end}} + +//For each policy, ensure correctness (systemverilog only) and liveness +{{range $polI, $pol := $block.Policies}}assert property ({{$block.Name}}_policy_{{$pol.Name}}_state_in >= ` + "`" + `POLICY_STATE_{{$block.Name}}_{{$pol.Name}}_violation || {{$block.Name}}_policy_{{$pol.Name}}_state_out != ` + "`" + `POLICY_STATE_{{$block.Name}}_{{$pol.Name}}_violation); +//(temporarily disabled) assert property (transTaken_{{$block.Name}}_policy_{{$pol.Name}} == 1); +{{end}} + +endmodule + + +module F_{{$block.Name}} ( + //inputs (plant to controller){{range $index, $var := $block.InputVars}} + input wire {{getVerilogWidthArrayForType $var.Type}} {{$var.Name}}_ptc_in, + output wire {{getVerilogWidthArrayForType $var.Type}} {{$var.Name}}_ptc_out, + {{end}} + //outputs (controller to plant){{range $index, $var := $block.OutputVars}} + input wire {{getVerilogWidthArrayForType $var.Type}} {{$var.Name}}_ctp_in, + output wire {{getVerilogWidthArrayForType $var.Type}} {{$var.Name}}_ctp_out, + {{end}} + + //state var for EBMC to overload + {{range $polI, $pol := $block.Policies}}input wire {{getVerilogWidthArray (add (len $pol.States) 1)}} {{$block.Name}}_policy_{{$pol.Name}}_state_embc_in, + {{end}} + {{range $polI, $pol := $block.Policies}}//internal vars for EBMC to overload + {{range $vari, $var := $pol.InternalVars}}{{if not $var.Constant}}input wire {{getVerilogWidthArrayForType $var.Type}} {{$var.Name}}_embc_in, + {{end}}{{end}} + {{end}} + + + input wire CLOCK +); + +//For each policy, we need a reg for the state machine +{{range $polI, $pol := $block.Policies}}reg {{getVerilogWidthArray (add (len $pol.States) 1)}} {{$block.Name}}_policy_{{$pol.Name}}_state = 0; +wire {{getVerilogWidthArray (add (len $pol.States) 1)}} {{$block.Name}}_policy_{{$pol.Name}}_state_next; +{{end}} + +/*{{range $index, $var := $block.InputVars}} +{{getVerilogType $var.Type}} {{$var.Name}} {{if $var.InitialValue}} = {{$var.InitialValue}}{{end}}; +{{end}}{{range $index, $var := $block.OutputVars}} +{{getVerilogType $var.Type}} {{$var.Name}} {{if $var.InitialValue}} = {{$var.InitialValue}}{{end}}; +{{end}}*/ + +{{range $polI, $pol := $block.Policies}} +{{$pfbEnf := index $pbfPolicies $polI}}{{if not $pfbEnf}}//Policy is broken!{{else}}//internal vars +{{range $vari, $var := $pfbEnf.OutputPolicy.InternalVars}}{{if not $var.Constant}}{{getVerilogType $var.Type}} {{$var.Name}}{{if $var.InitialValue}} = {{$var.InitialValue}}{{end}}; +wire {{getVerilogWidthArrayForType $var.Type}} {{$var.Name}}_next; +{{end}}{{end}}{{end}}{{end}} + +F_combinatorialVerilog_{{$block.Name}} combPart ( + //inputs (plant to controller){{range $index, $var := $block.InputVars}} + .{{$var.Name}}_ptc_in({{$var.Name}}_ptc_in), + .{{$var.Name}}_ptc_out({{$var.Name}}_ptc_out), + {{end}} + //outputs (controller to plant){{range $index, $var := $block.OutputVars}} + .{{$var.Name}}_ctp_in({{$var.Name}}_ctp_in), + .{{$var.Name}}_ctp_out({{$var.Name}}_ctp_out), + {{end}} + + {{range $polI, $pol := $block.Policies}}//internal vars for EBMC to overload + {{range $vari, $var := $pol.InternalVars}}{{if not $var.Constant}}.{{$var.Name}}_in({{$var.Name}}), + .{{$var.Name}}_out({{$var.Name}}_next), + {{end}}{{end}}{{end}} + + //state input var + {{range $polI, $pol := $block.Policies}}{{if $polI}}, + {{end}}.{{$block.Name}}_policy_{{$pol.Name}}_state_in({{$block.Name}}_policy_{{$pol.Name}}_state), + .{{$block.Name}}_policy_{{$pol.Name}}_state_out({{$block.Name}}_policy_{{$pol.Name}}_state_next) + {{end}} +); + + always@(posedge CLOCK) begin + //capture synchronous inputs + + {{range $polI, $pol := $block.Policies}}//internal vars + {{$block.Name}}_policy_{{$pol.Name}}_state = {{$block.Name}}_policy_{{$pol.Name}}_state_next; + {{range $vari, $var := $pol.InternalVars}}{{if not $var.Constant}}{{$var.Name}} = {{$var.Name}}_next; + {{end}}{{end}}{{end}} + + + end + +endmodule + +module test_F_{{$block.Name}} ( + //inputs (plant to controller){{range $index, $var := $block.InputVars}} + input wire {{getVerilogWidthArrayForType $var.Type}} {{$var.Name}}_ptc_in, + output wire {{getVerilogWidthArrayForType $var.Type}} {{$var.Name}}_ptc_out, + {{end}} + //outputs (controller to plant){{range $index, $var := $block.OutputVars}} + input wire {{getVerilogWidthArrayForType $var.Type}} {{$var.Name}}_ctp_in, + output wire {{getVerilogWidthArrayForType $var.Type}} {{$var.Name}}_ctp_out, + {{end}} + + input wire CLOCK +); + +{{range $index, $var := $block.InputVars}} +reg {{getVerilogWidthArrayForType $var.Type}} {{$var.Name}}_ptc_in_reg; +wire {{getVerilogWidthArrayForType $var.Type}} {{$var.Name}}_ptc_out_wire; +reg {{getVerilogWidthArrayForType $var.Type}} {{$var.Name}}_ptc_out_reg; +{{end}} + +//outputs (controller to plant){{range $index, $var := $block.OutputVars}} +reg {{getVerilogWidthArrayForType $var.Type}} {{$var.Name}}_ctp_in_reg; +wire {{getVerilogWidthArrayForType $var.Type}} {{$var.Name}}_ctp_out_wire; +reg {{getVerilogWidthArrayForType $var.Type}} {{$var.Name}}_ctp_out_reg; +{{end}} + +F_{{$block.Name}} test ( + + //inputs (plant to controller){{range $index, $var := $block.InputVars}} + .{{$var.Name}}_ptc_in({{$var.Name}}_ptc_in_reg), + .{{$var.Name}}_ptc_out({{$var.Name}}_ptc_out_wire), + {{end}} + //outputs (controller to plant){{range $index, $var := $block.OutputVars}} + .{{$var.Name}}_ctp_in({{$var.Name}}_ctp_in_reg), + .{{$var.Name}}_ctp_out({{$var.Name}}_ctp_out_wire), + {{end}} + + .CLOCK(CLOCK) +); + +always@(posedge CLOCK) begin + //inputs (plant to controller) + {{range $index, $var := $block.InputVars}} + {{$var.Name}}_ptc_in_reg = {{$var.Name}}_ptc_in; + {{$var.Name}}_ptc_out_reg = {{$var.Name}}_ptc_out_wire; + {{end}} + + //outputs (controller to plant){{range $index, $var := $block.OutputVars}} + {{$var.Name}}_ctp_in_reg = {{$var.Name}}_ctp_in; + {{$var.Name}}_ctp_out_reg = {{$var.Name}}_ctp_out_wire; + {{end}} + +end + +//inputs (plant to controller) +{{range $index, $var := $block.InputVars}} +assign {{$var.Name}}_ptc_out = {{$var.Name}}_ptc_out_reg; +{{end}} + +//outputs (controller to plant) +{{range $index, $var := $block.OutputVars}} +assign {{$var.Name}}_ctp_out = {{$var.Name}}_ctp_out_reg; +{{end}} + +endmodule + +{{end}} +` + +var verilogTemplateFuncMap = template.FuncMap{ + "getVerilogECCTransitionCondition": getVerilogECCTransitionCondition, + "getVerilogType": getVerilogType, + "getPolicyEnfInfo": getPolicyEnfInfo, + "getAllPolicyEnfInfo": getAllPolicyEnfInfo, + "getVerilogWidthArray": getVerilogWidthArray, + "getVerilogWidthArrayForType": getVerilogWidthArrayForType, + "add1IfClock": add1IfClock, + + "compileExpression": stconverter.VerilogCompileExpression, + + "add": add, +} + +var verilogTemplates = template.Must(template.New("").Funcs(verilogTemplateFuncMap).Parse(rteVerilogTemplate)) diff --git a/rvc/rteVerilogTemplateFunctions.go b/rvc/rteVerilogTemplateFunctions.go new file mode 100644 index 0000000..7f1d0d6 --- /dev/null +++ b/rvc/rteVerilogTemplateFunctions.go @@ -0,0 +1,116 @@ +package rtec + +import ( + "fmt" + "strings" + + "github.com/PRETgroup/easy-rte/rtedef" +) + +//VerilogECCTransition is used with getVerilogECCTransitionCondition to return results to the template +type VerilogECCTransition CECCTransition + +//getVerilogECCTransitionCondition returns the C "if" condition to use in state machine next state logic and associated events +// returns "full condition", "associated events" +func getVerilogECCTransitionCondition(function rtedef.EnforcedFunction, trans string) VerilogECCTransition { + + return VerilogECCTransition{IfCond: trans, AssEvents: nil} +} + +//getVerilogType returns the VHDL type to use with respect to an IEC61499 type +func getVerilogType(ctype string) string { + return "reg " + getVerilogWidthArrayForType(ctype) +} + +func getVerilogWidthArrayForType(ctype string) string { + verilogType := "" + + switch strings.ToLower(ctype) { + case "bool": + verilogType = "" + case "char": + verilogType = "[7:0]" + case "uint8_t": + verilogType = "[7:0]" + case "uint16_t": + verilogType = "[15:0]" + case "uint32_t": + verilogType = "[31:0]" + case "uint64_t": + verilogType = "[63:0]" + case "int8_t": + verilogType = "signed [7:0]" + case "int16_t": + verilogType = "signed [15:0]" + case "int32_t": + verilogType = "signed [31:0]" + case "int64_t": + verilogType = "signed [63:0]" + case "float": + panic("Float type not allowed in conversion") + case "double": + panic("Double type not allowed in conversion") + case "dtimer_t": + verilogType = "[63:0]" + case "rtimer_t": + panic("rtimer type not allowed in conversion") + default: + panic("Unknown type: " + ctype) + } + + return verilogType +} + +func add1IfClock(ctype string) string { + if ctype == "dtimer_t" { + return " + 1" + } + if ctype == "rtimer_t" { + panic("rtimer type not allowed in conversion") + } + return "" +} + +func getVerilogWidthArray(l int) string { + cl2 := ceilLog2(uint64(l)) - 1 + if cl2 >= 1 { + return fmt.Sprintf("[%v:0]", cl2) + } + return "" +} + +var t = [6]uint64{ + 0xFFFFFFFF00000000, + 0x00000000FFFF0000, + 0x000000000000FF00, + 0x00000000000000F0, + 0x000000000000000C, + 0x0000000000000002, +} + +//ceilLog2 performs a log2 ceiling function quickly +func ceilLog2(x uint64) int { + + y := 0 + if (x & (x - 1)) != 0 { + y = 1 + } + j := 32 + var i int + + for i = 0; i < 6; i++ { + k := 0 + if (x & t[i]) != 0 { + k = j + } + y += k + x >>= uint64(k) + j >>= 1 + } + + return y +} + +func add(a, b int) int { + return a + b +} diff --git a/rvc/rteVhdlTemplate.go b/rvc/rteVhdlTemplate.go new file mode 100644 index 0000000..03c68ec --- /dev/null +++ b/rvc/rteVhdlTemplate.go @@ -0,0 +1,147 @@ +package rtec + +import ( + "text/template" + + "github.com/PRETgroup/goFB/goFB/stconverter" +) + +const rteVhdlTemplate = `{{define "_policyIn"}}{{$block := .}} + --input policies + {{range $polI, $pol := $block.Policies}}{{$pfbEnf := getPolicyEnfInfo $block $polI}} + {{if not $pfbEnf}}--{{$pol.Name}} is broken! + {{else}}{{/* this is where the policy comes in */}}--INPUT POLICY {{$pol.Name}} BEGIN + case {{$pol.Name}}_state is + {{range $sti, $st := $pol.States}}when s_{{$pol.Name}}_{{$st.Name}} => + {{range $tri, $tr := $pfbEnf.InputPolicy.GetViolationTransitions}}{{if eq $tr.Source $st.Name}}{{/* + */}} + if ({{$cond := getVhdlECCTransitionCondition $block (compileExpression $tr.STGuard)}}{{$cond.IfCond}}) then + --transition {{$tr.Source}} -> {{$tr.Destination}} on {{$tr.Condition}} + --select a transition to solve the problem + {{$solution := $pfbEnf.SolveViolationTransition $tr true}} + {{if $solution.Comment}}--{{$solution.Comment}}{{end}} + {{range $soleI, $sole := $solution.Expressions}}{{$sol := getVhdlECCTransitionCondition $block (compileExpression $sole)}}{{$sol.IfCond}}; + {{end}} + end if; {{end}}{{end}} + {{end}} + end case; + {{end}} + --INPUT POLICY {{$pol.Name}} END + {{end}} +{{end}} + +{{define "_policyOut"}}{{$block := .}} + --output policies + {{range $polI, $pol := $block.Policies}}{{$pfbEnf := getPolicyEnfInfo $block $polI}} + {{if not $pfbEnf}}--{{$pol.Name}} is broken! + {{else}}{{/* this is where the policy comes in */}}--OUTPUT POLICY {{$pol.Name}} BEGIN + case {{$pol.Name}}_state is + {{range $sti, $st := $pol.States}}when s_{{$pol.Name}}_{{$st.Name}} => + {{range $tri, $tr := $pfbEnf.OutputPolicy.GetViolationTransitions}}{{if eq $tr.Source $st.Name}}{{/* + */}} + if ({{$cond := getVhdlECCTransitionCondition $block (compileExpression $tr.STGuard)}}{{$cond.IfCond}}) then + --transition {{$tr.Source}} -> {{$tr.Destination}} on {{$tr.Condition}} + --select a transition to solve the problem + {{$solution := $pfbEnf.SolveViolationTransition $tr false}} + {{if $solution.Comment}}--{{$solution.Comment}}{{end}} + {{range $soleI, $sole := $solution.Expressions}}{{$sol := getVhdlECCTransitionCondition $block (compileExpression $sole)}}{{$sol.IfCond}}; + {{end}} + end if; {{end}}{{end}} + + {{end}} + end case; + + --advance timers + {{range $varI, $var := $pfbEnf.OutputPolicy.GetDTimers}} + {{$var.Name}} := {{$var.Name}} + 1;{{end}} + + --select transition to advance state + case {{$pol.Name}}_state is + {{range $sti, $st := $pol.States}}when s_{{$pol.Name}}_{{$st.Name}} => + {{range $tri, $tr := $pfbEnf.OutputPolicy.GetNonViolationTransitions}}{{if eq $tr.Source $st.Name}}{{/* + */}} + if ({{$cond := getVhdlECCTransitionCondition $block (compileExpression $tr.STGuard)}}{{$cond.IfCond}}) then + --transition {{$tr.Source}} -> {{$tr.Destination}} on {{$tr.Condition}} + {{$pol.Name}}_state := s_{{$pol.Name}}_{{$tr.Destination}}; + --set expressions + {{range $exi, $ex := $tr.Expressions}} + {{$ex.VarName}} := {{$ex.Value}};{{end}} + end if; {{end}}{{end}} + + {{end}} + end case; + {{end}} + --OUTPUT POLICY {{$pol.Name}} END + {{end}} +{{end}} + +{{define "functionVhdl"}}{{$block := index .Functions .FunctionIndex}}{{$blocks := .Functions}} +--This file should be called enforcer_{{$block.Name}}.vhdl +--This is autogenerated code. Edit by hand at your peril! + +library ieee; +use ieee.std_logic_1164.all; +use ieee.numeric_std.all; + +entity enforcer_{{$block.Name}} is + port ( + {{range $index, $var := $block.InputVars}} + {{$var.Name}}_ptc_in : in {{getVhdlType $var.Type}}{{if $var.InitialValue}} := {{$var.InitialValue}}{{end}}; + {{$var.Name}}_ptc_out : out {{getVhdlType $var.Type}}{{if $var.InitialValue}} := {{$var.InitialValue}}{{end}}; + {{end}} + + {{range $index, $var := $block.OutputVars}} + {{$var.Name}}_ctp_in : in {{getVhdlType $var.Type}}{{if $var.InitialValue}} := {{$var.InitialValue}}{{end}}; + {{$var.Name}}_ctp_out : out {{getVhdlType $var.Type}}{{if $var.InitialValue}} := {{$var.InitialValue}}{{end}}; + {{end}} + + CLOCK: in std_logic + ); +end entity; + +architecture rtl of enforcer_{{$block.Name}} is + +--For each policy, we need a state_type for the state machine +{{range $polI, $pol := $block.Policies}} + type {{$pol.Name}}_state_type is ({{if len $pol.States}}{{range $index, $state := $pol.States}} + s_{{$pol.Name}}_{{$state}}{{if not $index}}, {{end}}{{end}}{{else}}s_{{$pol.Name}}_unknown{{end}} + ); + + signal {{$pol.Name}}_state : {{$pol.Name}}_state_type := {{if len $pol.States}}{{$state := index $pol.States 0}}s_{{$pol.Name}}_{{$state}}{{else}}s_{{$pol.Name}}_unknown{{end}}; +{{end}} +begin + + process(CLOCK) + {{range $index, $var := $block.InputVars}} + variable {{$var.Name}} : {{getVhdlType $var.Type}}{{if $var.InitialValue}} := {{$var.InitialValue}}{{end}}; + {{end}}{{range $index, $var := $block.OutputVars}} + variable {{$var.Name}} : {{getVhdlType $var.Type}}{{if $var.InitialValue}} := {{$var.InitialValue}}{{end}}; + {{end}}{{range $polI, $pol := $block.Policies}} + {{$pfbEnf := getPolicyEnfInfo $block $polI}}{{if not $pfbEnf}}--Policy is broken!{{else}}--internal vars + variable {{range $vari, $var := $pfbEnf.OutputPolicy.InternalVars}}{{$var.Name}} : {{getVhdlType $var.Type}}{{if $var.InitialValue}} := "{{$var.InitialValue}}"{{end}}; + {{end}}{{end}}{{end}} + + begin + if (rising_edge(CLOCK)) then + --capture synchronous inputs + {{range $index, $var := $block.InputVars}} + {{$var.Name}} := {{$var.Name}}_ptc_in; + {{end}} + + {{if $block.Policies}}{{template "_policyIn" $block}}{{end}} + + {{if $block.Policies}}{{template "_policyOut" $block}}{{end}} + + end if; + end process; +end architecture;{{end}}` + +var vhdlTemplateFuncMap = template.FuncMap{ + "getVhdlECCTransitionCondition": getVhdlECCTransitionCondition, + "getVhdlType": getVhdlType, + "getPolicyEnfInfo": getPolicyEnfInfo, + + "compileExpression": stconverter.VhdlCompileExpression, +} + +var vhdlTemplates = template.Must(template.New("").Funcs(vhdlTemplateFuncMap).Parse(rteVhdlTemplate)) diff --git a/rvc/rteVhdlTemplateFunctions.go b/rvc/rteVhdlTemplateFunctions.go new file mode 100644 index 0000000..b4c25be --- /dev/null +++ b/rvc/rteVhdlTemplateFunctions.go @@ -0,0 +1,59 @@ +package rtec + +import ( + "fmt" + "strings" + + "github.com/PRETgroup/easy-rte/rtedef" +) + +//VhdlECCTransition is used with getVhdlECCTransitionCondition to return results to the template +type VhdlECCTransition CECCTransition + +//getVhdlECCTransitionCondition returns the C "if" condition to use in state machine next state logic and associated events +// returns "full condition", "associated events" +func getVhdlECCTransitionCondition(function rtedef.EnforcedFunction, trans string) VhdlECCTransition { + + return VhdlECCTransition{IfCond: trans, AssEvents: nil} +} + +//getVhdlType returns the VHDL type to use with respect to an IEC61499 type +func getVhdlType(ctype string) string { + vhdlType := "" + + switch strings.ToLower(ctype) { + case "bool": + vhdlType = "integer range 0 to 1" + case "char": + vhdlType = "integer range 0 to (2**8 - 1)" + case "uint8_t": + vhdlType = "integer range 0 to (2**8 - 1)" + case "uint16_t": + vhdlType = "integer range 0 to (2**16 - 1)" + case "uint32_t": + fmt.Printf("WARNING: uint32_t type constrainted to max value 2^31-1 in VHDL") + vhdlType = "integer range 0 to (2**31 - 1)" + case "uint64_t": + panic("uint16_t type not allowed in conversion") + case "int8_t": + vhdlType = "integer range -(2**7) to (2**7-1)" + case "int16_t": + vhdlType = "integer range -(2**15) to (2**15-1)" + case "int32_t": + vhdlType = "integer" + case "int64_t": + panic("int64_t type not allowed in conversion") + case "float": + panic("Float type not allowed in conversion") + case "double": + panic("Double type not allowed in conversion") + case "dtimer_t": + vhdlType = "integer range 0 to (2**31 - 1)" + case "rtimer_t": + panic("rtimer type not allowed in conversion") + default: + panic("Unknown type: " + ctype) + } + + return vhdlType +} diff --git a/rvc/rtecTemplate.go b/rvc/rtecTemplate.go new file mode 100644 index 0000000..8c05bf8 --- /dev/null +++ b/rvc/rtecTemplate.go @@ -0,0 +1,301 @@ +package rtec + +import ( + "text/template" + + "github.com/PRETgroup/goFB/goFB/stconverter" +) + +const rtecTemplate = `{{define "_policyIn"}}{{$block := .}} +//input policies +{{range $polI, $pol := $block.Policies}}{{$pfbEnf := getPolicyEnfInfo $block $polI}} +{{if not $pfbEnf}}//{{$pol.Name}} is broken! +{{else}}{{/* this is where the policy comes in */}}//INPUT POLICY {{$pol.Name}} BEGIN +//This will run the input enforcer for {{$block.Name}}'s policy {{$pol.Name}} +void {{$block.Name}}_run_input_enforcer_{{$pol.Name}}(enforcervars_{{$block.Name}}_t* me, inputs_{{$block.Name}}_t* inputs) { + switch(me->_policy_{{$pol.Name}}_state) { + {{range $sti, $st := $pol.States}}case POLICY_STATE_{{$block.Name}}_{{$pol.Name}}_{{$st.Name}}: + {{range $tri, $tr := $pfbEnf.InputPolicy.GetViolationTransitions}}{{if eq $tr.Source $st.Name}}{{/* + */}} + if({{$cond := getCECCTransitionCondition $block (compileExpression $tr.STGuard)}}{{$cond.IfCond}}) { + //transition {{$tr.Source}} -> {{$tr.Destination}} on {{$tr.Condition}} + //select a transition to solve the problem + {{$solution := $pfbEnf.SolveViolationTransition $tr true}} + {{if $solution.Comment}}//{{$solution.Comment}}{{end}} + {{range $soleI, $sole := $solution.Expressions}}{{$sol := getCECCTransitionCondition $block (compileExpression $sole)}}{{$sol.IfCond}}; + {{end}} + } {{end}}{{end}} + + break; + + {{end}} + } +} +{{end}} +//INPUT POLICY {{$pol.Name}} END +{{end}}{{end}} + +{{define "_policyOut"}}{{$block := .}} +//output policies +{{range $polI, $pol := $block.Policies}}{{$pfbEnf := getPolicyEnfInfo $block $polI}} +{{if not $pfbEnf}}//{{$pol.Name}} is broken! +{{else}}{{/* this is where the policy comes in */}}//OUTPUT POLICY {{$pol.Name}} BEGIN +//This will run the input enforcer for {{$block.Name}}'s policy {{$pol.Name}} +void {{$block.Name}}_run_output_enforcer_{{$pol.Name}}(enforcervars_{{$block.Name}}_t* me, inputs_{{$block.Name}}_t* inputs, outputs_{{$block.Name}}_t* outputs) { + //advance timers + {{range $varI, $var := $pfbEnf.OutputPolicy.GetDTimers}} + me->{{$var.Name}}++;{{end}} + + //run enforcer + switch(me->_policy_{{$pol.Name}}_state) { + {{range $sti, $st := $pol.States}}case POLICY_STATE_{{$block.Name}}_{{$pol.Name}}_{{$st.Name}}: + {{range $tri, $tr := $pfbEnf.OutputPolicy.GetViolationTransitions}}{{if eq $tr.Source $st.Name}}{{/* + */}} + if({{$cond := getCECCTransitionCondition $block (compileExpression $tr.STGuard)}}{{$cond.IfCond}}) { + //transition {{$tr.Source}} -> {{$tr.Destination}} on {{$tr.Condition}} + //select a transition to solve the problem + {{$solution := $pfbEnf.SolveViolationTransition $tr false}} + {{if $solution.Comment}}//{{$solution.Comment}}{{end}} + {{range $soleI, $sole := $solution.Expressions}}{{$sol := getCECCTransitionCondition $block (compileExpression $sole)}}{{$sol.IfCond}}; + {{end}} + } {{end}}{{end}} + + break; + + {{end}} + } + + //select transition to advance state + switch(me->_policy_{{$pol.Name}}_state) { + {{range $sti, $st := $pol.States}}case POLICY_STATE_{{$block.Name}}_{{$pol.Name}}_{{$st.Name}}: + {{range $tri, $tr := $pfbEnf.OutputPolicy.Transitions}}{{if eq $tr.Source $st.Name}}{{/* + */}} + if({{$cond := getCECCTransitionCondition $block (compileExpression $tr.STGuard)}}{{$cond.IfCond}}) { + //transition {{$tr.Source}} -> {{$tr.Destination}} on {{$tr.Condition}} + me->_policy_{{$pol.Name}}_state = POLICY_STATE_{{$block.Name}}_{{$pol.Name}}_{{$tr.Destination}}; + //set expressions + {{range $exi, $ex := $tr.Expressions}} + me->{{$ex.VarName}} = {{$ex.Value}};{{end}} + break; + } {{end}}{{end}} + + //ensure a transition was taken in this state + assert(false && "{{$block.Name}}_{{$pol.Name}}_{{$st.Name}} must take a transition"); //if we are still here, then no transition was taken and we are no longer satisfying liveness + + break; + + {{end}} + } + + //ensure we did not violate (i.e. we did not enter violation state) + assert(me->_policy_{{$pol.Name}}_state != POLICY_STATE_{{$block.Name}}_{{$pol.Name}}_violation); +} +{{end}} +//OUTPUT POLICY {{$pol.Name}} END +{{end}} +{{end}} + +{{define "functionH"}}{{$block := index .Functions .FunctionIndex}}{{$blocks := .Functions}} +//This file should be called F_{{$block.Name}}.h +//This is autogenerated code. Edit by hand at your peril! + +#include +#include +#include + +//the dtimer_t type +typedef uint64_t dtimer_t; + +//For each policy, we need an enum type for the state machine +{{range $polI, $pol := $block.Policies}} +enum {{$block.Name}}_policy_{{$pol.Name}}_states { {{if len $pol.States}}{{range $index, $state := $pol.States}}{{if $index}}, {{end}} + POLICY_STATE_{{$block.Name}}_{{$pol.Name}}_{{$state}}{{end}}{{else}}POLICY_STATE_{{$block.Name}}_{{$pol.Name}}_unknown{{end}}, + POLICY_STATE_{{$block.Name}}_{{$pol.Name}}_violation +}; +{{end}} + +//Inputs to the function {{$block.Name}} +typedef struct { + {{range $index, $var := $block.InputVars}}{{$var.Type}} {{$var.Name}}{{if $var.ArraySize}}[{{$var.ArraySize}}]{{end}}; + {{end}} +} inputs_{{$block.Name}}_t; + +//Outputs from the function {{$block.Name}} +typedef struct { + {{range $index, $var := $block.OutputVars}}{{$var.Type}} {{$var.Name}}{{if $var.ArraySize}}[{{$var.ArraySize}}]{{end}}; + {{end}} +} outputs_{{$block.Name}}_t; + +//enforcer state and vars: +typedef struct { + {{range $polI, $pol := $block.Policies}}enum {{$block.Name}}_policy_{{$pol.Name}}_states _policy_{{$pol.Name}}_state; + {{$pfbEnf := getPolicyEnfInfo $block $polI}}{{if not $pfbEnf}}//Policy is broken!{{else}}//internal vars + {{range $vari, $var := $pfbEnf.OutputPolicy.InternalVars}}{{if not $var.Constant}}{{$var.Type}} {{$var.Name}}{{if $var.ArraySize}}[{{$var.ArraySize}}]{{end}}; + {{end}}{{end}} + {{end}} + {{end}} +} enforcervars_{{$block.Name}}_t; + +{{range $polI, $pol := $block.Policies -}} +{{range $varI, $var := $pol.InternalVars -}} +{{if $var.Constant}}#define CONST_{{$pol.Name}}_{{$var.Name}} {{$var.InitialValue}}{{end}} +{{end}}{{end}} + +//This function is provided in "F_{{$block.Name}}.c" +//It sets up the variable structures to their initial values +void {{$block.Name}}_init_all_vars(enforcervars_{{$block.Name}}_t* me, inputs_{{$block.Name}}_t* inputs, outputs_{{$block.Name}}_t* outputs); + +//This function is provided in "F_{{$block.Name}}.c" +//It will run the synthesised enforcer and call the controller function +void {{$block.Name}}_run_via_enforcer(enforcervars_{{$block.Name}}_t* me, inputs_{{$block.Name}}_t* inputs, outputs_{{$block.Name}}_t* outputs); + +//This function is provided from the user +//It is the controller function +extern void {{$block.Name}}_run(inputs_{{$block.Name}}_t* inputs, outputs_{{$block.Name}}_t* outputs); + +//enforcer functions + +{{range $polI, $pol := $block.Policies}} +//This function is provided in "F_{{$block.Name}}.c" +//It will run the input enforcer for {{$block.Name}}'s policy {{$pol.Name}} +void {{$block.Name}}_run_input_enforcer_{{$pol.Name}}(enforcervars_{{$block.Name}}_t* me, inputs_{{$block.Name}}_t* inputs); + +//This function is provided in "F_{{$block.Name}}.c" +//It will run the input enforcer for {{$block.Name}}'s policy {{$pol.Name}} +void {{$block.Name}}_run_output_enforcer_{{$pol.Name}}(enforcervars_{{$block.Name}}_t* me, inputs_{{$block.Name}}_t* inputs, outputs_{{$block.Name}}_t* outputs); + +//This function is provided in "F_{{$block.Name}}.c" +//It will check the state of the enforcer monitor code +//It returns one of the following: +//0: currently true (safe) +//1: always true (safe) +//-1: currently false (unsafe) +//-2: always false (unsafe) +//It will need to do some reachability analysis to achieve this +int {{$block.Name}}_check_rv_status_{{$pol.Name}}(enforcervars_{{$block.Name}}_t* me); + +{{end}} +{{end}} + +{{define "functionC"}}{{$block := index .Functions .FunctionIndex}}{{$blocks := .Functions}} +//This file should be called F_{{$block.Name}}.c +//This is autogenerated code. Edit by hand at your peril! +#include "F_{{$block.Name}}.h" + +void {{$block.Name}}_init_all_vars(enforcervars_{{$block.Name}}_t* me, inputs_{{$block.Name}}_t* inputs, outputs_{{$block.Name}}_t* outputs) { + //set any input vars with default values + {{range $index, $var := $block.InputVars}}{{if $var.InitialValue}}{{$initialArray := $var.GetInitialArray}}{{if $initialArray}}{{range $initialIndex, $initialValue := $initialArray}}inputs->{{$var.Name}}[{{$initialIndex}}] = {{$initialValue}}; + {{end}}{{else}}inputs->{{$var.Name}} = {{$var.InitialValue}}; + {{end}}{{end}}{{end}} + //set any output vars with default values + {{range $index, $var := $block.OutputVars}}{{if $var.InitialValue}}{{$initialArray := $var.GetInitialArray}}{{if $initialArray}}{{range $initialIndex, $initialValue := $initialArray}}outputs->{{$var.Name}}[{{$initialIndex}}] = {{$initialValue}}; + {{end}}{{else}}outputs->{{$var.Name}} = {{$var.InitialValue}}; + {{end}}{{end}}{{end}} + + {{if $block.Policies}}{{range $polI, $pol := $block.Policies}} + me->_policy_{{$pol.Name}}_state = {{if $pol.States}}POLICY_STATE_{{$block.Name}}_{{$pol.Name}}_{{(index $pol.States 0).Name}}{{else}}POLICY_STATE_{{$block.Name}}_{{$pol.Name}}_unknown{{end}}; + {{$pfbEnf := getPolicyEnfInfo $block $polI}}{{if not $pfbEnf}}//Policy is broken!{{else}}//input policy internal vars + {{range $vari, $var := $pfbEnf.OutputPolicy.InternalVars}}{{if not $var.Constant}} + {{$initialArray := $var.GetInitialArray}}{{if $initialArray}}{{range $initialIndex, $initialValue := $initialArray}}me->{{$var.Name}}[{{$initialIndex}}] = {{$initialValue}}; + {{end}}{{else}}me->{{$var.Name}} = {{if $var.InitialValue}}{{$var.InitialValue}}{{else}}0{{end}}; + {{end}}{{end}}{{end}}{{end}} + {{end}}{{end}} +} + +void {{$block.Name}}_run_via_enforcer(enforcervars_{{$block.Name}}_t* me, inputs_{{$block.Name}}_t* inputs, outputs_{{$block.Name}}_t* outputs) { + //run the policies in reverse order for the inputs (last policies have highest priority) + {{$lpol := len $block.Policies}} + {{range $polI, $pol_unused := $block.Policies}}{{$acti := sub (sub $lpol 1) $polI}}{{$pol := index $block.Policies $acti}} {{$block.Name}}_run_input_enforcer_{{$pol.Name}}(me, inputs); + {{end}} + + {{$block.Name}}_run(inputs, outputs); + + //run policies in specified order for outputs + {{range $polI, $pol := $block.Policies}}{{$block.Name}}_run_output_enforcer_{{$pol.Name}}(me, inputs,outputs); + {{end}} +} + +{{if $block.Policies}}{{template "_policyIn" $block}}{{end}} + +{{if $block.Policies}}{{template "_policyOut" $block}}{{end}} + +//This function is provided in "F_{{$block.Name}}.c" +//It will check the state of the enforcer monitor code +//It returns one of the following: +//0: currently true (safe) +//1: always true (safe) +//-1: currently false (unsafe) +//-2: always false (unsafe) +//It will need to do some reachability analysis to achieve this +{{/*int {{$block.Name}}_check_rv_status_{{$pol.Name}}(enforcervars_{{$block.Name}}_t* me) { + //TODO: this function + return -2; +}*/}} +{{end}} +{{define "mainCBMCC"}}{{$block := index .Functions .FunctionIndex}}{{$blocks := .Functions}} +//This file should be called cbmc_main_{{$block.Name}}.c +//This is autogenerated code. Edit by hand at your peril! + +//It can be used with the cbmc model checker +//Call it using the following command: +//$ cbmc cbmc_main_{{$block.Name}}.c{{range $blockI, $block := $blocks}} F_{{$block.Name}}.c{{end}} + +{{range $blockI, $block := $blocks}} +#include "F_{{$block.Name}}.h"{{end}} +#include +#include + +int main() { + +{{range $blockI, $block := $blocks}} + //I/O and state for {{$block.Name}} + enforcervars_{{$block.Name}}_t enf_{{$block.Name}}; + inputs_{{$block.Name}}_t inputs_{{$block.Name}}; + outputs_{{$block.Name}}_t outputs_{{$block.Name}}; + + //set values to known state + {{$block.Name}}_init_all_vars(&enf_{{$block.Name}}, &inputs_{{$block.Name}}, &outputs_{{$block.Name}}); + + //introduce nondeterminism + //a nondet_xxxxx function name tells cbmc that it could be anything, but must be unique + //randomise inputs + {{range $inputI, $input := $block.InputVars -}} + inputs_{{$block.Name}}.{{$input.Name}} = nondet_{{$block.Name}}_input_{{$inputI}}(); + {{end}} + + //randomise enforcer state, i.e. clock values and position (excepting violation state) + {{range $polI, $pol := $block.Policies -}} + {{range $varI, $var := $pol.InternalVars -}} + {{if not $var.Constant}}enf_{{$block.Name}}.{{$var.Name}} = nondet_{{$block.Name}}_enf_{{$pol.Name}}_{{$varI}}();{{end}} + {{end}} + enf_{{$block.Name}}._policy_{{$pol.Name}}_state = nondet_{{$block.Name}}_enf_{{$pol.Name}}_state() % {{len $pol.States}}; + {{end}} + + //run the enforcer (i.e. tell CBMC to check this out) + {{$block.Name}}_run_via_enforcer(&enf_{{$block.Name}}, &inputs_{{$block.Name}}, &outputs_{{$block.Name}}); +{{end}} +} + +{{range $blockI, $block := $blocks}} +void {{$block.Name}}_run(inputs_{{$block.Name}}_t *inputs, outputs_{{$block.Name}}_t *outputs) { + //randomise controller + + {{range $outputI, $output := $block.OutputVars -}} + outputs->{{$output.Name}} = nondet_{{$block.Name}}_output_{{$outputI}}(); + {{end}} +} +{{end}} +{{end}} +` + +var cTemplateFuncMap = template.FuncMap{ + "getCECCTransitionCondition": getCECCTransitionCondition, + + "getPolicyEnfInfo": getPolicyEnfInfo, + + "compileExpression": stconverter.CCompileExpression, + + "sub": sub, +} + +var cTemplates = template.Must(template.New("").Funcs(cTemplateFuncMap).Parse(rtecTemplate)) diff --git a/rvc/rtecTemplateFunctions.go b/rvc/rtecTemplateFunctions.go new file mode 100644 index 0000000..19f3286 --- /dev/null +++ b/rvc/rtecTemplateFunctions.go @@ -0,0 +1,122 @@ +package rtec + +import ( + "regexp" + "strings" + + "github.com/PRETgroup/easy-rte/rtedef" +) + +//CECCTransition is used with getCECCTransitionCondition to return results to the template +type CECCTransition struct { + IfCond string + AssEvents []string +} + +//getCECCTransitionCondition returns the C "if" condition to use in state machine next state logic and associated events +// returns "full condition", "associated events" +func getCECCTransitionCondition(function rtedef.EnforcedFunction, trans string) CECCTransition { + var events []string + + re1 := regexp.MustCompile("([<>=!]+)") //for capturing operators + re2 := regexp.MustCompile("([a-zA-Z0-9_<>=]+)") //for capturing variable and event names and operators + isNum := regexp.MustCompile("^[0-9.]+$") + + retVal := trans + + //rename AND and OR + retVal = strings.Replace(retVal, "AND", "&&", -1) + retVal = strings.Replace(retVal, "OR", "||", -1) + + //re1: add whitespace around operators + retVal = re1.ReplaceAllStringFunc(retVal, func(in string) string { + if in != "!" { + return " " + in + " " + } + return " !" + }) + + //re2: add "me->" where appropriate + retVal = re2.ReplaceAllStringFunc(retVal, func(in string) string { + if strings.ToLower(in) == "and" || strings.ToLower(in) == "or" || strings.ContainsAny(in, "!><=") || strings.ToLower(in) == "true" || strings.ToLower(in) == "false" { + //no need to make changes, these aren't variables or events + return in + } + + if isNum.MatchString(in) { + //no need to make changes, it is a numerical value of some sort + return in + } + + //check to see if it is input data + if function.InputVars != nil { + for _, Var := range function.InputVars { + if Var.Name == in { + return "inputs->" + in + } + } + } + + //check to see if it is output data + if function.OutputVars != nil { + for _, Var := range function.OutputVars { + if Var.Name == in { + return "outputs->" + in + } + } + } + + //check to see if it is a policy internal var + for i := 0; i < len(function.Policies); i++ { + for _, Var := range function.Policies[i].InternalVars { + if Var.Name == in || Var.Name+"_i" == in { + if Var.Constant { + return "CONST_" + function.Policies[i].Name + "_" + in + } + return "me->" + in + } + } + } + + //else, return it (no idea what else to do!) - it might be a function call or strange text constant + return in + }) + + //tidy the whitespace + retVal = strings.Replace(retVal, " ", " ", -1) + + return CECCTransition{IfCond: retVal, AssEvents: events} +} + +//getPolicyEnfInfo will get a PEnforcer for a given policy +func getPolicyEnfInfo(function rtedef.EnforcedFunction, policyIndex int) *rtedef.PEnforcer { + enfPol, err := rtedef.MakePEnforcer(function.InterfaceList, function.Policies[policyIndex]) + if err != nil { + return nil + } + //Uncomment these two lines to generate the intermediate enforcer JSON file + //bytes, _ := json.MarshalIndent(enfPol, "", "\t") + //ioutil.WriteFile(function.Name+".json", bytes, 0644) + return enfPol +} + +//getAllPolicyEnfInfo will get a PEnforcer for a given policy +func getAllPolicyEnfInfo(function rtedef.EnforcedFunction) []rtedef.PEnforcer { + pols := make([]rtedef.PEnforcer, 0, len(function.Policies)) + for i := 0; i < len(function.Policies); i++ { + enfPol, err := rtedef.MakePEnforcer(function.InterfaceList, function.Policies[i]) + if err != nil { + return nil + } + pols = append(pols, *enfPol) + } + + //Uncomment these two lines to generate the intermediate enforcer JSON file + //bytes, _ := json.MarshalIndent(enfPol, "", "\t") + //ioutil.WriteFile(function.Name+".json", bytes, 0644) + return pols +} + +func sub(a, b int) int { + return a - b +} diff --git a/rvdef/rv.go b/rvdef/rv.go new file mode 100644 index 0000000..1b5cce5 --- /dev/null +++ b/rvdef/rv.go @@ -0,0 +1,157 @@ +package rvdef + +import ( + "errors" + "strconv" + "strings" +) + +//An Monitor is what we're here for, it's what we're going to wrap with our policies! +type Monitor struct { + Name string `xml:"Name,attr"` + + InterfaceList + + Policies []Policy `xml:"Policy"` +} + +//InterfaceList stores the IO +type InterfaceList []Variable + +//HasIONamed will check a given InterfaceList to see if it has an output of that name +func (il InterfaceList) HasIONamed(input bool, s string) bool { + for i := 0; i < len(il); i++ { + if il[i].Name == s { + return true + } + } + return false +} + +//A Variable is used to store I/O or internal var data +type Variable struct { + Name string `xml:"Name,attr"` + Type string `xml:"Type,attr"` + Constant bool `xml:"Constant,attr"` + ArraySize string `xml:"ArraySize,attr,omitempty"` + InitialValue string `xml:"InitialValue,attr,omitempty"` + Comment string `xml:"Comment,attr"` +} + +//GetInitialArray returns a formatted initial array if there is one to do so +func (v Variable) GetInitialArray() []string { + //if cannot parse an array size then give up + _, err := strconv.Atoi(v.ArraySize) + if err != nil { + return nil + } + + //remove everything except commas and values + raw := v.InitialValue + raw = strings.TrimPrefix(raw, "[") + raw = strings.TrimSuffix(raw, "]") + + raws := strings.Split(raw, ",") + for i := 0; i < len(raws); i++ { + raws[i] = strings.Trim(raws[i], " ") + } + return raws +} + +//IsDTimer returns true if DTimer +func (v Variable) IsDTimer() bool { + return strings.ToLower(v.Type) == "dtimer_t" +} + +//Policy stores a policy, i.e. the vars that must be kept +type Policy struct { + Name string `xml:"Name,attr"` + InternalVars []Variable `xml:"InternalVars>VarDeclaration,omitempty"` + States []PState `xml:"Machine>PState"` + Transitions []PTransition `xml:"Machine>PTransition,omitempty"` +} + +//PState is a state in the policy specification of an enforcerFB +type PState struct { + Name string + Accepting bool +} + +//PTransition is a transition between PState in a Policy (mealy machine transitions) +type PTransition struct { + Source string + Destination string + Condition string + Expressions []PExpression //output expressions associated with this transition +} + +//PExpression is used to assign a var a value based on a PTransitions +type PExpression struct { + VarName string + Value string +} + +//NewMonitor creates a new Monitor struct +func NewMonitor(name string) Monitor { + return Monitor{Name: name} +} + +//AddIO adds the provided IO to a given Monitor, while checking to make sure that each name is unique in the interface +func (f *Monitor) AddIO(intNames []string, typ string, size string, initialValue string) error { + seenNames := make(map[string]bool) + for _, inp := range f.InterfaceList { + seenNames[inp.Name] = true + } + + vars := make([]Variable, len(intNames)) + for i, name := range intNames { + if seenNames[name] == true { + return errors.New("The name " + name + " is already in use") + } + seenNames[name] = true + vars[i] = Variable{ + Name: name, + Type: typ, + ArraySize: size, + InitialValue: initialValue, + } + } + + f.InterfaceList = append(f.InterfaceList, vars...) + return nil +} + +//AddPolicy adds a Policy to an Monitor +func (f *Monitor) AddPolicy(name string) { + f.Policies = append(f.Policies, Policy{Name: name}) +} + +//AddDataInternals adds data internals to a efb, and adds the InternalVars section if it is nil +func (efb *Policy) AddDataInternals(intNames []string, typ string, isConstant bool, size string, initialValue string) *Policy { + for _, iname := range intNames { + efb.InternalVars = append(efb.InternalVars, Variable{Name: iname, Type: typ, Constant: isConstant, ArraySize: size, InitialValue: initialValue}) + } + return efb +} + +//AddState adds a state to a bfb +func (efb *Policy) AddState(name string, accepting bool) error { + efb.States = append(efb.States, PState{Name: name, Accepting: accepting}) + return nil //TODO: add check (make sure name is unique) +} + +//AddTransition adds a state transition to a bfb +func (efb *Policy) AddTransition(source string, dest string, cond string, expressions []PExpression) error { + efb.Transitions = append(efb.Transitions, PTransition{ + Source: source, + Destination: dest, + Condition: cond, + Expressions: expressions, + }) + return nil //TODO: make sure [source] and [dest] can be found, make sure [cond] is valid, make sure [expressions] is valid +} + +type DebugInfo struct { + SourceLine int + SourceFile string +} diff --git a/rvdef/rvMonitor.go b/rvdef/rvMonitor.go new file mode 100644 index 0000000..aea403a --- /dev/null +++ b/rvdef/rvMonitor.go @@ -0,0 +1,290 @@ +package rvdef + +import ( + "fmt" + "reflect" + "strings" + + "github.com/PRETgroup/stcompilerlib" +) + +//FBECCGuardToSTExpression converts a given FB's guard into a STExpression parsetree +func FBECCGuardToSTExpression(pName, guard string) ([]stcompilerlib.STInstruction, *stcompilerlib.STParseError) { + return stcompilerlib.ParseString(pName, guard) +} + +//PSTTransition is a container struct for a PTransition and its ST translated guard +type PSTTransition struct { + PTransition + STGuard stcompilerlib.STExpression +} + +//A PMonitorPolicy is what goes inside a PMonitor, it is derived from a Policy +type PMonitorPolicy struct { + InternalVars []Variable + States []PState + Transitions []PSTTransition +} + +//GetDTimers returns all DTIMERS in a PMonitorPolicy +func (pol PMonitorPolicy) GetDTimers() []Variable { + dTimers := make([]Variable, 0) + for _, v := range pol.InternalVars { + if strings.ToLower(v.Type) == "dtimer_t" { + dTimers = append(dTimers, v) + } + } + return dTimers +} + +//GetTransitionsForSource returns a slice of all transitions in this PMonitorPolicy +//which have a source as "src" +func (pol PMonitorPolicy) GetTransitionsForSource(src string) []PSTTransition { + nTrans := make([]PSTTransition, 0) + for _, tr := range pol.Transitions { + if tr.Source == src { + nTrans = append(nTrans, tr) + } + } + return nTrans +} + +//DoesExpressionInvolveTime returns true if a given expression uses time +func (pol PMonitorPolicy) DoesExpressionInvolveTime(expr stcompilerlib.STExpression) bool { + op := expr.HasOperator() + if op == nil { + return VariablesContain(pol.GetDTimers(), expr.HasValue()) + } + for _, arg := range expr.GetArguments() { + if pol.DoesExpressionInvolveTime(arg) { + return true + } + } + return false +} + +//A PMonitor will store a given input and output policy and can derive the enforcers required to uphold them +type PMonitor struct { + interfaceList InterfaceList + Name string + Policy PMonitorPolicy +} + +//MakePMonitor will convert a given policy to an enforcer for that policy +func MakePMonitor(il InterfaceList, p Policy) (*PMonitor, error) { + //make the enforcer + enf := &PMonitor{interfaceList: il, Name: p.Name} + //first, convert policy transitions + outpTr, err := p.GetPSTTransitions() + if err != nil { + return nil, err + } + + enf.Policy = PMonitorPolicy{ + InternalVars: p.InternalVars, + States: p.States, + Transitions: outpTr, + } + + enf.Policy.RemoveNilTransitions() + enf.Policy.RemoveDuplicateTransitions() + + return enf, nil +} + +//RemoveNilTransitions will do a search through a policies transitions and remove any that have nil guards +func (pol *PMonitorPolicy) RemoveNilTransitions() { + for i := 0; i < len(pol.Transitions); i++ { + for j := i; j < len(pol.Transitions); j++ { + if pol.Transitions[j].STGuard == nil || pol.Transitions[j].Condition == "" || stcompilerlib.STCompileExpression(pol.Transitions[j].STGuard) == "" { + pol.Transitions = append(pol.Transitions[:j], pol.Transitions[j+1:]...) + j-- + } + } + } +} + +//RemoveDuplicateTransitions will do a search through a policies transitions and remove any that are simple duplicates +//(i.e. every field the same and in the same order). +func (pol *PMonitorPolicy) RemoveDuplicateTransitions() { + for i := 0; i < len(pol.Transitions); i++ { + for j := i + 1; j < len(pol.Transitions); j++ { + if reflect.DeepEqual(pol.Transitions[i], pol.Transitions[j]) { + pol.Transitions = append(pol.Transitions[:j], pol.Transitions[j+1:]...) + j-- + } + } + } +} + +//CURRENTLY UNUSED +//RemoveAlwaysTrueTransitions will do a search through a policies transitions and remove any that are just "true" +func (pol *PMonitorPolicy) RemoveAlwaysTrueTransitions() { + for i := 0; i < len(pol.Transitions); i++ { + for j := i; j < len(pol.Transitions); j++ { + if val := pol.Transitions[j].STGuard.HasValue(); val == "true" || val == "1" { + pol.Transitions = append(pol.Transitions[:j], pol.Transitions[j+1:]...) + j-- + } + } + } +} + +//VariablesContain returns true if a list of variables contains a given name +func VariablesContain(vars []Variable, name string) bool { + for i := 0; i < len(vars); i++ { + if vars[i].Name == name { + return true + } + } + return false +} + +func stringSliceContains(slice []string, str string) bool { + for _, s := range slice { + if s == str { + return true + } + } + return false +} + +//GetPSTTransitions will convert all internal PTransitions into PSTTransitions (i.e. PTransitions with a ST symbolic tree condition) +func (p *Policy) GetPSTTransitions() ([]PSTTransition, error) { + stTrans := make([]PSTTransition, len(p.Transitions)) + for i := 0; i < len(p.Transitions); i++ { + stguard, err := FBECCGuardToSTExpression(p.Name, p.Transitions[i].Condition) + if err != nil { + return nil, err + } + if len(stguard) != 1 { + return nil, fmt.Errorf("Incompatible policy guard (wrong number of expressions)") + } + expr, ok := stguard[0].(stcompilerlib.STExpression) + if !ok { + return nil, fmt.Errorf("Incompatible policy guard (not an expression)") + } + stTrans[i] = PSTTransition{ + PTransition: p.Transitions[i], + STGuard: expr, + } + } + return stTrans, nil +} + +//SplitExpressionsOnOr will take a given STExpression and return a slice of STExpressions which are +//split over the "or" operators, e.g. +//[a] should become [a] +//[or a b] should become [a] [b] +//[or a [b and c]] should become [a] [b and c] +//[[a or b] and [c or d]] should become [a and c] [a and d] [b and c] [b and d] +func SplitExpressionsOnOr(expr stcompilerlib.STExpression) []stcompilerlib.STExpression { + //IF IS OR + // BREAK APART + //IF IS VALUE + // RETURN CURRENT + //IF IS OTHER OPERATOR + // MARK LOCATION AND RECURSE + + // broken := breakIfOr(expr) + // if len(broken) == 1 { + // return broken + // } + + op := expr.HasOperator() + if op == nil { //if it's just a value, return + return []stcompilerlib.STExpression{expr} + } + if op.GetToken() == "or" { //if it's an "or", return the arguments + rets := make([]stcompilerlib.STExpression, 0) + args := expr.GetArguments() + for i := 0; i < len(args); i++ { //for each argument of the "or", return it, unless it is itself an "or" (in which case, expand further) + arg := args[i] + argOp := arg.HasOperator() + if argOp == nil || argOp.GetToken() != "or" { + rets = append(rets, arg) + continue + } + args = append(args, arg.GetArguments()...) + } + return rets + } + + //otherwise, things are more interesting + + //make the thing we're returning + rets := make([]stcompilerlib.STExpressionOperator, 0) + + //build a new expression + var nExpr stcompilerlib.STExpressionOperator + + //operator is op, arguments are args + nExpr.Operator = op + args := expr.GetArguments() + nExpr.Arguments = make([]stcompilerlib.STExpression, len(args)) + + rets = append(rets, nExpr) + //for each argument in the expression operator + for i, arg := range args { + //get arguments to operator by calling SplitExpressionsOnOr again + argT := SplitExpressionsOnOr(arg) + //if argT has more than one value, it indicates that this argument was "split", and we should return two nExpr, one with each argument + //we will increase the size of rets by a multiplyFactor, which is the size of argT + //i.e. if we receive two arguments, and we already had two elements in rets, it indicates we need to return 4 values + //for instance, if our original command was "(a or b) and (c or d)" we'd need to return 4 elements (a and c) (a and d) (b and c) (b and d) + multiplyFactor := len(argT) + //for each factor in multiplyFactor, duplicate rets[n] + //e.g. multiplyFactor 2 on [1 2 3] becomes [1 1 2 2 3 3] + //e.g. multiplyFactor 3 on [1 2 3] becomes [1 1 1 2 2 2 3 3 3] + for y := 0; y < len(rets); y++ { + for z := 1; z < multiplyFactor; z++ { + + var newElem stcompilerlib.STExpressionOperator + copyElem := rets[y] + newElem.Operator = copyElem.Operator + newElem.Arguments = make([]stcompilerlib.STExpression, len(copyElem.Arguments)) + copy(newElem.Arguments, copyElem.Arguments) + + rets = append(rets, stcompilerlib.STExpressionOperator{}) + copy(rets[y+1:], rets[y:]) + rets[y] = newElem + y++ + } + } + + //for each argument, copy it into the return elements at the appropriate locations + //(if we have multiple arguments, they will be chosen in a round-robin fashion) + for j := 0; j < len(argT); j++ { + at := argT[j] + for k := j; k < len(rets); k += len(argT) { + rets[k].Arguments[i] = at + } + } + + //expected, _ := json.MarshalIndent(rets, "\t", "\t") + //fmt.Printf("Current:\n\t%s\n\n", expected) + } + + //conversion for returning + actualRets := make([]stcompilerlib.STExpression, len(rets)) + for i := 0; i < len(rets); i++ { + actualRets[i] = rets[i] + } + return actualRets + +} + +//DeepGetValues recursively gets all values from a given stcompilerlib.STExpression +func DeepGetValues(expr stcompilerlib.STExpression) []string { + if expr == nil { + return nil + } + if val := expr.HasValue(); val != "" { + return []string{val} + } + vals := make([]string, 0) + for _, arg := range expr.GetArguments() { + vals = append(vals, DeepGetValues(arg)...) + } + return vals +} diff --git a/rvparser/main/main b/rvparser/main/main new file mode 100755 index 0000000..5bc72b4 Binary files /dev/null and b/rvparser/main/main differ diff --git a/rvparser/main/main.go b/rvparser/main/main.go new file mode 100644 index 0000000..8c05871 --- /dev/null +++ b/rvparser/main/main.go @@ -0,0 +1,130 @@ +package main + +import ( + "encoding/xml" + "flag" + "fmt" + "io/ioutil" + + "github.com/PRETgroup/easy-rte/rtedef" + + "github.com/PRETgroup/easy-rte/rteparser" +) + +var ( + inFileName = flag.String("i", "", "Specifies the name of the source file (.erte) file to be compiled.") + outFileName = flag.String("o", "out.xml", "Specifies the name of the output file (.erte.xml) files.") + policyProduct = flag.Bool("product", false, "(Experimental) Set this to true to take the product of all specified policies rather than executing them in sequence") +) + +var ( + xmlHeader = []byte(`` + "\n") +) + +var ( + inputExtension = "erte" + outputExtension = "xml" +) + +func main() { + flag.Parse() + + if *inFileName == "" { + fmt.Println("You need to specify a file or directory name to compile! Check out -help for options") + return + } + + // fileInfo, err := os.Stat(*inFileName) + // if err != nil { + // fmt.Println("Error reading file statistics:", err.Error()) + // return + // } + + // var fileNames []string + + // if fileInfo.IsDir() { + // //Running in Dir mode + // files, err := ioutil.ReadDir(*inFileName) + // if err != nil { + // log.Fatal(err) + // } + + // for _, file := range files { + // //only read the .tfb files + // name := file.Name() + // nameComponents := strings.Split(name, ".") + // extension := nameComponents[len(nameComponents)-1] + // if extension == inputExtension { + // fileNames = append(fileNames, name) + // } + // } + // } else { + // //Running in Single mode + // fileNames = append(fileNames, *inFileName) + // } + + // var funcs []rtedef.EnforcedFunction + + // for _, name := range fileNames { + // sourceFile, err := ioutil.ReadFile(fmt.Sprintf("%s%c%s", *inFileName, os.PathSeparator, name)) + // if err != nil { + // fmt.Printf("Error reading file '%s' for conversion: %s\n", name, err.Error()) + // return + // } + + // mfbs, parseErr := rteparser.ParseString(name, string(sourceFile)) + // if parseErr != nil { + // fmt.Printf("Error during parsing file '%s': %s\n", name, parseErr.Error()) + // return + // } + + // funcs = append(funcs, mfbs...) + + // } + + sourceFile, err := ioutil.ReadFile(*inFileName) + if err != nil { + fmt.Printf("Error reading file '%s' for conversion: %s\n", *inFileName, err.Error()) + return + } + mfbs, parseErr := rteparser.ParseString(*inFileName, string(sourceFile)) + if parseErr != nil { + fmt.Printf("Error during parsing file '%s': %s\n", *inFileName, parseErr.Error()) + return + } + for _, fun := range mfbs { + + if *policyProduct { + if len(fun.Policies) > 1 { + finalPolicy := fun.Policies[0] + for i := 1; i < len(fun.Policies); i++ { + finalPolicy, err = fun.PolicyProduct(finalPolicy, fun.Policies[i]) + if err != nil { + fmt.Printf("Error taking product of policies in '%s': %s\n", *inFileName, parseErr.Error()) + return + } + } + fun.Policies = []rtedef.Policy{finalPolicy} + } + } + + // name := fun.Name + // extn := outputExtension + //TODO: work out what extension to use based on the fb.XMLname field + bytes, err := xml.MarshalIndent(fun, "", "\t") + if err != nil { + fmt.Println("Error during marshal:", err.Error()) + return + } + //output := append(xmlHeader, fbTypeHeader...) + output := append(xmlHeader, bytes...) + + fmt.Printf("Writing to %s\n", *outFileName) + err = ioutil.WriteFile(*outFileName, output, 0644) + if err != nil { + fmt.Println("Error during file write:", err.Error()) + return + } + } + +} diff --git a/rvparser/parse.go b/rvparser/parse.go new file mode 100644 index 0000000..bd94c7f --- /dev/null +++ b/rvparser/parse.go @@ -0,0 +1,250 @@ +package rvparser + +import ( + "errors" + "strings" + "text/scanner" + + "github.com/PRETgroup/easy-rv/rvdef" +) + +const ( + pNewline = "\n" + + pMonitor = "monitor" + pInterface = "interface" + pArchitecture = "architecture" + + pOpenBrace = "{" + pCloseBrace = "}" + pOpenBracket = "[" + pCloseBracket = "]" + pComma = "," + pSemicolon = ";" + pColon = ":" + pInitEq = ":=" + pAssigment = ":=" + + pFBpolicy = "policy" + pOf = "of" + + pWith = "with" + + pTrans = "->" + pOn = "on" + + pConstant = "constant" + + pInternal = "internal" + pInternals = "internals" + pState = "state" + pStates = "states" + pAlgorithm = "algorithm" + pAlgorithms = "algorithms" + + pAccepting = "accepting" + pRejecting = "rejecting" + pTrap = "trap" +) + +//ParseString takes an input string (i.e. filename) and input and returns all FBs in that string +func ParseString(name string, input string) ([]rvdef.Monitor, *ParseError) { + //break up input string into all of its parts + items := scanString(name, input) + + //now parse the items + return parseItems(name, items) +} + +func scanString(name string, input string) []string { + var s scanner.Scanner + + s.Filename = name + s.Init(strings.NewReader(input)) + + //we don't want to ignore \n characters (we want to know what line we're on) + s.Whitespace = 1<<'\t' | 0<<'\n' | 1<<'\r' | 1<<' ' + //we don't want scanner.ScanChars + s.Mode = scanner.ScanIdents | scanner.ScanFloats | scanner.ScanStrings | scanner.ScanRawStrings | scanner.ScanComments | scanner.SkipComments + + //TODO: think about the scanner error function. Maybe we should provide one, that when an error occurs, halts scanning? + + var tok rune + var items []string + for tok != scanner.EOF { + tok = s.Scan() + items = append(items, s.TokenText()) + } + + //combine multi-character operators + for i := 0; i < len(items)-1; i++ { + if items[i] == "<" && items[i+1] == "-" { + items[i] = "<-" + items = append(items[:i+1], items[i+2:]...) + } + + if items[i] == "-" && items[i+1] == ">" { + items[i] = "->" + items = append(items[:i+1], items[i+2:]...) + } + + if items[i] == ":" && items[i+1] == "=" { + items[i] = ":=" + items = append(items[:i+1], items[i+2:]...) + } + + if items[i] == "=" && items[i+1] == "=" { + items[i] = "==" + items = append(items[:i+1], items[i+2:]...) + } + + if items[i] == ">" && items[i+1] == "=" { + items[i] = ">=" + items = append(items[:i+1], items[i+2:]...) + } + + if items[i] == "<" && items[i+1] == "=" { + items[i] = "<=" + items = append(items[:i+1], items[i+2:]...) + } + + if items[i] == "!" { + items[i] = "!" + items[i+1] + items = append(items[:i+1], items[i+2:]...) + } + + if items[i] == "&" && items[i+1] == "&" { + items[i] = "&&" + items = append(items[:i+1], items[i+2:]...) + } + + if items[i] == "|" && items[i+1] == "|" { + items[i] = "||" + items = append(items[:i+1], items[i+2:]...) + } + } + + return items +} + +//parseItems creates and runs a pparse struct +func parseItems(name string, items []string) ([]rvdef.Monitor, *ParseError) { + t := pParse{items: items, currentLine: 1, currentFile: name} + + for !t.done() { + s := t.pop() + if t.done() { + break + } + //have we defined a monitor name + if s == pMonitor { + if err := t.parseMonitor(s); err != nil { + return nil, err + } + continue + } + + //is this defining an interface for a monitor + if s == pInterface { + if err := t.parseMonitorInterface(); err != nil { + return nil, err + } + continue + } + + //is this defining an architecture for a monitor + if s == pArchitecture || s == pFBpolicy { + if err := t.parseMonitorArchitecture(s); err != nil { + return nil, err + } + continue + } + return nil, t.errorWithArg(ErrUnexpectedValue, s) + } + + return t.funcs, nil +} + +//isValidType returns true if string s is one of the valid event/data types +func isValidType(s string) bool { + s = strings.ToLower(s) + if s == "bool" || + s == "char" || + s == "uint8_t" || + s == "uint16_t" || + s == "uint32_t" || + s == "uint64_t" || + s == "int8_t" || + s == "int16_t" || + s == "int32_t" || + s == "int64_t" || + s == "float" || + s == "double" || + s == "dtimer_t" || + s == "rtimer_t" { + return true + } + return false +} + +//parseMonitor will create a new function and add it to the list of internal functions +func (t *pParse) parseMonitor(typ string) *ParseError { + var funcs []rvdef.Monitor + for { + name := t.pop() + if !t.isNameUnused(name) { + return t.errorWithArg(ErrNameAlreadyInUse, name) + } + + if typ == pMonitor { + funcs = append(funcs, rvdef.NewMonitor(name)) + } else { + return t.errorWithReason(ErrInternal, "I can't parse type "+typ) + } + + if t.peek() == pComma { + t.pop() //get rid of comma + continue + } + break + } + + s := t.pop() + if s != pSemicolon { + return t.errorUnexpectedWithExpected(s, pSemicolon) + } + + t.funcs = append(t.funcs, funcs...) + + return nil +} + +func (t *pParse) parseMonitorArchitecture(archType string) *ParseError { + var s string + var pName string + + //if this is a policy, the name is here + if archType == pFBpolicy { + s = t.pop() + pName = s + } + + //first word should be of + s = t.pop() + if s != pOf { + return t.errorUnexpectedWithExpected(s, pOf) + } + + //second word is fb name + s = t.pop() + fbIndex := t.getIndexFromName(s) + if fbIndex == -1 { + return t.errorWithArg(ErrUndefinedFunction, s) + } + + if archType == pFBpolicy { + t.funcs[fbIndex].AddPolicy(pName) + return t.parsePolicyArchitecture(fbIndex) + } + return t.error(errors.New("can't parse unknown architecture type")) +} diff --git a/rvparser/parseError.go b/rvparser/parseError.go new file mode 100644 index 0000000..a03208a --- /dev/null +++ b/rvparser/parseError.go @@ -0,0 +1,75 @@ +package rvparser + +import ( + "errors" + "fmt" +) + +var ( + //ErrInternal means something went wrong and it's the transpiler's fault + ErrInternal = errors.New("An internal error occured") + + //ErrUnexpectedEOF means the document ended unexpectedly + ErrUnexpectedEOF = errors.New("Unexpected EOF") + + //ErrUnexpectedValue is used to indicate a parsed value was not what was expected (i.e. a word instead of a semicolon) + ErrUnexpectedValue = errors.New("Unexpected value") + + //ErrUndefinedFunction is used to indicate a Function was referenced that can't be found (so probably a typo has occured) + ErrUndefinedFunction = errors.New("Can't find Function with name") + + //ErrInvalidType is used when the type of a data variable is bad + ErrInvalidType = errors.New("Invalid or missing data type") + + //ErrInvalidIOMeta is used when metadata for an I/O line is bad + ErrInvalidIOMeta = errors.New("Invalid metadata for data/event line") + + //ErrNameAlreadyInUse is returned whenever something is named but the name is already in use elsewhere + ErrNameAlreadyInUse = errors.New("This name is already defined elsewhere") +) + +//ParseError is used to contain a helpful error message when parsing fails +type ParseError struct { + LineNumber int + Argument string + Reason string + Err error +} + +//Error makes ParseError fulfill error interface +func (p ParseError) Error() string { + s := fmt.Sprintf("Error (Line %v): %s", p.LineNumber, p.Err.Error()) + if p.Argument != "" { + s += " '" + p.Argument + "'" + } + if p.Reason != "" { + s += ", (" + p.Reason + ")" + } + return s +} + +// helper functions to help construct helpful error messages + +func (t *pParse) errorWithArg(err error, arg string) *ParseError { + return &ParseError{LineNumber: t.currentLine, Argument: arg, Reason: "", Err: err} +} + +func (t *pParse) errorWithArgAndLineNumber(err error, arg string, line int) *ParseError { + return &ParseError{LineNumber: line, Argument: arg, Reason: "", Err: err} +} + +func (t *pParse) errorWithReason(err error, reason string) *ParseError { + return &ParseError{LineNumber: t.currentLine, Argument: "", Reason: reason, Err: err} +} + +func (t *pParse) error(err error) *ParseError { + return &ParseError{LineNumber: t.currentLine, Argument: "", Reason: "", Err: err} +} + +func (t *pParse) errorWithArgAndReason(err error, arg string, reason string) *ParseError { + return &ParseError{LineNumber: t.currentLine, Argument: arg, Reason: reason, Err: err} +} + +func (t *pParse) errorUnexpectedWithExpected(unexpected string, expected string) *ParseError { + return &ParseError{LineNumber: t.currentLine, Argument: unexpected, Reason: "Expected: " + expected, Err: ErrUnexpectedValue} +} diff --git a/rvparser/parseMonitorInterface.go b/rvparser/parseMonitorInterface.go new file mode 100644 index 0000000..fd6d29f --- /dev/null +++ b/rvparser/parseMonitorInterface.go @@ -0,0 +1,127 @@ +package rvparser + +//parseMonitorInterface will add an interface to an existing internal function +func (t *pParse) parseMonitorInterface() *ParseError { + var s string + //first word should be of + s = t.pop() + if s != pOf { + return t.errorUnexpectedWithExpected(s, pOf) + } + + //second word is fb name + s = t.pop() + fbIndex := t.getIndexFromName(s) + if fbIndex == -1 { + return t.errorWithArg(ErrUndefinedFunction, s) + } + + //third should be open brace + s = t.pop() + if s != pOpenBrace { + return t.errorUnexpectedWithExpected(s, pOpenBrace) + } + + //now we run until closed brace + for { + //inside the interface, we have + //[enforce] event|bool|byte|word|dword|lword|sint|usint|int|uint|dint|udint|lint|ulint|real|lreal|time|any (name[, name]) [on (name[, name]) - non-event types only]; //(comments) + //repeated over and over again + s = t.peek() + if s == "" { + return t.error(ErrUnexpectedEOF) + } + if s == pCloseBrace { + t.pop() + return nil //we're done here + } + //still here? attempt to add I/O + if err := t.addMonitorIO(fbIndex); err != nil { + return err + } + } +} + +//addMonitorIO adds a line of event/data [:= default] to the FB interface +// some error checking is done +//fbIndex: the index of the Function we are working on inside t +func (t *pParse) addMonitorIO(fbIndex int) *ParseError { + fb := &t.funcs[fbIndex] + + //next s is type + typ := t.pop() + if !isValidType(typ) { + return t.errorWithArgAndReason(ErrInvalidType, typ, "Expected valid type") + } + + var intNames []string + + //there might be an array size next + size := "" + if t.peek() == pOpenBracket { + t.pop() // get rid of open bracket + size = t.pop() + if s := t.peek(); s != pCloseBracket { + return t.errorUnexpectedWithExpected(s, pCloseBracket) + } + t.pop() //get rid of close bracket + } + + //this could be an array of names, so we'll loop while we are finding commas + for { + name := t.pop() + + intNames = append(intNames, name) + if t.peek() == pComma { + t.pop() //get rid of the pComma + continue + } + break + } + + //there might be a default value next + initialValue := "" + if t.peek() == pInitEq { + t.pop() //get rid of pInitial + + bracketOpen := 0 + for { + s := t.peek() + if s == "" { + return t.error(ErrUnexpectedEOF) + } + //deal with brackets, if we have an open bracket we must have a close bracket, etc + if s == pOpenBracket && bracketOpen == 0 { + bracketOpen = 1 + } else if s == pOpenBracket && bracketOpen != 0 { + return t.errorUnexpectedWithExpected(s, "[Value]") + } + if s == pCloseBracket && bracketOpen == 1 { + bracketOpen = 2 + } else if s == pCloseBracket && bracketOpen != 1 { + return t.errorUnexpectedWithExpected(s, pSemicolon) + } + if s == pSemicolon && bracketOpen == 1 { //can't return if brackets are open + return t.errorUnexpectedWithExpected(s, pCloseBracket) + } + if s == pSemicolon { + break + } + initialValue += s + t.pop() //pop whatever we were just peeking at + } + } + + //clear out last semicolon + if s := t.pop(); s != pSemicolon { + return t.errorUnexpectedWithExpected(s, pSemicolon) + } + + //we now have everything we need to add the io to the interface + + if err := fb.AddIO(intNames, typ, size, initialValue); err != nil { + return t.errorWithArg(ErrNameAlreadyInUse, err.Error()) + } + + return nil +} diff --git a/rvparser/parseMonitorInterface_test.go b/rvparser/parseMonitorInterface_test.go new file mode 100644 index 0000000..049c432 --- /dev/null +++ b/rvparser/parseMonitorInterface_test.go @@ -0,0 +1,130 @@ +package rvparser + +import ( + "testing" + + "github.com/PRETgroup/easy-rv/rvdef" +) + +var interfaceTests = []ParseTest{ + + { + Name: "events typo 1", + Input: `monitor testBlock; + interface of testBlock { + bool inEvent; + outEvent; + }`, + Err: ErrInvalidType, + }, + { + Name: "events typo 2", + Input: `monitor testBlock; + interface of testBlock { + bool inEvent; + bool outEvent + }`, + Err: ErrUnexpectedValue, + }, + { + Name: "data typo 1", + Input: `monitor testBlock; + interface of testBlock { + bool inEvent; + asdasd inData; + bool outEvent; + }`, + Err: ErrInvalidType, + }, + { + Name: "data input 1", + Input: `monitor testBlock; + interface of testBlock { + bool inEvent; + bool outEvent; + }`, + Output: []rvdef.Monitor{ + rvdef.Monitor{ + Name: "testBlock", + InterfaceList: []rvdef.Variable{ + rvdef.Variable{Name: "inEvent", Type: "bool", ArraySize: "", InitialValue: "", Comment: ""}, + rvdef.Variable{Name: "outEvent", Type: "bool", ArraySize: "", InitialValue: "", Comment: ""}, + }, + Policies: []rvdef.Policy(nil)}, + }, + Err: nil, + }, + { + Name: "data input 2", + Input: `monitor testBlock; + interface of testBlock { + bool inEvent; + bool[3] inData; + bool outEvent; + }`, + Output: []rvdef.Monitor{ + rvdef.Monitor{ + Name: "testBlock", + InterfaceList: []rvdef.Variable{ + rvdef.Variable{Name: "inEvent", Type: "bool", ArraySize: "", InitialValue: "", Comment: ""}, + rvdef.Variable{Name: "inData", Type: "bool", ArraySize: "3", InitialValue: "", Comment: ""}, + rvdef.Variable{Name: "outEvent", Type: "bool", ArraySize: "", InitialValue: "", Comment: ""}, + }, + Policies: []rvdef.Policy(nil), + }, + }, + Err: nil, + }, + { + Name: "data input array typo 1", + Input: `basicFB testBlock; + interface of testBlock { + event inEvent; + bool[3 inData; + event outEvent; + }`, + Err: ErrUnexpectedValue, + }, + { + Name: "data input 3", + Input: `monitor testBlock; + interface of testBlock { + int8_t inEvent; + bool[3] inData := [0,1,0]; + char outEvent; + }`, + Output: []rvdef.Monitor{ + rvdef.Monitor{ + Name: "testBlock", + InterfaceList: rvdef.InterfaceList{ + rvdef.Variable{Name: "inEvent", Type: "int8_t", ArraySize: "", InitialValue: "", Comment: ""}, + rvdef.Variable{Name: "inData", Type: "bool", ArraySize: "3", InitialValue: "[0,1,0]", Comment: ""}, + rvdef.Variable{Name: "outEvent", Type: "char", ArraySize: "", InitialValue: "", Comment: ""}, + }, + Policies: []rvdef.Policy(nil)}}, + Err: nil, + }, + { + Name: "data default typo 1", + Input: `basicFB testBlock; + interface of testBlock { + bool inEvent; + bool[3] inData := 0,1,0; + bool outEvent; + }`, + Err: ErrUnexpectedValue, + }, + { + Name: "Unexpected EOF", + Input: `basicFB testBlock; + interface of testBlock { + bool inEvent; + bool inEvent2; + int32_t `, + Err: ErrUnexpectedValue, + }, +} + +func TestParseStringInterface(t *testing.T) { + runParseTests(t, interfaceTests) +} diff --git a/rvparser/parsePolicyArchitecture.go b/rvparser/parsePolicyArchitecture.go new file mode 100644 index 0000000..380ce3b --- /dev/null +++ b/rvparser/parsePolicyArchitecture.go @@ -0,0 +1,311 @@ +package rvparser + +import ( + "strings" + + "github.com/PRETgroup/easy-rv/rvdef" +) + +//parsePolicyArchitecture shall only be called once we have already parsed the +// "architecture of [blockname]" part of the definition +// so, we are up to the brace +func (t *pParse) parsePolicyArchitecture(fbIndex int) *ParseError { + if s := t.pop(); s != pOpenBrace { + return t.errorUnexpectedWithExpected(s, pOpenBrace) + } + //we now have several things that could be in here + //internal | internals | state | states | closeBrace + + //unlike in an interface, the various things that are in an architecture can be presented out of order + //this only has consequences with regards to states in the state machine + //because we can't verify them "on-the-fly" (a state might point to a state we've not yet parsed) + //Situations like this is the main reason most non-syntax parse-related validation is done in the iec61499 package + + for { + s := t.pop() + if s == "" { + return t.error(ErrUnexpectedEOF) + } else if s == pCloseBrace { + //this is the end of the architecture + break + } else if s == pInternal || s == pInternals { //we actually care about { vs not-{, and so either internal or internals are valid prefixes for both situations + if err := t.parsePossibleArrayInto(fbIndex, (*pParse).parsePInternal); err != nil { + return err + } + } else if s == pState || s == pStates { + if err := t.parsePossibleArrayInto(fbIndex, (*pParse).parsePState); err != nil { + return err + } + } + } + + return nil +} + +//parsePossibleArrayInto will parse either a single item or an array of items into a single-item function +func (t *pParse) parsePossibleArrayInto(fbIndex int, singleFn func(*pParse, int) *ParseError) *ParseError { + + //if the next argument is a brace, we are going to be looping and creating many singles + s := t.peek() + if s == pOpenBrace { + t.pop() //get rid of the open brace + for { + if err := singleFn(t, fbIndex); err != nil { + return err + } + if s := t.peek(); s == pCloseBrace { + t.pop() //get rid of the close brace + break + } + } + return nil + } + + return singleFn(t, fbIndex) +} + +//parsePInternal parses a single internal and adds it to fb identified by fbIndex +func (t *pParse) parsePInternal(fbIndex int) *ParseError { + //the beginning of this is very similar to parseFBio, but different enough that it should be another function + fb := &t.funcs[fbIndex] + + //check if it is constant + isConstant := false + if t.peek() == pConstant { + isConstant = true + t.pop() + } + + //next s is type + typ := t.pop() + + if !isValidType(typ) { + return t.errorWithArgAndReason(ErrInvalidType, typ, "Expected valid type") + } + + var intNames []string + + //there might be an array size next + size := "" + if t.peek() == pOpenBracket { + t.pop() // get rid of open bracket + size = t.pop() + if s := t.peek(); s != pCloseBracket { + return t.errorUnexpectedWithExpected(s, pCloseBracket) + } + t.pop() //get rid of close bracket + } + + for { + name := t.pop() + + intNames = append(intNames, name) + if t.peek() == pComma { + t.pop() //get rid of the pComma + continue + } + if t.peek() == pInitEq { + break + } + break + } + + //there might be a default value next + initialValue := "" + if t.peek() == pInitEq { + t.pop() //get rid of pInitial + + bracketOpen := 0 + for { + s := t.peek() + if s == "" { + return t.error(ErrUnexpectedEOF) + } + //deal with brackets, if we have an open bracket we must have a close bracket, etc + if s == pOpenBracket && bracketOpen == 0 { + bracketOpen = 1 + } + if s == pOpenBracket && bracketOpen != 0 { + return t.errorUnexpectedWithExpected(s, "[Value]") + } + if s == pCloseBracket && bracketOpen == 1 { + bracketOpen = 2 + } + if s == pCloseBracket && bracketOpen != 1 { + return t.errorUnexpectedWithExpected(s, pSemicolon) + } + if s == pSemicolon && bracketOpen == 1 { //can't return if brackets are open + return t.errorUnexpectedWithExpected(s, pCloseBracket) + } + if s == pSemicolon { + break + } + initialValue += s + t.pop() //pop whatever we were just peeking at + } + } + + //clear out last semicolon + if s := t.pop(); s != pSemicolon { + return t.errorUnexpectedWithExpected(s, pSemicolon) + } + + //we now have everything we need to add the internal to the fb + + fb.Policies[len(fb.Policies)-1].AddDataInternals(intNames, typ, isConstant, size, initialValue) + + return nil +} + +//parsePState parses a single state and adds it to fb identified by fbIndex +// most things in this function are validated later in the iec61499 package +func (t *pParse) parsePState(fbIndex int) *ParseError { + fb := &t.funcs[fbIndex] + + //next is name of state + name := t.pop() + + for _, st := range fb.Policies[len(fb.Policies)-1].States { + if st.Name == name { + return t.errorWithArg(ErrNameAlreadyInUse, name) + } + } + + //next should be either "accepting" or "rejecting" + accepting := true + status := t.pop() + if status == pRejecting { + accepting = false + } else if status != pAccepting { + return t.errorUnexpectedWithExpected(status, "Either '"+pAccepting+"' or '"+pRejecting+"'") + } + + //next should either be "trap" or be an open brace + trap := false + s := t.pop() + if s == pTrap { + trap = true + //clear the last semicolon + if t.peek() != pSemicolon { + return t.errorUnexpectedWithExpected(t.peek(), pSemicolon) + } + t.pop() //pop the pSemicolon + } else if s != pOpenBrace { + return t.errorUnexpectedWithExpected(s, "Either '"+pTrap+"' or '"+pOpenBrace+"'") + } + + //now we have an unknown number of ->s + // format is + // -> [on guard] [: output expression][, output expression...] ; + // for transitions, or, + // enforce [expression][, expression...] on [guard] + if !trap { + for { + var expressions []rvdef.PExpression + var expressionComponents []string + var expressionVar string + s := t.pop() + + if s == "" { + return t.error(ErrUnexpectedEOF) + } + if s == pCloseBrace { + break + } + + if s == pTrans { + + //next is dest state + destState := t.pop() + + var condComponents []string + //next is on if we have a condition + if t.peek() == pOn { + t.pop() //clear the pOn + + //now we have an unknown number of condition components, terminated by a semicolon + for { + //pColon means that there are EXPRESSIONS that follow, but we're done here + //pSemicolon means that there is NOTHING that follows, and we're done here + if t.peek() == pColon || t.peek() == pSemicolon { + break + } + + s = t.pop() + if s == "" { + return t.error(ErrUnexpectedEOF) + } + + //if any condComponent is "&&" then turn it into and + if s == "&&" { + s = "and" + } + //if any condComponint is "||" then turn it into or + if s == "||" { + s = "or" + } + condComponents = append(condComponents, s) + + } + } + if len(condComponents) == 0 { //put in a default condition if no condition exists + condComponents = append(condComponents, "true") + } + + //if we broke on a colon then we now have EXPRESSIONS to parse + if t.peek() == pColon { + t.pop() //clear the pColon + //the format is + // VARIABLE := EXPRESSION [, VARIABLE := EXPRESSION] + expressionVar = "" + for { + if t.peek() == pSemicolon || t.peek() == pComma { + //finish the previous expression (if possible, indicated by expressionVar) and start the next one (if available, indicated by a comma) + if expressionVar != "" { + expressions = append(expressions, rvdef.PExpression{ + VarName: expressionVar, + Value: strings.Join(expressionComponents, " "), + }) + expressionComponents = make([]string, 0) //reset expressions + } + expressionVar = "" + + if t.peek() == pComma { + t.pop() + continue + } + break + } + s = t.pop() + if s == "" { + return t.error(ErrUnexpectedEOF) + } + //we already dealt with case where it's a comma or a semicolon in the peek section above + if expressionVar == "" { //we've not yet started the expression, so here's the "VARIABLE :=" part + expressionVar = s + s = t.pop() + if s != pAssigment { + return t.errorUnexpectedWithExpected(s, pAssigment) + } + continue + } else { + //now here's the condition components + expressionComponents = append(expressionComponents, s) + } + } + } + + if t.peek() != pSemicolon { + return t.errorUnexpectedWithExpected(t.peek(), pSemicolon) + } + t.pop() //pop the pSemicolon + //save the transition + fb.Policies[len(fb.Policies)-1].AddTransition(name, destState, strings.Join(condComponents, " "), expressions) + } + } + } + //everything is parsed, add it to the state machine + fb.Policies[len(fb.Policies)-1].AddState(name, accepting) + + return nil +} diff --git a/rvparser/parsePolicyArchitecture_test.go b/rvparser/parsePolicyArchitecture_test.go new file mode 100644 index 0000000..ca2a954 --- /dev/null +++ b/rvparser/parsePolicyArchitecture_test.go @@ -0,0 +1,164 @@ +package rvparser + +import ( + "testing" + + "github.com/PRETgroup/easy-rv/rvdef" +) + +var efbArchitectureTests = []ParseTest{ + { + Name: "missing brace after s1", + Input: `monitor testBlock; + interface of testBlock{ + } + policy of testBlock { + states { + s1 + + } + }`, + Err: ErrUnexpectedValue, + }, + { + Name: "AEIPolicy", + Input: `monitor AEIPolicy; + interface of AEIPolicy { + bool AS, VS; //in here means that they're going from PLANT to CONTROLLER + bool AP, VP;//out here means that they're going from CONTROLLER to PLANT + + uint64_t AEI_ns := 900000000; + } + policy AEI of AEIPolicy { + internals { + dtimer_t tAEI; //DTIMER increases in DISCRETE TIME continuously + } + + //P3: AS or AP must be true within AEI after a ventricular event VS or VP. + + states { + s1 accepting { + //-> [on guard] [: output expression][, output expression...] ; + -> s2 on (VS or VP): tAEI := 0; + } + + s2 rejecting { + -> s1 on (AS or AP); + -> violation on (tAEI > AEI_ns); + } + + violation rejecting trap; + } + }`, + Output: []rvdef.Monitor{ + rvdef.Monitor{ + Name: "AEIPolicy", + InterfaceList: []rvdef.Variable{ + rvdef.Variable{Name: "AS", Type: "bool", ArraySize: "", InitialValue: "", Comment: ""}, + rvdef.Variable{Name: "VS", Type: "bool", ArraySize: "", InitialValue: "", Comment: ""}, + rvdef.Variable{Name: "AP", Type: "bool", ArraySize: "", InitialValue: "", Comment: ""}, + rvdef.Variable{Name: "VP", Type: "bool", ArraySize: "", InitialValue: "", Comment: ""}, + rvdef.Variable{Name: "AEI_ns", Type: "uint64_t", ArraySize: "", InitialValue: "900000000", Comment: ""}, + }, + Policies: []rvdef.Policy{ + rvdef.Policy{ + Name: "AEI", + InternalVars: []rvdef.Variable{ + rvdef.Variable{Name: "tAEI", Type: "dtimer_t", ArraySize: "", InitialValue: "", Comment: ""}, + }, + States: []rvdef.PState{{Name: "s1", Accepting: true}, {Name: "s2", Accepting: false}, {Name: "violation", Accepting: false}}, + Transitions: []rvdef.PTransition{ + rvdef.PTransition{Source: "s1", Destination: "s2", Condition: "( VS or VP )", Expressions: []rvdef.PExpression{rvdef.PExpression{VarName: "tAEI", Value: "0"}}}, + rvdef.PTransition{Source: "s2", Destination: "s1", Condition: "( AS or AP )", Expressions: []rvdef.PExpression(nil)}, + rvdef.PTransition{Source: "s2", Destination: "violation", Condition: "( tAEI > AEI_ns )", Expressions: []rvdef.PExpression(nil)}, + }, + }, + }, + }, + }, + }, + { + Name: "AB5Policy", + Input: `monitor ab5; + interface of ab5 { + bool A; + bool B; + } + + policy AB5 of ab5 { + internals { + dtimer_t v; + } + + states { + + //first state is initial, and represents "We're waiting for an A" + s0 accepting { + //if we receive neither A nor B, do nothing + -> s0 on (!A and !B): v := 0; + + //if we receive an A only, head to state s1 + -> s1 on (A and !B): v := 0; + + //if we receive a !A and B then VIOLATION + -> violation on (!A and B); + + //if we receive both A and B then done + -> done on (A and B); + } + + //s1 is "we're waiting for a B, and it needs to get here within 5 ticks" + s1 rejecting { + //if we receive nothing, and we aren't over-time, then we do nothing + -> s1 on (!A and !B and v < 5); + + //if we receive a B only, head to state s0 + -> s0 on (!A and B); + + //if we go overtime, or we receive another A, then VIOLATION + -> violation on ((v >= 5) or (A and B) or (A and !B)); + } + + done accepting trap; + + violation rejecting trap; + } + }`, + Output: []rvdef.Monitor{ + rvdef.Monitor{ + Name: "ab5", + InterfaceList: []rvdef.Variable{ + rvdef.Variable{Name: "A", Type: "bool", ArraySize: "", InitialValue: "", Comment: ""}, + rvdef.Variable{Name: "B", Type: "bool", ArraySize: "", InitialValue: "", Comment: ""}, + }, + Policies: []rvdef.Policy{ + rvdef.Policy{ + Name: "AB5", + InternalVars: []rvdef.Variable{ + rvdef.Variable{Name: "v", Type: "dtimer_t", ArraySize: "", InitialValue: "", Comment: ""}, + }, + States: []rvdef.PState{ + rvdef.PState{Name: "s0", Accepting: true}, + rvdef.PState{Name: "s1", Accepting: false}, + rvdef.PState{Name: "done", Accepting: true}, + rvdef.PState{Name: "violation", Accepting: false}, + }, + Transitions: []rvdef.PTransition{ + rvdef.PTransition{Source: "s0", Destination: "s0", Condition: "( !A and !B )", Expressions: []rvdef.PExpression{rvdef.PExpression{VarName: "v", Value: "0"}}}, + rvdef.PTransition{Source: "s0", Destination: "s1", Condition: "( A and !B )", Expressions: []rvdef.PExpression{rvdef.PExpression{VarName: "v", Value: "0"}}}, + rvdef.PTransition{Source: "s0", Destination: "violation", Condition: "( !A and B )", Expressions: []rvdef.PExpression(nil)}, + rvdef.PTransition{Source: "s0", Destination: "done", Condition: "( A and B )", Expressions: []rvdef.PExpression(nil)}, + rvdef.PTransition{Source: "s1", Destination: "s1", Condition: "( !A and !B and v < 5 )", Expressions: []rvdef.PExpression(nil)}, + rvdef.PTransition{Source: "s1", Destination: "s0", Condition: "( !A and B )", Expressions: []rvdef.PExpression(nil)}, + rvdef.PTransition{Source: "s1", Destination: "violation", Condition: "( ( v >= 5 ) or ( A and B ) or ( A and !B ) )", Expressions: []rvdef.PExpression(nil)}, + }, + }, + }, + }, + }, + }, +} + +func TestParsePFBArchitecture(t *testing.T) { + runParseTests(t, efbArchitectureTests) +} diff --git a/rvparser/parse_test.go b/rvparser/parse_test.go new file mode 100644 index 0000000..49043f9 --- /dev/null +++ b/rvparser/parse_test.go @@ -0,0 +1,147 @@ +package rvparser + +import ( + "encoding/json" + "fmt" + "io/ioutil" + "reflect" + "testing" + + "github.com/PRETgroup/easy-rv/rvdef" +) + +type ParseTest struct { + Name string + Input string + Output []rvdef.Monitor //if applicable + Err error //if applicable +} + +var basicTests = []ParseTest{ + { + Name: "simple typo 1", + Input: `monitor testBlock; + interface of asdasd {}`, + Err: ErrUndefinedFunction, + }, + { + Name: "simple typo 2", + Input: `dadasdasd`, + Err: ErrUnexpectedValue, + }, + { + Name: "simple typo 3", + Input: `monitor testBlock1, , testBlock3; + interface of testBlock2 {}`, + Err: ErrUnexpectedValue, + }, + { + Name: "simple typo 4", + Input: `monitor testBlock1, testBlock2; + interface of testBlock2;`, + Err: ErrUnexpectedValue, + }, + { + Name: "simple typo 5", + Input: `monitor testBlock1, testBlock2; + interface of testBlock2 {`, + Err: ErrUnexpectedEOF, + }, + { + Name: "simple typo 6", + Input: `monitor testBlock1, testBlock2; + interface of testBlock2 {} + policy AB of testBlock2 {`, + Err: ErrUnexpectedEOF, + }, + { + Name: "simple typo 7", + Input: `monitor testBlock1; + policy AB of asdasd {}`, + Err: ErrUndefinedFunction, + }, + { + Name: "simple typo 8", + Input: `monitor testBlock1, testBlock2; + architecture testBlock2 {}`, + Err: ErrUnexpectedValue, + }, + { + Name: "missing word 1", + Input: `monitor testBlock1; + interface testBlock1 {}`, + Err: ErrUnexpectedValue, + }, + { + Name: "empty interface 1", + Input: `monitor testBlock; + interface of testBlock {}`, + Output: []rvdef.Monitor{ + rvdef.Monitor{ + Name: "testBlock", + InterfaceList: []rvdef.Variable(nil), + Policies: []rvdef.Policy(nil), + }, + }, + Err: nil, + }, + { + Name: "empty interfaces 1", + Input: `monitor testBlock1, testBlock2, testBlock3; + interface of testBlock2 {}`, + Output: []rvdef.Monitor{ + rvdef.Monitor{ + Name: "testBlock1", + InterfaceList: []rvdef.Variable(nil), + Policies: []rvdef.Policy(nil), + }, + rvdef.Monitor{ + Name: "testBlock2", + InterfaceList: []rvdef.Variable(nil), + Policies: []rvdef.Policy(nil), + }, + rvdef.Monitor{ + Name: "testBlock3", + InterfaceList: []rvdef.Variable(nil), + Policies: []rvdef.Policy(nil), + }, + }, + Err: nil, + }, +} + +func runParseTests(t *testing.T, pTests []ParseTest) { + for i, test := range pTests { + out, err := ParseString(fmt.Sprintf("Test[%d]", i), test.Input) + if err != nil && test.Err == nil { + t.Errorf("Test[%d](%s): Error '%s' occurred when it shouldn't have", i, test.Name, err.Error()) + } else if err == nil && test.Err != nil { + t.Errorf("Test[%d](%s): Error didn't occur and it should have been '%s'", i, test.Name, test.Err.Error()) + } else if err != nil && test.Err != nil { + if err.Err.Error() != test.Err.Error() { + t.Errorf("Test[%d](%s): Error codes don't match (it was '%s', should have been '%s')", i, test.Name, err.Error(), test.Err.Error()) + } + } else if err == nil && test.Err == nil { + if !reflect.DeepEqual(out, test.Output) { + t.Errorf("Test[%d](%s): Outputs don't match!", i, test.Name) + + bytes, _ := json.MarshalIndent(test.Output, "", "\t") + //fmt.Printf("\n\nDesired:\n%s", bytes) + ioutil.WriteFile("test_desired.out.json", bytes, 0644) + + bytes, _ = json.MarshalIndent(out, "", "\t") + ioutil.WriteFile("test_actual.out.json", bytes, 0644) + + goString := fmt.Sprintf("%#v", out) + ioutil.WriteFile("test_actual.out.govar", []byte(goString), 0644) + + } + + } + + } +} + +func TestParseBasics(t *testing.T) { + runParseTests(t, basicTests) +} diff --git a/rvparser/pparse.go b/rvparser/pparse.go new file mode 100644 index 0000000..73d6dba --- /dev/null +++ b/rvparser/pparse.go @@ -0,0 +1,80 @@ +package rvparser + +import ( + "github.com/PRETgroup/easy-rv/rvdef" +) + +//pParse is the containing struct for the parsing code +type pParse struct { + funcs []rvdef.Monitor + + items []string + itemIndex int + + currentLine int + currentFile string +} + +//getCurrentDebugInfo returns the debug info for the last popped item +func (t *pParse) getCurrentDebugInfo() rvdef.DebugInfo { + return rvdef.DebugInfo{ + SourceLine: t.currentLine, + SourceFile: t.currentFile, + } +} + +//isNameUnused will check all registered functions to see if a name can be used (as they need to be unique) +func (t *pParse) isNameUnused(name string) bool { + for i := 0; i < len(t.funcs); i++ { + if t.funcs[i].Name == name { + return false + } + } + return true +} + +//pop gets the current element of the pParse internal items slice +// and increments the index +func (t *pParse) pop() string { + if t.done() { + return "" + } + s := t.items[t.itemIndex] + t.itemIndex++ + + if s == pNewline { + t.currentLine++ + return t.pop() + } + return s +} + +//peek gets the current element of the pParse internal items slice (or the next non-newline character) +// without incrementing the index +func (t *pParse) peek() string { + if t.done() { + return "" + } + for i := 0; i < len(t.items); i++ { + if t.items[t.itemIndex+i] != pNewline { + return t.items[t.itemIndex+i] + } + } + return "" +} + +//done checks to see if the pParse is completed (i.e. nothing left to parse) +func (t *pParse) done() bool { + return t.itemIndex >= len(t.items) +} + +//getIndexFromName will search the pParse slice of FBs for one that matches +// the provided name and return the index if found +func (t *pParse) getIndexFromName(name string) int { + for i := 0; i < len(t.funcs); i++ { + if t.funcs[i].Name == name { + return i + } + } + return -1 +}