Project

General

Profile

« Previous | Next » 

Revision dbc69edc

Added by Corentin Lauverjat over 1 year ago

  • ID dbc69edc9425c1b5f291583739fb0d7c3401a8c5
  • Parent 8c36178f

Passage à dune

View differences:

.dockerignore
1
.git
2
bin
.gitignore
1 1
*~
2
/src/_build/
2
_build/
3 3
/setup.data
4 4
/setup.log
5 5
/src/version.ml
6 6
/src/pluginList.ml
7 7
/myocamlbuild.ml
8 8
*.cmt
9
*.log
10
Makefile
11
/configure
12
/src/_tags
13
/bin
14
*cache/
15
/config.status
9
*.log
.merlin
1
S src
2
S src/backends
3
S src/backends/C
4
S src/backends/EMF
5
S src/backends/Horn
6
S src/backends/Java
7
S src/checks
8
S src/features
9
S src/features/machine_types
10
S src/parsers
11
S src/plugins
12
S src/plugins/mpfr
13
S src/plugins/salsa
14
S src/plugins/scopes
15
S src/tools
16
S src/tools/stateflow
17
S src/tools/stateflow/common
18
S src/tools/stateflow/json-parser
19
S src/tools/stateflow/models
20
S src/tools/stateflow/semantics
21
S src/utils
22

  
23
B src/_build
24
B src/_build/backends
25
B src/_build/backends/C
26
B src/_build/backends/EMF
27
B src/_build/backends/Horn
28
B src/_build/checks
29
B src/_build/features
30
B src/_build/features/machine_types
31
B src/_build/parsers
32
B src/_build/plugins
33
B src/_build/plugins/mpfr
34
B src/_build/plugins/salsa
35
B src/_build/plugins/scopes
36
B src/_build/tools
37
B src/_build/tools/stateflow
38
B src/_build/tools/stateflow/common
39
B src/_build/tools/stateflow/models
40
B src/_build/tools/stateflow/semantics
41
B src/_build/utils
42

  
43
B test
.ocaml-config.sh
1
#!/bin/sh
2
case "$OCAML_VERSION,$OPAM_VERSION" in
3
    4.01.0,1.1.0) ppa=avsm/ocaml41+opam11 ;;
4
    4.01.0,1.2.0) ppa=avsm/ocaml41+opam12 ;;
5
    4.02.1,1.1.0) ppa=avsm/ocaml42+opam11 ;;
6
    4.02.1,1.2.0) ppa=avsm/ocaml42+opam12 ;;
7
    *) echo Unknown $OCAML_VERSION,$OPAM_VERSION; exit 1 ;;
8
esac
9

  
10
echo "\n" | add-apt-repository ppa:$ppa
Dockerfile
1
FROM alpine:3.12 
2
# AS builder
3

  
4
RUN apk add --no-cache make m4 patch git pkgconfig libc-dev gcc \ 
5
    ocaml ocaml-compiler-libs ocaml-ocamldoc opam ocaml-findlib mpfr-dev \ 
6
    gmp-dev autoconf
7

  
8
# Configuration de OPAM
9
RUN opam init --auto-setup -y --disable-sandboxing && \
10
    eval $(opam config env)
11

  
12
# Installation de Z3 avec les bindings OCaml
13
RUN apk add perl python2 g++ &&  \
14
    opam install -y z3 && \
15
    opam clean
16

  
17
# Installation des autres dépendences projet
18
RUN opam install -y ocamlbuild depext ocamlgraph mlmpfr num cmdliner \
19
    fmt logs yojson menhir && \
20
    opam clean
21

  
22
# Copie des sources
23
COPY . /var/lustrec
24

  
25
WORKDIR /var/lustrec 
26

  
27
# Build
28
RUN eval $(opam env) && \
29
    autoconf && \
30
    ./configure && \
31
    make lustrec lustret && \
32
    mkdir -p /usr/local/include/lustrec && \
33
    ln include/*.h /usr/local/include/lustrec
34

  
35

  
36
#FROM alpine:3.12 
37
#
38
## GMP linking is dynamic
39
#RUN apk add --no-cache gmp-dev
40
#
41
## Copy header files needed for running LustreC
42
#COPY --from=builder /var/lustrec/include/*.h /usr/local/include/lustrec/
43
## Copy Lustrec binaries
44
#COPY --from=builder /var/lustrec/bin /lustrec/
45
#
46
#
47
#WORKDIR /lustrec
INSTALL
1
On Mac
2
brew install autoconf opam cmake
3
Download ada from https://www.adacore.com/download
4

  
5

  
6
Then
7
opam install ocamlfind ocamlgraph cmdliner fmt logs dune num yojson 
8

  
9

  
10

  
11
For the ADA backend:
12
- GNAT 2018 community edition on https://www.adacore.com/download
13
- gprbuild shall be in your path
Makefile-lustresf.in
1
lustresf:
2
	@echo Compiling binary lustresf
3
	@make -C src lustresf
4

  
5
json-parser:
6
	@echo Compiling binary json-parser
7
	@make -C src json-parser
Makefile.in
1
prefix=@prefix@
2
exec_prefix=@exec_prefix@
3
bindir=@bindir@
4
datarootdir = ${prefix}/share
5
includedir = ${prefix}/include
6

  
7
LUSI_LIBS=include/lustrec_math.lusi include/simulink_math_fcn.lusi include/conv.lusi
8
LUSI_MPFR_LIB=include/mpfr_lustre.lusi
9
LOCAL_BINDIR=bin
10
LOCAL_DOCDIR=doc/manual
11
BIN_TARGETS = lustrec lustret lustrev @lustresf_target@
12

  
13
DEFAULT_TEST_TARGET=COMPIL_LUS\|MAKE\|BIN\|DIFF
14
DEFAULT_EXCLUDE_TEST=LUSTRET
15

  
16
all: $(BIN_TARGETS)
17

  
18
lustrec:
19
	@echo Compiling binary lustrec
20
	@make -C src lustrec
21

  
22
lustret:
23
	@echo Compiling binary lustret
24
	@make -C src lustret
25

  
26
lustrev:
27
	@echo Compiling binary lustrev
28
	@make -C src lustrev
29

  
30
lustrei:
31
	@echo Compiling binary lustrei
32
	@make -C src lustrei
33

  
34
@lustresf@
35

  
36
configure: configure.ac
37
	@echo configure.ac has changed relaunching autoconf
38
	@autoconf
39

  
40
Makefile: Makefile.in config.status configure
41
	@echo Makefile.in has changed relaunching autoconf
42
	@./config.status --recheck
43

  
44
doc:
45
	@echo Generating doc
46
	@make -C src doc
47

  
48
dot: doc
49
	@make -C src dot
50

  
51
clean: clean-lusic
52
	@make -C src clean
53

  
54
dist-src-clean: clean
55
	@rm -f config.log config.status include/*.lusic include/lustrec_math.h include/simulink_math_fcn.h include/conv.h include/mpfr_lustre.h
56
	@rm -f Makefile ./src/Makefile ./src/pluginList.ml ./src/version.ml ./src/_tags ./src/ocaml_utils.ml
57

  
58
DIST_ARCHIVE_NAME=lustrec-$(shell $(LOCAL_BINDIR)/lustrec -version | grep version | cut -d, -f 2 | sed -e "s/ version //" -e "s/ (/-/" -e "s/ /-/" -e "s/\//-/" -e "s/)//")-src.tar.gz
59

  
60
dist-gzip: $(LOCAL_BINDIR)/lustrec dist-src-clean
61
	@rm -f $(shell ls ../*lustrec*src*tar.gz)
62
	@tar zcvf ../$(DIST_ARCHIVE_NAME) -C .. --exclude-vcs --exclude=Makefile  --exclude=$(LOCAL_BINDIR) $(shell basename $(PWD))
63
	@echo "Source distribution built: ../$(DIST_ARCHIVE_NAME)"
64

  
65
dist-clean: dist-src-clean
66
	@rm -f configure Makefile opam share/FindLustre.cmake
67

  
68
%.lusic: %.lusi
69
	@echo Compiling $<
70
	@$(LOCAL_BINDIR)/lustrec -verbose 0 -I include -d include $<
71

  
72
clean-lusic:
73
	@rm -f $(LUSI_LIBS:%.lusi=%.lusic)
74
	@rm -f $(LUSI_MPFR_LIB:%.lusi=%.lusic)
75

  
76
compile-lusi: $(LUSI_LIBS:%.lusi=%.lusic)
77

  
78
compile-mpfr-lusi: $(LUSI_MPFR_LIB)
79
	@echo Compiling $<
80
	@$(LOCAL_BINDIR)/lustrec -verbose 0 -mpfr 1 -d include $<
81

  
82
install-include: compile-lusi compile-mpfr-lusi
83
	install -m 0655 include/* ${includedir}/lustrec
84

  
85
install-base: clean-lusic
86
	mkdir -p ${bindir}
87
	for x in $(BIN_TARGETS); do install -m 0755 $(LOCAL_BINDIR)/$$x ${bindir}; done
88
	mkdir -p ${datarootdir}
89
	install -m 0655 share/*.cmake ${datarootdir}
90
	mkdir -p ${includedir}/lustrec
91
	install -m 0655 include/* ${includedir}/lustrec
92

  
93
install: install-base install-include
94

  
95
uninstall:
96
	rm -Rf ${includedir}/lustrec
97
	rm -Rf ${datarootdir}/share/FindLustre.cmake
98
	for x in $(BIN_TARGETS); do rm -f ${bindir}/$$x; done
99

  
100
test-config: ${bindir}/lustrec
101
	if @PATH_TO_TESTS_DEFINED@; then \
102
	  mkdir -p test; \
103
	  cd test; \
104
	  cmake -DLUSTRE_PATH_HINT=${bindir} -DSUBPROJ=@CDASHSUBPROJ@ ../@PATH_TO_TESTS@; \
105
	fi
106

  
107
test-no-submit: test-config
108
	cd test; ctest -M Experimental -T Start -T Update -T Configure -T Build -T Test -R ${DEFAULT_TEST_TARGET} -E ${DEFAULT_EXCLUDE_TEST}
109

  
110
test-submit: test-config
111
	cd test; ctest -M Experimental -T Submit -R ${DEFAULT_TEST_TARGET} -E ${DEFAULT_EXCLUDE_TEST}
112

  
113

  
114
test: test-config
115
	cd test; ctest -D Experimental -R ${DEFAULT_TEST_TARGET} -E ${DEFAULT_EXCLUDE_TEST}
116

  
117

  
118
test-full-no-submit: test-config
119
	cd test; ctest -M Experimental -T Start -T Update -T Configure -T Build -T Test
120

  
121
test-full-submit: test-config
122
	cd test; ctest -M Experimental -T Submit
123

  
124
test-full: test-config
125
	cd test; ctest -D Experimental
126

  
127
tests:
128
	@echo Launching tests
129
	@make -C src tests
130

  
131
.PHONY: all compile-lusi doc dot lustrec lustrec.odocl clean install dist-clean tests
README.lustrec
1
To compile Lustrec:
2
------------------
3

  
4
# autoconf
5
# ./configure
6
# make
7
# make install
8

  
9

  
10
To use lustrec:
11
--------------
12

  
13
In a modular setting:
14
# lustrec <filename.lus>
15
will generate filename.c and filename.h
16

  
17
With a main node:
18
# lustrec -node <main_node> <filename.lus>
19
will generate the same two files,
20
but also filename_main.c that contains a main function
21
and filename_alloc.h that contains the node allocation macros 
22

  
23
With a main node, with a static memory allocation scheme:
24
# lustrec -node <main_node> -dynamic <filename.lus>
25
same as above, but main function will dynamically allocate node memory
26

  
27
To compile it:
28
# gcc -Iinclude filename.c
29
# gcc -Iinclude filename_main.c
30
where include links to the include folder
31

  
32
To run it with the generated main function:
33
- compile the io_frontend.o
34
# gcc -c include/io_frontend.c
35
# gcc -Iinclude -o target_name io_frontend.o filename.o filename_main.o
36
# ./target_name
37

  
38
To analyze it with frama-c
39
# frama-c -cpp-extra-args='-Iinclude'  filename.c
README.md
1
Current status : [![Build Status](https://travis-ci.org/coco-team/lustrec.svg?branch=master)](https://travis-ci.org/coco-team/lustrec)
1 2

  
2
Current Status:    [![Build Status](https://travis-ci.org/coco-team/lustrec.svg?branch=master)](https://travis-ci.org/coco-team/lustrec)
3

  
4
[![Stories in Ready](https://badge.waffle.io/coco-team/lustrec.png?label=ready&title=Ready)](https://waffle.io/coco-team/lustrec)
5
[![Throughput Graph](https://graphs.waffle.io/coco-team/lustrec/throughput.svg)](https://waffle.io/coco-team/lustrec/metrics/throughput)
6

  
7
# LustreC
3
# About LustreC
8 4

  
9 5
LustreC is a modular compiler of Lustre code into C and Horn Clauses.
10 6

  
11 7
# Dependencies
12
On a fresh ubuntu/debian-like install
8

  
9
```
10
export LD_LIBRARY_PATH="$(ocamlfind query z3):$LD_LIBRARY_PATH"
11
```
12

  
13
## On a fresh ubuntu/debian-like install
14
```
13 15
> apt-get install opam libmpfr-dev
16
```
14 17
Get a fresh version of ocaml
18
```
15 19
> opam switch 4.06.1
20
```
16 21
Install some dependencies
22
```
17 23
> opam install depext ocamlgraph mlmpfr num cmdliner fmt logs yojson menhir
24
```
18 25
In OSX, some issues with Z3, please pin the following version:
26
```
19 27
> opam pin add z3 4.8.1
20 28
> opam install z3
29
```
30

  
31
## On Mac
32
brew install autoconf opam cmake
33
Download ada from https://www.adacore.com/download
34

  
35

  
36
Then
37
opam install ocamlfind ocamlgraph cmdliner fmt logs dune num yojson 
38

  
39

  
40
For the ADA backend:
41
- GNAT 2018 community edition on https://www.adacore.com/download
42
- gprbuild shall be in your path
43

  
21 44
# Build
22 45
```
23 46
> autoconf
24 47
> ./configure
25 48
> make
49
> make install
26 50
```
27 51

  
28 52
# Usage
......
30 54
> ./bin/lustrec -help
31 55
```
32 56

  
57
## Examples
58

  
59
In a modular setting:
60
`lustrec <filename.lus>`
61
will generate filename.c and filename.h
62

  
63
With a main node:
64
`lustrec -node <main_node> <filename.lus>`
65
will generate the same two files,
66
but also filename_main.c that contains a main function
67
and filename_alloc.h that contains the node allocation macros 
68

  
69
With a main node, with a static memory allocation scheme:
70
`lustrec -node <main_node> -dynamic <filename.lus>`
71
same as above, but main function will dynamically allocate node memory
72

  
73
To compile it:
74
```
75
gcc -Iinclude filename.c
76
gcc -Iinclude filename_main.c
77
```
78
where include links to the include folder
79

  
80
To run it with the generated main function:
81
- compile the io_frontend.o
82
```
83
gcc -c include/io_frontend.c
84
gcc -Iinclude -o target_name io_frontend.o filename.o filename_main.o
85
./target_name
86
``` 
87

  
88
To analyze it with frama-c
89
`frama-c -cpp-extra-args='-Iinclude'  filename.c`
90

  
91
# Contributors 
92

  
93
# Developer documentation
94

  
95
```
96
dune build @doc-private
97
```
98
The documentation is generated to `_build/default/_doc/_html/lustrec@XXXXXXXX/`
99

  
100
You can find non-code specific documentation in the `/doc` folder.
101

  
33 102
# People
34 103
* Pierre-Loic Garoche (ONERA)
35 104
* Xavier Thirioux (IRIT)
ReleaseProcess.md
1
This file tries to describe the current Lustre release process.
2
Current version is written for a Lustre administrator
3
and may certainly be only readable for them.
4

  
5
Lustre releases should be done with the following steps:
6
    
7
1) Edit lustrec/configure.ac
8
   and bump the version to the right number with
9
 
10
   AC_INIT([lustrec], [1.3], [ploc@garoche.net])
11
   AC_SUBST(VERSION_CODENAME, "Xia/Zhong-Kang")
12

  
13

  
14
3) commit the modified files
15
   lustrec/configure.ac
16
   with a meaningful comment saying you are preparing a Lustre version
17

  
18
4) Do a fresh checkout somewhere
19
    Build lustre from your pristine source tree
20
    git clone https://cavale.enseeiht.fr/git/lustrec lustrec-1.3
21

  
22
    cd lustre-1.3
23
    autoconf
24
    ./configure
25
    make
26

  
27
5) (optional) do any testing you usually do.
28

  
29
6) Tag lustre tree with appropriate version (inside source tree)
30

  
31
     git tag lustrec-1.3-Xia-Zhong-Kang
32
     git push --tags 
33

  
34
7) Make lustre packages
35

  
36
    git archive --format tgz -o $HOME/lustrec-1.3-Xia-Zhong-Kang-src.tgz --prefix lustrec/ master
37
    cd $HOME
38
    tar xvf lustrec-1.3-Xia-Zhong-Kang-src.tgz
39
   cd lustrec
40
   autoconf
41
   cd ..
42
   tar zcvf lustrec-1.3-Xia-Zhong-Kang-src.tgz lustrec
43

  
44
8) (optional) Tests your packages or ask for help to test them
45
    
46
9) put your package in
47
    https://cavale.enseeiht.fr/redmine/projects/lustrec/files
48

  
49
10) Advertise your freshly release package on every social network you belong to.
50

  
51
You are right this process IS painful and should be automated (a lot...)
52
be sure we are working on it :))
53

  
54
12) Re-edit lustre/configure.ac 
55
  and bump the version to the the next number with svn
56

  
57
  #AC_INIT([lustrec], [1.4-gitversion], [ploc@garoche.net])
58
  #AC_SUBST(VERSION_CODENAME, "Xia/Xiang-dev")
ReleaseProcess.txt
1
This file tries to describe the current Lustre release process.
2
Current version is written for a Lustre administrator
3
and may certainly be only readable for them.
4

  
5
Lustre releases should be done with the following steps:
6
    
7
1) Edit lustrec/configure.ac
8
   and bump the version to the right number with
9
 
10
   AC_INIT([lustrec], [1.3], [ploc@garoche.net])
11
   AC_SUBST(VERSION_CODENAME, "Xia/Zhong-Kang")
12

  
13

  
14
3) commit the modified files
15
   lustrec/configure.ac
16
   with a meaningful comment saying you are preparing a Lustre version
17

  
18
4) Do a fresh checkout somewhere
19
    Build lustre from your pristine source tree
20
    git clone https://cavale.enseeiht.fr/git/lustrec lustrec-1.3
21

  
22
    cd lustre-1.3
23
    autoconf
24
    ./configure
25
    make
26

  
27
5) (optional) do any testing you usually do.
28

  
29
6) Tag lustre tree with appropriate version (inside source tree)
30

  
31
     git tag lustrec-1.3-Xia-Zhong-Kang
32
     git push --tags 
33

  
34
7) Make lustre packages
35

  
36
    git archive --format tgz -o $HOME/lustrec-1.3-Xia-Zhong-Kang-src.tgz --prefix lustrec/ master
37
    cd $HOME
38
    tar xvf lustrec-1.3-Xia-Zhong-Kang-src.tgz
39
   cd lustrec
40
   autoconf
41
   cd ..
42
   tar zcvf lustrec-1.3-Xia-Zhong-Kang-src.tgz lustrec
43

  
44
8) (optional) Tests your packages or ask for help to test them
45
    
46
9) put your package in
47
    https://cavale.enseeiht.fr/redmine/projects/lustrec/files
48

  
49
10) Advertise your freshly release package on every social network you belong to.
50

  
51
You are right this process IS painful and should be automated (a lot...)
52
be sure we are working on it :))
53

  
54
12) Re-edit lustre/configure.ac 
55
  and bump the version to the the next number with svn
56

  
57
  #AC_INIT([lustrec], [1.4-gitversion], [ploc@garoche.net])
58
  #AC_SUBST(VERSION_CODENAME, "Xia/Xiang-dev")
bin/.merlin
1
EXCLUDE_QUERY_DIR
2
B /home/corentin/.opam/default/lib/apron
3
B /home/corentin/.opam/default/lib/base
4
B /home/corentin/.opam/default/lib/base/base_internalhash_types
5
B /home/corentin/.opam/default/lib/base/caml
6
B /home/corentin/.opam/default/lib/base/shadow_stdlib
7
B /home/corentin/.opam/default/lib/biniou
8
B /home/corentin/.opam/default/lib/easy-format
9
B /home/corentin/.opam/default/lib/gmp
10
B /home/corentin/.opam/default/lib/jane-street-headers
11
B /home/corentin/.opam/default/lib/num
12
B /home/corentin/.opam/default/lib/ocamlgraph
13
B /home/corentin/.opam/default/lib/ppx_compare/runtime-lib
14
B /home/corentin/.opam/default/lib/ppx_enumerate/runtime-lib
15
B /home/corentin/.opam/default/lib/ppx_hash/runtime-lib
16
B /home/corentin/.opam/default/lib/ppx_inline_test/config
17
B /home/corentin/.opam/default/lib/ppx_inline_test/runtime-lib
18
B /home/corentin/.opam/default/lib/ppx_sexp_conv/runtime-lib
19
B /home/corentin/.opam/default/lib/sexplib0
20
B /home/corentin/.opam/default/lib/time_now
21
B /home/corentin/.opam/default/lib/tiny
22
B /home/corentin/.opam/default/lib/yojson
23
B /home/corentin/.opam/default/lib/z3
24
B /home/corentin/.opam/default/lib/zarith
25
B /usr/lib/ocaml
26
B ../_build/default/bin/.lustre_compiler.eobjs/byte
27
B ../_build/default/bin/.lustre_testgen.eobjs/byte
28
B ../_build/default/bin/.lustre_verifier.eobjs/byte
29
B ../_build/default/lib/.lustrec.objs/byte
30
S /home/corentin/.opam/default/lib/apron
31
S /home/corentin/.opam/default/lib/base
32
S /home/corentin/.opam/default/lib/base/base_internalhash_types
33
S /home/corentin/.opam/default/lib/base/caml
34
S /home/corentin/.opam/default/lib/base/shadow_stdlib
35
S /home/corentin/.opam/default/lib/biniou
36
S /home/corentin/.opam/default/lib/easy-format
37
S /home/corentin/.opam/default/lib/gmp
38
S /home/corentin/.opam/default/lib/jane-street-headers
39
S /home/corentin/.opam/default/lib/num
40
S /home/corentin/.opam/default/lib/ocamlgraph
41
S /home/corentin/.opam/default/lib/ppx_compare/runtime-lib
42
S /home/corentin/.opam/default/lib/ppx_enumerate/runtime-lib
43
S /home/corentin/.opam/default/lib/ppx_hash/runtime-lib
44
S /home/corentin/.opam/default/lib/ppx_inline_test/config
45
S /home/corentin/.opam/default/lib/ppx_inline_test/runtime-lib
46
S /home/corentin/.opam/default/lib/ppx_sexp_conv/runtime-lib
47
S /home/corentin/.opam/default/lib/sexplib0
48
S /home/corentin/.opam/default/lib/time_now
49
S /home/corentin/.opam/default/lib/tiny
50
S /home/corentin/.opam/default/lib/yojson
51
S /home/corentin/.opam/default/lib/z3
52
S /home/corentin/.opam/default/lib/zarith
53
S /usr/lib/ocaml
54
S .
55
S ../lib
56
S ../lib/backends
57
S ../lib/backends/Ada
58
S ../lib/backends/C
59
S ../lib/backends/EMF
60
S ../lib/backends/Horn
61
S ../lib/backends/VHDL
62
S ../lib/checks
63
S ../lib/features/machine_types
64
S ../lib/parsers
65
S ../lib/plugins/mpfr
66
S ../lib/plugins/scopes
67
S ../lib/tools/importer
68
S ../lib/tools/seal
69
S ../lib/tools/tiny
70
S ../lib/tools/zustre
71
S ../lib/utils
72
FLG -ppx '/home/corentin/n7/2A/stage/lustrec_new/_build/default/.ppx/bfcab61e6a21ecf6d2f80029fc1ef484/ppx.exe --as-ppx --cookie '\''inline_tests="enabled"'\'''
73
FLG -w @1..3@5..28@30..39@43@46..47@49..57@61..62-40 -strict-sequence -strict-formats -short-paths -keep-locs -w -warn-error -w @1..3@5..28@30..39@43@46..47@49..57@61..62-40 -strict-sequence -strict-formats -short-paths -keep-locs -w -warn-error -w @1..3@5..28@30..39@43@46..47@49..57@61..62-40 -strict-sequence -strict-formats -short-paths -keep-locs -w -warn-error
bin/dune
1
(executable
2
 (modes (best exe))
3
 (modules Lustre_compiler)
4
 (public_name lustrec)
5
 (name lustre_compiler)
6
 (libraries lustrec)
7
 (flags
8
  (:standard -w -warn-error))
9
 (preprocess
10
  (pps ppx_inline_test)))
11

  
12
(executable
13
 (modes (best exe))
14
 (modules Lustre_testgen)
15
 (public_name lustret)
16
 (name lustre_testgen)
17
 (libraries lustrec)
18
 (flags
19
  (:standard -w -warn-error))
20
 (preprocess
21
  (pps ppx_inline_test)))
22

  
23

  
24
(executable
25
 (modes (best exe))
26
 (modules Lustre_verifier)
27
 (public_name lustrev)
28
 (name lustre_verifier)
29
 (libraries lustrec)
30
 (flags
31
  (:standard -w -warn-error))
32
 (preprocess
33
  (pps ppx_inline_test)))
bin/lustre_compiler.ml
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11
open Lustrec
12
open Format
13
open Log
14
open Compiler_common
15

  
16
open Utils
17
open Lustre_types
18
 
19

  
20
let usage = "Usage: lustrec [options] \x1b[4msource file\x1b[0m"
21

  
22
let extensions = [".ec"; ".lus"; ".lusi"]
23

  
24
(* print a .lusi header file from a source prog *)
25
let print_lusi prog dirname basename extension =
26
  let header = Lusic.extract_header dirname basename prog in
27
  let header_name = dirname ^ "/" ^ basename ^ extension in
28
  let h_out = open_out header_name in
29
  let h_fmt = formatter_of_out_channel h_out in
30
  begin
31
    Typing.uneval_prog_generics header;
32
    Clock_calculus.uneval_prog_generics header;
33
    Printers.pp_lusi_header h_fmt basename header;
34
    close_out h_out
35
  end
36

  
37

  
38

  
39

  
40

  
41

  
42
(* compile a .lus source file *)
43
let rec compile dirname basename extension =
44
  let source_name = dirname ^ "/" ^ basename ^ extension in
45

  
46
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 0>");
47

  
48
  (* Parsing source *)
49
  let prog = parse source_name extension in
50
  
51
  let prog =
52
    if !Options.mpfr &&
53
         extension = ".lus" (* trying to avoid the injection of the module for lusi files *) 
54
    then
55
      Lustrec_mpfr.mpfr_module::prog
56
    else
57
      prog
58
  in
59
  let params = Backends.get_normalization_params () in
60

  
61
  let prog, dependencies = 
62
    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 1 : Normalisation@,");
63
    try 
64
      Compiler_stages.stage1 params prog dirname basename extension
65
    with Compiler_stages.StopPhase1 prog -> (
66
      if !Options.lusi then
67
	begin
68
	  let lusi_ext = extension ^ "i" in
69
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. generating interface file %s@ " (basename ^ lusi_ext));
70
	  print_lusi prog dirname basename lusi_ext;
71
	  Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
72
	  exit 0
73
	end
74
      else if !Options.print_nodes then (
75
        Format.printf "%a@.@?" Printers.pp_node_list prog;
76
        exit 0
77
      )
78
      else
79
        assert false
80
    )
81
  in
82
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. Normalized program:@ %a@ "Printers.pp_prog prog);
83
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@,");
84

  
85
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 2 : Machines generation@,");
86

  
87
  let prog, machine_code = 
88
    Compiler_stages.stage2 params prog 
89
  in
90

  
91
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. Generated machines:@ %a@ " Machine_code_common.pp_machines machine_code);
92

  
93
  if Scopes.Plugin.show_scopes () then
94
    begin
95
      let all_scopes = Scopes.compute_scopes prog !Options.main_node in
96
      (* Printing scopes *)
97
      if !Options.verbose_level >= 1 then
98
	Format.printf "Possible scopes are:@   ";
99
      Format.printf "@[<v>%a@ @]@ @?" Scopes.print_scopes all_scopes;
100
      exit 0
101
	
102
    end;
103
  let machine_code = Plugins.refine_machine_code prog machine_code in
104
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ @ ");
105
  
106
  Compiler_stages.stage3 prog machine_code dependencies basename extension;
107
  begin
108
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ @]@.");
109
    (* We stop the process here *)
110
    exit 0
111
  end
112

  
113
let compile dirname basename extension =
114
  Plugins.init ();
115
  match extension with
116
  | ".lusi"  
117
  | ".lus"   -> compile dirname basename extension
118
  | _        -> assert false
119

  
120
let anonymous filename =
121
  let ok_ext, ext = List.fold_left
122
    (fun (ok, ext) ext' ->
123
      if not ok && Filename.check_suffix filename ext' then
124
	true, ext'
125
      else
126
	ok, ext)
127
    (false, "") extensions in
128
  if ok_ext then
129
    let dirname = Filename.dirname filename in
130
    let basename = Filename.chop_suffix (Filename.basename filename) ext in
131
    compile dirname basename ext
132
  else
133
    raise (Arg.Bad ("Can only compile *.lusi, *.lus or *.ec files"))
134

  
135
let _ =
136
  Global.initialize ();
137
  Corelang.add_internal_funs ();
138
  try
139
    Printexc.record_backtrace true;
140

  
141
    let options = Options_management.lustrec_options @ (Plugins.options ()) in
142
    
143
    Arg.parse options anonymous usage
144
  with
145
  | Parse.Error _
146
  | Types.Error (_,_) | Clocks.Error (_,_) -> exit 1
147
  | Error.Error (loc , kind) (*| Task_set.Error _*) ->
148
     Error.pp_error loc (fun fmt -> Error.pp_error_msg fmt kind);
149
     exit (Error.return_code kind)
150
  (* | Causality.Error _  -> exit (Error.return_code Error.AlgebraicLoop) *)
151
  | Sys_error msg -> (eprintf "Failure: %s@." msg); exit 1
152
  | exc -> (track_exception (); raise exc) 
153

  
154
(* Local Variables: *)
155
(* compile-command:"make -C .." *)
156
(* End: *)
bin/lustre_testgen.ml
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11

  
12
(* This module is used for the lustre test generator *)
13
open Lustrec
14
open Format
15
open Log
16

  
17
open Utils
18
open Lustre_types
19
open Compiler_common
20

  
21
let usage = "Usage: lustret [options] \x1b[4msource file\x1b[0m"
22

  
23
let extensions = [".lus"]
24

  
25
let pp_trace trace_filename mutation_list = 
26
  let trace_file = open_out trace_filename in
27
  let trace_fmt = formatter_of_out_channel trace_file in
28
  Format.fprintf trace_fmt "@[<v 2>{@ %a@ }@]"
29
    (fprintf_list
30
       ~sep:",@ "
31
       (fun fmt (mutation, mutation_loc, mutant_name) ->
32
	 Format.fprintf fmt "\"%s\": { @[<v 0>%a,@ %a@ }@]" 
33
	   mutant_name
34
	   Mutation.print_directive_json mutation
35
	   Mutation.print_loc_json mutation_loc
36
       ))
37
    mutation_list;
38
  Format.fprintf trace_fmt "@.@?" 
39
  
40
  
41
let testgen_source dirname basename extension =
42
  let source_name = dirname ^ "/" ^ basename ^ extension in
43

  
44
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v>");
45

  
46
  (* Parsing source *)
47
  let prog = parse source_name extension in
48
  let params = Backends.get_normalization_params () in
49
  let prog, dependencies =
50
    try
51
      Compiler_stages.stage1 params prog dirname basename extension 
52
   with Compiler_stages.StopPhase1 prog -> (
53
      if !Options.print_nodes then (
54
        Format.printf "%a@.@?" Printers.pp_node_list prog;
55
        exit 0
56
      )
57
      else
58
        assert false
59
    )
60
 in
61
  
62
  (* Two cases
63
     - generation of coverage conditions
64
     - generation of mutants: a number of mutated lustre files 
65
  *)
66
  
67
  if !Options.gen_mcdc then (
68
    let prog_mcdc = PathConditions.mcdc prog in
69
    (* We re-type the fresh equations *)
70
    (*let _ = Modules.load ~is_header:false prog_mcdc in*)
71
    let _ = type_decls !Global.type_env prog_mcdc in
72
    
73
    let destname = !Options.dest_dir ^ "/" ^ basename in
74
    let source_file = destname ^ ".mcdc" in (* Could be changed *)
75

  
76
    (* Modified Lustre is produced in fresh .lus file *)
77
    let source_lus = source_file ^ ".lus" in
78
    let source_out = open_out source_lus in
79
    let fmt = formatter_of_out_channel source_out in
80
    Printers.pp_prog fmt prog_mcdc;
81
    Format.fprintf fmt "@.@?";
82

  
83
    (* Prog is 
84
       (1) cleaned from initial equations TODO
85
       (2) produced as EMF
86
    *)
87
    Options.output := "emf";
88
    let params = Backends.get_normalization_params () in
89
    let prog_mcdc = Normalization.normalize_prog params prog_mcdc in
90
    let prog_mcdc, machine_code = Compiler_stages.stage2 params prog_mcdc in
91
    let source_emf = source_file ^ ".emf" in 
92
    let source_out = open_out source_emf in
93
    let fmt = formatter_of_out_channel source_out in
94
    EMF_backend.translate fmt basename prog_mcdc machine_code;
95

  
96
    exit 0
97
  ) ;
98

  
99
  
100
  (* generate mutants *)
101
  let mutants = Mutation.mutate !Options.nb_mutants prog in
102
  
103
  (* Print generated mutants in target directory. *)
104
  let cpt = ref 0 in
105
  let mutation_list =
106
    List.map (fun (mutation, mutation_loc, mutant) ->
107
    (* Debugging code *)
108
    (* if List.mem !cpt [238;371;601;799;875;998] then *)
109
    (*   Format.eprintf "Mutant %i: %a -> %a" !cpt Printers.pp_expr orig_e Printers.pp_expr new_e  *)
110
    (* ; *)
111
      incr cpt;
112
      let mutant_basename = (Filename.basename basename)^ ".mutant.n" ^ (string_of_int !cpt) ^ extension  in
113
      let mutant_filename = 
114
	match !Options.dest_dir with
115
	| "" -> (* Mutants are generated in source directory *)
116
	   basename^ ".mutant.n" ^ (string_of_int !cpt) ^ extension 
117
      | dir ->  (* Mutants are generated in target directory *)
118
	 dir ^ "/" ^ mutant_basename 
119
    in
120
    let mutant_out = (
121
      try 
122
	open_out mutant_filename 
123
      with
124
	Sys_error _ -> Format.eprintf "Unable to open file %s for writing.@." mutant_filename; exit 1
125
    )
126
    in
127
    let mutant_fmt = formatter_of_out_channel mutant_out in
128
    report ~level:1 (fun fmt -> fprintf fmt ".. generating mutant %s: %a@,@?"
129
      mutant_filename
130
      Mutation.print_directive mutation
131
    );
132
    Format.fprintf mutant_fmt "%a@." Printers.pp_prog mutant;
133
    mutation, mutation_loc, mutant_basename
134
    )
135
      mutants
136
  in
137
  Log.report ~level:1 (fun fmt -> fprintf fmt ".. done @ @]@.");
138
  
139
  (* Printing traceability *)
140
  let trace_filename = 
141
    match !Options.dest_dir with
142
    | "" -> (* Mutant report is generated in source directory *)
143
       basename^ ".mutation.json" 
144
    | dir ->  (* Mutants are generated in target directory *)
145
       dir ^ "/" ^ (Filename.basename basename)^ ".mutation.json"
146
  in
147
  pp_trace trace_filename mutation_list;
148

  
149
  (* Printing the CMakeLists.txt file *)
150
  let cmakelists = 
151
    (if !Options.dest_dir = "" then "" else !Options.dest_dir ^ "/") ^ "CMakeLists.txt"
152
  in
153
  let cmake_file = open_out cmakelists in
154
  let cmake_fmt = formatter_of_out_channel cmake_file in
155
  Format.fprintf cmake_fmt "cmake_minimum_required(VERSION 3.5)@.";
156
  Format.fprintf cmake_fmt "include(\"%s/share/helpful_functions.cmake\")@." Version.prefix;
157
  Format.fprintf cmake_fmt "include(\"%s/share/FindLustre.cmake\")@." Version.prefix;
158
  Format.fprintf cmake_fmt "LUSTREFILES(LFILES ${CMAKE_CURRENT_SOURCE_DIR} )@.";
159
  Format.fprintf cmake_fmt "@[<v 2>FOREACH(lus_file ${LFILES})@ ";
160
  Format.fprintf cmake_fmt "get_lustre_name_ext(${lus_file} L E)@ ";
161
  Format.fprintf cmake_fmt "Lustre_Compile(@[<v 0>@ ";
162
  if !Options.main_node <> "" then Format.fprintf cmake_fmt "NODE \"%s_mutant\"@ " !Options.main_node;
163
  Format.fprintf cmake_fmt "LIBNAME \"${L}_%s_mutant\"@ " !Options.main_node;
164
  Format.fprintf cmake_fmt "LUS_FILES \"${lus_file}\")@]@]@.";
165
  Format.fprintf cmake_fmt "ENDFOREACH()@.@?";
166
  
167
  
168
  (* We stop the process here *)
169
  exit 0
170
    
171
let testgen dirname basename extension =
172
  match extension with
173
  | ".lus"   -> testgen_source dirname basename extension
174
  | _        -> assert false
175

  
176
let anonymous filename =
177
  let ok_ext, ext = List.fold_left
178
    (fun (ok, ext) ext' ->
179
      if not ok && Filename.check_suffix filename ext' then
180
	true, ext'
181
      else
182
	ok, ext)
183
    (false, "") extensions in
184
  if ok_ext then
185
    let dirname = Filename.dirname filename in
186
    let basename = Filename.chop_suffix (Filename.basename filename) ext in
187
    testgen dirname basename ext
188
  else
189
    raise (Arg.Bad ("Can only compile *.lus files"))
190

  
191
let _ =
192
  Global.initialize ();
193
  Corelang.add_internal_funs ();
194
  try
195
    Printexc.record_backtrace true;
196

  
197
    let options = Options_management.lustret_options
198

  
199
    in
200
    
201
    Arg.parse options anonymous usage
202
  with
203
  | Parse.Error _
204
  | Types.Error (_,_) | Clocks.Error (_,_)
205
  | Error.Error _ (*| Task_set.Error _*)
206
  | Causality.Error _ -> exit 1
207
  | Sys_error msg -> (eprintf "Failure: %s@." msg)
208
  | exc -> (track_exception (); raise exc)
209

  
210
(* Local Variables: *)
211
(* compile-command:"make -C .." *)
212
(* End: *)
bin/lustre_verifier.ml
1
(********************************************************************)
2
(*                                                                  *)
3
(*  The LustreC compiler toolset   /  The LustreC Development Team  *)
4
(*  Copyright 2012 -    --   ONERA - CNRS - INPT                    *)
5
(*                                                                  *)
6
(*  LustreC is free software, distributed WITHOUT ANY WARRANTY      *)
7
(*  under the terms of the GNU Lesser General Public License        *)
8
(*  version 2.1.                                                    *)
9
(*                                                                  *)
10
(********************************************************************)
11
open Lustrec
12
open Format
13
open Log
14
open Compiler_common
15

  
16
open Utils
17
open Lustre_types
18
 
19

  
20
let usage = "Usage: lustrev [options] \x1b[4msource file\x1b[0m"
21

  
22
let extensions = [".ec"; ".lus"; ".lusi"]
23

  
24

  
25
(* verify a .lus source file 
26

  
27
we have multiple "backends"
28
- zustre: linked to z3/spacer. Shall preserve the structure and rely on contracts. Produces both a lustre model with new properties, maybe as a lusi with lustre contract, and a JSON summarizing the results and providing tests cases or counter examples if any
29

  
30
- seal: linked to seal. Require global inline and main node
31
  focuses only on the selected node (the main)
32
  map the machine code into SEAL datastructure and compute invariants
33
  - provides the node and its information (typical point of interest for taylor expansion, range for inputs, existing invariants, computation error for the node content)
34
  - simplification of program through taylor expansion
35
  - scaling when provided with typical ranges (not required to be sound for the moment)
36
  - computation of lyapunov invariants
37
  - returns an annotated node with invariants and a JSON to explain computation
38
  - could also returns plots
39

  
40
- tiny: linked to tiny library to perform floating point analyses
41
  shall be provided with ranges for inputs or local variables (memories)
42
  
43
*)
44
let rec verify dirname basename extension =
45
  let source_name = dirname ^ "/" ^ basename ^ extension in
46
  Options.compile_header := false; (* to avoid producing .h / .lusic *)
47
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 0>");
48
  decr Options.verbose_level;
49

  
50
  (* Parsing source *)
51
  let prog = parse source_name extension in
52

  
53
  (* Checking which solver is active *)
54
  incr Options.verbose_level;
55
  let verifier = Verifiers.get_active () in
56
  let module Verifier = (val verifier : VerifierType.S) in
57

  
58
  decr Options.verbose_level;
59
  let params = Verifier.get_normalization_params () in
60
  (* Normalizing it *)
61
  let prog, dependencies = 
62
    Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 1 : Normalisation@,");
63
    try
64
      incr Options.verbose_level;
65
      decr Options.verbose_level;
66
      Compiler_stages.stage1 params prog dirname basename extension
67
    with Compiler_stages.StopPhase1 prog -> (
68
      if !Options.print_nodes then (
69
        Format.printf "%a@.@?" Printers.pp_node_list prog;
70
        exit 0
71
      )
72
      else
73
        assert false
74
    )
75
  in
76
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@,");
77
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. Normalized program:@ %a@ "Printers.pp_prog prog);
78

  
79
  Log.report ~level:1 (fun fmt -> fprintf fmt "@[<v 2>.. Phase 2 : Machines generation@,");
80

  
81
  let prog, machine_code = 
82
    Compiler_stages.stage2 params prog 
83
  in
84

  
85
  Log.report ~level:1 (fun fmt -> fprintf fmt "@]@ ");
86
  Log.report ~level:3 (fun fmt -> fprintf fmt ".. Generated machines:@ %a@ "
87
                                    Machine_code_common.pp_machines machine_code);
88
  
89
  if Scopes.Plugin.show_scopes () then
90
    begin
91
      let all_scopes = Scopes.compute_scopes prog !Options.main_node in
92
      (* Printing scopes *)
93
      if !Options.verbose_level >= 1 then
94
	Format.printf "Possible scopes are:@   ";
95
      Format.printf "@[<v>%a@ @]@ @?" Scopes.print_scopes all_scopes;
96
      exit 0
97
	
98
    end;
99

  
100
  let machine_code = Plugins.refine_machine_code prog machine_code in
101

  
102
  (*assert (dependencies = []); (* Do not handle deps yet *)*)
103
  incr Options.verbose_level;
104
  Verifier.run basename prog machine_code;
105
  begin
106
    decr Options.verbose_level;
107
    Log.report ~level:1 (fun fmt -> fprintf fmt ".. done !@ ");
108
    incr Options.verbose_level;
109
    Log.report ~level:1 (fun fmt -> fprintf fmt "@]@.");
110
    (* We stop the process here *)
111
    exit 0
112
  end
113

  
114

  
115
let anonymous filename =
116
  let ok_ext, ext = List.fold_left
117
    (fun (ok, ext) ext' ->
118
      if not ok && Filename.check_suffix filename ext' then
119
	true, ext'
120
      else
121
	ok, ext)
122
    (false, "") extensions in
123
  if ok_ext then
124
    let dirname = Filename.dirname filename in
125
    let basename = Filename.chop_suffix (Filename.basename filename) ext in
126
    verify dirname basename ext
127
  else
128
    raise (Arg.Bad ("Can only compile *.lusi, *.lus or *.ec files"))
129

  
130
let _ =
131
  Global.initialize ();
132
  Corelang.add_internal_funs ();
133
  try
134
    Printexc.record_backtrace true;
135

  
136
    let options = Options_management.lustrev_options @ (Verifiers.options ()) in
137
    
138
    Arg.parse options anonymous usage
139
  with
140
  | Parse.Error _
141
    | Types.Error (_,_) | Clocks.Error (_,_) -> exit 1
142
  | Error.Error (loc , kind) (*| Task_set.Error _*) -> 
143
     Error.pp_error loc (fun fmt -> Error.pp_error_msg fmt kind);
144
     exit (Error.return_code kind)
145
  (* | Causality.Error _  -> exit (Error.return_code Error.AlgebraicLoop) *)
146
  | Sys_error msg -> (eprintf "Failure: %s@." msg); exit 1
147
  | exc -> (track_exception (); raise exc) 
148

  
149
             (* Local Variables: *)
150
             (* compile-command:"make -C .." *)
151
             (* End: *)
bin/tools/importer/_dune
1

  
2
(executable
3
 (modes (best exe))
4
 (modules Lustre_importer)
5
 (public_name lustrei)
6
 (name lustre_importer)
7
 (libraries lustrec)
8
 (flags
9
  (:standard -w -warn-error))
10
 (preprocess
11
  (pps ppx_inline_test)))
12

  
bin/tools/importer/lustre_importer.ml
1
(* An application that loads json provided input and produces Lustre
2

  
3
Usage:
4
lustrei -vhdl myvhdl.json 
5
lustrei -scade myscademodel.json 
6
  will produce a lustre file that can be compiled and analyzed
7

  
8
VHDL is handled in a double way: as a backend and as an import language
9
In a first step, lustrei -vhdl -print myvhdl.json shall print the VHDL model in stdout
10

  
11
 *)
12
(*
13
open Vhdl_ast
14
open Vhdl_test
15
  *)
16
open Lustrec
17
open Yojson.Safe
18
open Vhdl_deriving_yojson
19
open Vhdl_json_lib
20
open Printf
21

  
22
let _ =
23
(*
24
  (* Load model with Yojson *)
25
  let json = xx in
26

  
27
  (* Create VHDL values *)
28
  let vhdl : vhdl_design_t = xxxx json in
29

  
30
  (* Printing result *)
31
  Format.printf "Loaded VHDL:@.%a@." pp_vhdl_design vhdl
32
 *)
33

  
34
  let vhdl_json = from_file Sys.argv.(1) in
35
  Format.printf "Original file:\n%s\n\n" (pretty_to_string vhdl_json);
36

  
37
  (*let vhdl = design1 in
38
  Format.printf "Loaded VHDL:@.%a@." pp_vhdl_design vhdl;*)
39

  
40
  let vhdl1_json = vhdl_json |> 
41
                   prune_str "TOKEN" |>
42
                   prune_str "IDENTIFIER" |>
43
                   prune_str "SUBTYPE_INDICATION" |>
44
                   prune_null_assoc |>
45
                   to_list_content_str "DESIGN_UNIT" |>
46
                   to_list_content_str "INTERFACE_VARIABLE_DECLARATION" |>
47
                   flatten_ivd |>
48
                   flatten_numeric_literal |>
49
                   to_list_str "ENTITY_DECLARATION" |>
50
                   to_list_str "ARCHITECTURE_BODY" |>
51
                   to_list_str "PACKAGE_DECLARATION" in
52
  Format.printf "Preprocessed json:\n";
53
  Format.printf "%s\n\n" (pretty_to_string vhdl1_json);
54
(*  List.iter (Format.printf "%s\n") (print_depth vhdl1_json 7 ""); *)
55

  
56
  to_file (Sys.argv.(1)^".out.json") vhdl1_json;
57

  
58
(*
59
  let typ = {name = "type"; definition = (Some (Range (Some "toto", 7, 0)))} in
60
  Format.printf "\nModel to string\n%s\n\n" (pretty_to_string (vhdl_subtype_indication_t_to_yojson typ));
61

  
62
  let elem = "[\"SUBTYPE_DECLARATION\", {\"name\": \"byte\", \"typ\": { \"name\": \"bit_vector\", \"definition\": [ \"RANGE_WITH_DIRECTION\", \"downto\", 7, 0 ]}}]" in
63
  match vhdl_definition_t_of_yojson (from_string elem) with
64
    Ok x -> Format.printf "\nString to string\n%s\n\n" (pretty_to_string (vhdl_definition_t_to_yojson x));
65
  | Error e -> Format.printf "Error: %s\n" e;
66
*)
67

  
68
  match vhdl_file_t_of_yojson vhdl1_json with
69
    Ok x -> Format.printf "Parsed VHDL: \n%s\n" (pretty_to_string (vhdl_file_t_to_yojson x))
70
  | Error e -> Format.printf "Error: %s\n" e;
bin/tools/stateflow/README.md
1
# stateflow_CPS_semantics
2
A continuation passing style semantics for Stateflow in Ocaml
3

  
4
Software implements:
5
- our generic CPS semantics, instanciated as
6
  - an evaluator (aka simulator)
7
  - an imperative code generator
8
  - a lustre automaton generator compatible with lustrec (github/coco-team/lustrec)
9
- the reference denotational semantics of Stateflow by Hamon as presented in his EMSOFT'05 paper.
10

  
11
Options:
12
sf_sem takes as input a model name and a backend. Traces are hard coded in the source files.
13

  
14
Backends are interpretor, imperative code generator, lustre code generator.
15
  -model model in {simple, stopwatch} (default: simple)
16
  -eval execute the model on trace <int>
17
  -eval-mode select evaluator: cps, emsoft05 or compare
18
  -gen_imp generate imperative code
19
  -gen_lustre generate lustre model
20
  -modular generate modular code (either for imperative or lustre backend) 0 is not modular, 1 modularize nodes, 2 modularize entry, during and exit actions (default 0)
21

  
22
Example:
23
./sf_sem -model stopwatch -eval-mode compare -eval 1
24

  
bin/tools/stateflow/_dune
1

  
2
(include_subdirs unqualified)
3

  
4
(executable
5
 (modes (best exe))
6
 (modules :standard \ cPS_evaluator)
7
 (public_name lustresf)
8
 (name sf_sem)
9
 (libraries lustrec logs)
10
 (flags
11
  (:standard -w -warn-error))
12
 (preprocess
13
  (pps ppx_inline_test)))
14

  
15

  
bin/tools/stateflow/common/.merlin
1
REC
bin/tools/stateflow/common/activeStates.ml
1
open Lustrec
2
open Basetypes 
3

  
4
(* Module to manipulate set of active states.
5

  
6
   It relies on sets of path to represent active ones.
7
*)
8

  
9
(*******************************)
10
module Vars =
11
struct
12
  include Set.Make (struct type t = path_t let compare = compare end)
13

  
14
  let pp_set fmt rho =
15
    Format.fprintf fmt "@[<v 0>%a@ @]"
16
      (Utils.fprintf_list ~sep:"@ "
17
	 (fun fmt p -> Format.fprintf fmt "%a" pp_path p))
18
      (elements rho)
19
end
20

  
21
module Env =
22
struct
23
  include Map.Make (struct type t = path_t let compare = compare end)
24

  
25
  let from_set s default =
26
    Vars.fold (fun e m -> add e default m ) s empty
27
      
28
  let find a b =
29
    try 
30
      find a b
31
    with Not_found -> (
32
      Format.printf "Looking for %a@." pp_path a ;
33
      raise Not_found
34
    )
35
  let keys a =
36
    fold (fun key _ -> Vars.add key) a Vars.empty
37

  
38
  let pp_env fmt rho =
39
    Format.fprintf fmt "@[<v 0>%a@ @]"
40
      (Utils.fprintf_list ~sep:"@ "
41
	 (fun fmt (p,b) -> Format.fprintf fmt "%a -> %b" pp_path p b))
42
      (bindings rho)
43
end
44

  
45

  
bin/tools/stateflow/common/basetypes.ml
1

  
2
open Lustrec 
3

  
4
let sf_level = 2
5

  
6
(* Basic datatype for model elements: state and junction name, events ... *)
7
type state_name_t         = string
8
type junction_name_t      = string
9
type path_t               = state_name_t list
10
type event_base_t         = string
11
type event_t              = event_base_t option
12
type user_variable_name_t = string
13

  
14
(* Connected to lustrec types *)
15
type base_action_t    = { defs : Lustre_types.statement list;
16
			  ainputs: Lustre_types.var_decl list;
17
			  aoutputs: Lustre_types.var_decl list;
18
			  avariables: Lustre_types.var_decl list;
19
			  (* ident: string; *)
... This diff was truncated because it exceeds the maximum size that can be displayed.

Also available in: Unified diff