jeltz/heptagon
1
0
Fork 0
Code Issues Pull requests Releases Activity

Merge branch 'ctrl-n' into decade

Browse source
This commit is contained in:
Gwenaël Delaval 2015-12-15 09:33:25 +01:00
commit e8ec3e012c
142 changed files with 5081 additions and 980 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
.gitignore vendored
View file

@ -28,3 +28,8 @@ test/_check_builds
lib/java/.classpath
/test/async/build/*
/test/image_filters/java/*
compiler/doc.odocl
compiler/doc.docdir
compiler/_tags
config
config.status

11
CHANGES
View file

@ -1,3 +1,14 @@
Heptagon 1.02.00 (13/12/2015)
-----------------------------
- syntax for attractivity and reachability in contracts
- option to force abstraction of infinite-domain state variables (ctrl-n)
Heptagon 1.01.00 (17/09/2015)
-----------------------------
- back-end towards controller synthesis tool ReaX
Heptagon 1.00.06 (21/02/2014)
-----------------------------

8
Makefile
View file

@ -1,4 +1,6 @@
.PHONY: all install
include config
.PHONY: all install uninstall clean
all:
(cd compiler/; $(MAKE))
@ -8,6 +10,10 @@ install:
(cd compiler; $(MAKE) install)
(cd lib; $(MAKE) install)
uninstall:
(cd compiler; $(MAKE) uninstall)
(cd lib; $(MAKE) uninstall)
clean:
(cd compiler; $(MAKE) clean)
(cd lib; $(MAKE) clean)

6
Makefile-distrib
View file

@ -2,7 +2,7 @@
include config
#version = $(shell date +"%d%m%y")
version = 1.00.06
version = 1.02.00
osname=$(shell uname -s)
hardware=$(shell uname -m)
heptdir = heptagon-$(version)
@ -26,7 +26,7 @@ binary-distrib:
cp -r test/bad test/good test/image_filters test/scripts test/CTestTestfile.cmake export/$(heptbindir)/test
# manual
mkdir -p export/$(heptbindir)/manual
cp manual/heptagon-manual.pdf export/$(heptbindir)/manual
cp manual/heptagon-manual.pdf manual/heptreax-manual.pdf export/$(heptbindir)/manual
# Makefile, config, INSTALL
cp config export/$(heptbindir)
cp Makefile-bin export/$(heptbindir)/Makefile
@ -48,7 +48,7 @@ source-distrib:
cp -r test/bad test/good test/image_filters test/scripts test/CTestTestfile.cmake export/$(heptdir)/test
# manual
mkdir -p export/$(heptdir)/manual
cp manual/heptagon-manual.pdf export/$(heptdir)/manual
cp manual/heptagon-manual.pdf manual/heptreax-manual.pdf export/$(heptdir)/manual
# Makefile, config.in, configure, install-sh, INSTALL, COPYING
cp config.in export/$(heptdir)
cp configure export/$(heptdir)

37
compiler/.project
View file

@ -1,37 +0,0 @@
<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
<name>heptc</name>
<comment></comment>
<projects>
</projects>
<buildSpec>
<buildCommand>
<name>Ocaml.ocamlbuildBuilder</name>
<arguments>
</arguments>
</buildCommand>
</buildSpec>
<natures>
<nature>ocaml.ocamlbuildnature</nature>
</natures>
<filteredResources>
<filter>
<id>1323971806815</id>
<name></name>
<type>30</type>
<matcher>
<id>org.eclipse.ui.ide.multiFilter</id>
<arguments>1.0-name-matches-false-false-_build</arguments>
</matcher>
</filter>
<filter>
<id>1323971806816</id>
<name></name>
<type>21</type>
<matcher>
<id>org.eclipse.ui.ide.multiFilter</id>
<arguments>1.0-name-matches-false-false-*.ml*</arguments>
</matcher>
</filter>
</filteredResources>
</projectDescription>

11
compiler/.projectSettings
View file

@ -1,11 +0,0 @@
<?xml version="1.0" encoding="UTF-8"?>
<section name="OcamlProjectSettings">
<section name="OcamlbuildSettings">
<item value="" key="ocamlbuildProjectLinkerFlags"/>
<item value="" key="ocamlbuildProjectLibs"/>
<item value="" key="ocamlbuildProjectCompilerFlags"/>
<item value="-j 0" key="ocamlbuildProjectOtherFlags"/>
<item value="true" key="ocamlbuildGenerateTypeInfo"/>
<item value="heptc.byte" key="ocamlbuildProjectTargets"/>
</section>
</section>

50
compiler/Makefile
View file

@ -1,9 +1,13 @@
include ../config
BIN:=$(COMPILER)
ifeq ($(ENABLE_SIMULATOR), yes)
BIN:=heptc.$(TARGET) hepts.$(TARGET)
else
BIN:=heptc.$(TARGET)
BIN:=$(BIN) $(SIMULATOR)
endif
ifeq ($(ENABLE_CTRL2EPT_TRANSLATOR), yes)
BIN:=$(BIN) $(CTRLNBAC2EPT_TRANSLATOR)
endif
.PHONY: all clean native byte clean debug install
@ -11,39 +15,31 @@ endif
all: $(TARGET)
native:
ifeq ($(ENABLE_SIMULATOR), yes)
$(OCAMLBUILD) $(COMPILER).native $(SIMULATOR).native
else
$(OCAMLBUILD) $(COMPILER).native
endif
$(OCAMLBUILD) $(addsuffix .native,$(BIN))
byte:
ifeq ($(ENABLE_SIMULATOR), yes)
$(OCAMLBUILD) $(COMPILER).byte $(SIMULATOR).byte
else
$(OCAMLBUILD) $(COMPILER).byte
endif
$(OCAMLBUILD) $(addsuffix .byte,$(BIN))
debug:
ifeq ($(ENABLE_SIMULATOR), yes)
$(OCAMLBUILD) $(COMPILER).d.byte $(SIMULATOR).d.byte
else
$(OCAMLBUILD) $(COMPILER).d.byte
endif
$(OCAMLBUILD) $(addsuffix .d.byte,$(BIN))
profile:
ifeq ($(ENABLE_SIMULATOR), yes)
$(OCAMLBUILD) $(COMPILER).p.native $(SIMULATOR).p.native
else
$(OCAMLBUILD) $(COMPILER).p.native
endif
$(OCAMLBUILD) $(addsuffix .p.native,$(BIN))
install:
$(INSTALL) -d $(INSTALL_BINDIR)
$(INSTALL) $(COMPILER).$(TARGET) $(INSTALL_BINDIR)/$(COMPILER)
ifeq ($(ENABLE_SIMULATOR), yes)
$(INSTALL) $(SIMULATOR).$(TARGET) $(INSTALL_BINDIR)/$(SIMULATOR)
endif
$(foreach t,$(BIN),$(INSTALL) $(t).$(TARGET) $(INSTALL_BINDIR)/$(t);)
uninstall:
$(foreach t,$(BIN),$(RM) $(INSTALL_BINDIR)/$(t);)
clean:
$(OCAMLBUILD) -clean
.PHONY: doc
doc: $(TARGET)
# Filter unused modules by scanning built ones:
find _build -regex '.*.cmi?' -printf '%f\n' \
| sed -e '/ocamlbuild/ d; s/\(.*\)\.cmi$$/\u\1/' \
| sort > doc.odocl;
$(OCAMLBUILD) doc.docdir/index.html

8
compiler/README_ocamlbuild_hepts.txt
View file

@ -1,8 +0,0 @@
To build the graphical simulator with ocamlbuild, one has to create an ocaml library
containing gtkThread.cmo (resp. .cmx): it is not in the lablgtk library.
To do so, go to the lablgtk library directory and type:
ocamlc -a gtkThread.cmo -o lablgtkthread.cma
ocamlopt -a gtkThread.cmx -o lablgtkthread.cmxa

6
compiler/TODO.txt
View file

@ -1,6 +0,0 @@
- Ne plus forcer l'ordre constantes puis types puis definitions de noeud. Il
faudra mettre à jour les phases du compilateur et modifier l'ast.
- Ajouter des constantes locales
- supprimer pinst dans minils
- heptcheck

8
compiler/_tags
View file

@ -1,8 +0,0 @@
<global> or <utilities> or <minils> or <heptagon> or <main> or <obc>:include
<**/*.ml>: debug, dtypes, pkg_ocamlgraph
<preproc.ml>: camlp4of, use_camlp4
true:use_menhir
<**/*.{byte,native}>: use_unix, use_str, debug, custom, pkg_menhirLib, pkg_ocamlgraph
<main/hepts.ml>: pkg_lablgtk2, thread
<main/hepts.{byte,native}>: pkg_lablgtk2, thread

12
compiler/_tags.in Normal file
View file

@ -0,0 +1,12 @@
<global> or <utilities> or <minils> or <heptagon> or <main> or <obc>:include
<**/*.ml*>: debug, dtypes, package(ocamlgraph)
<preproc.ml>: camlp4of, package(camlp4)
true: use_menhir
<**/*.{byte,native}>: package(unix), package(str)
<**/heptc.{byte,native}>: package(menhirLib), package(ocamlgraph)
<main/hepts.{ml,byte,native}>: package(lablgtk2), thread
"heptagon/parsing/hept_parser.mli": package(menhirLib)
<**/*.ml*> or <**/{heptc,ctrl2ept}.{byte,native}>: @package_reatk_ctrlNbac@
"minils/main/mls_compiler.ml" or "main/mls2seq.ml": pp(camlp4o pa_macro.cmo @ctrln_pp@)

2
compiler/global/clocks.ml
View file

@ -98,7 +98,7 @@ and unify_ck ck1 ck2 =
match (ck1, ck2) with
| Cbase, Cbase -> ()
| Cvar { contents = Cindex n1 }, Cvar { contents = Cindex n2 } when n1 = n2 -> ()
| Con (ck1, c1, n1), Con (ck2, c2, n2) when (c1 = c2) & (n1 = n2) ->
| Con (ck1, c1, n1), Con (ck2, c2, n2) when (c1 = c2) && (n1 = n2) ->
unify_ck ck1 ck2
| Cvar ({ contents = Cindex n } as v), ck
| ck, Cvar ({ contents = Cindex n } as v) ->

14
compiler/global/global_mapfold.ml
View file

@ -38,7 +38,7 @@ type 'a global_it_funs = {
static_exp_desc : 'a global_it_funs -> 'a -> static_exp_desc -> static_exp_desc * 'a;
ty : 'a global_it_funs -> 'a -> ty -> ty * 'a;
ct : 'a global_it_funs -> 'a -> ct -> ct * 'a;
ck : 'a global_it_funs -> 'a -> ck -> ck * 'a;
ck : 'a global_it_funs -> 'a -> Clocks.ck -> Clocks.ck * 'a;
link : 'a global_it_funs -> 'a -> link -> link * 'a;
var_ident : 'a global_it_funs -> 'a -> var_ident -> var_ident * 'a;
param : 'a global_it_funs -> 'a -> param -> param * 'a;
@ -97,14 +97,14 @@ and ct funs acc c = match c with
and ck_it funs acc c = try funs.ck funs acc c with Fallback -> ck funs acc c
and ck funs acc c = match c with
| Cbase -> c, acc
| Cvar(link_ref) ->
| Clocks.Cbase -> c, acc
| Clocks.Cvar(link_ref) ->
let l, acc = link_it funs acc link_ref.contents in
Cvar {link_ref with contents = l}, acc
| Con(ck, constructor_name, v) ->
Clocks.Cvar {contents = l}, acc
| Clocks.Con(ck, constructor_name, v) ->
let ck, acc = ck_it funs acc ck in
let v, acc = var_ident_it funs acc v in
Con (ck, constructor_name, v), acc
Clocks.Con (ck, constructor_name, v), acc
and link_it funs acc c =
try funs.link funs acc c with Fallback -> link funs acc c
@ -114,7 +114,7 @@ and link funs acc l = match l with
and var_ident_it funs acc i = funs.var_ident funs acc i
and var_ident funs acc i = i, acc
and var_ident _funs acc i = i, acc
and structure_it funs acc s = funs.structure funs acc s
and structure funs acc s =

7
compiler/global/global_printer.ml
View file

@ -27,7 +27,6 @@
(* *)
(***********************************************************************)
open Names
open Idents
open Signature
open Types
open Clocks
@ -71,8 +70,8 @@ let print_shortname ff {name = n} = print_name ff n
let print_ident = Idents.print_ident
let rec print_ck ff = function
| Cbase -> fprintf ff "."
| Con (ck, c, n) -> fprintf ff "%a on %a(%a)" print_ck ck print_qualname c print_ident n
| Clocks.Cbase -> fprintf ff "."
| Clocks.Con (ck, c, n) -> fprintf ff "%a on %a(%a)" print_ck ck print_qualname c print_ident n
| Cvar { contents = Cindex i } -> fprintf ff "'a%i" i
| Cvar { contents = Clink ck } ->
if !Compiler_options.full_type_info then
@ -195,5 +194,3 @@ let print_interface ff =
NamesEnv.iter
(fun key sigtype -> Format.fprintf ff "%a@," print_interface_value (key,sigtype)) m.m_values;
Format.fprintf ff "@]@."

2
compiler/global/idents.mli
View file

@ -27,8 +27,6 @@
(* *)
(***********************************************************************)
open Names
(** This modules manages unique identifiers,
/!\ To be effective, [enter_node] has to be called when entering a node
[gen_var] generates a variable identifier

3
compiler/global/initial.ml
View file

@ -59,6 +59,9 @@ let mk_static_int_op op args =
let mk_static_int i =
mk_static_exp tint (Sint i)
let mk_static_float f =
mk_static_exp tint (Sfloat f)
let mk_static_bool b =
mk_static_exp tbool (Sbool b)

20
compiler/global/location.ml
View file

@ -30,31 +30,19 @@
(* inspired from the source of the Caml Light 0.73 compiler *)
open Lexing
open Parsing
open Format
(* two important global variables: [input_name] and [input_chan] *)
type location =
Loc of position (* Position of the first character *)
* position (* Position of the next character following the last one *)
let input_name = ref "" (* Input file name. *)
let input_chan = ref stdin (* The channel opened on the input. *)
let initialize iname ic =
input_name := iname;
input_chan := ic
let no_location = Loc (dummy_pos, dummy_pos)
let error_prompt = ">"
(** Prints [n] times char [c] on [oc]. *)
let prints_n_chars ff n c = for i = 1 to n do pp_print_char ff c done
let prints_n_chars ff n c = for _i = 1 to n do pp_print_char ff c done
(** Prints out to [oc] a line designed to be printed under [line] from file [ic]
underlining from char [first] to char [last] with char [ch].
@ -82,7 +70,7 @@ let underline_line ic ff ch line first last =
let copy_lines nl ic ff prompt =
for i = 1 to nl do
for _i = 1 to nl do
pp_print_string ff prompt;
(try pp_print_string ff (input_line ic)
with End_of_file -> pp_print_string ff "<EOF>");
@ -90,13 +78,13 @@ let copy_lines nl ic ff prompt =
done
let copy_chunk p1 p2 ic ff =
try for i = p1 to p2 - 1 do pp_print_char ff (input_char ic) done
try for _i = p1 to p2 - 1 do pp_print_char ff (input_char ic) done
with End_of_file -> pp_print_string ff "<EOF>"
let skip_lines n ic =
try for i = 1 to n do
try for _i = 1 to n do
let _ = input_line ic in ()
done
with End_of_file -> ()

31
compiler/global/modules.ml
View file

@ -30,7 +30,6 @@
(* Module objects and global environnement management *)
open Misc
open Compiler_options
open Signature
open Types
@ -161,7 +160,11 @@ let initialize modul =
List.iter open_module !default_used_modules
(** { 3 Add functions prevent redefinitions } *)
let current () = g_env.current_mod
let select modul = g_env.current_mod <- modul
(** {3 Add functions prevent redefinitions} *)
let _check_not_defined env f =
if QualEnv.mem f env then raise Already_defined
@ -190,7 +193,7 @@ let replace_type f v =
let replace_const f v =
g_env.consts <- QualEnv.add f v g_env.consts
(** { 3 Find functions look in the global environement, nothing more } *)
(** {3 Find functions look in the global environement, nothing more} *)
let find_value x = QualEnv.find x g_env.values
let find_type x = QualEnv.find x g_env.types
@ -204,7 +207,7 @@ let find_struct n =
| Tstruct fields -> fields
| _ -> raise Not_found
(** { 3 Check functions }
(** {3 Check functions}
Try to load the needed module and then to find it,
return true if in the table, return false if it can't find it. *)
@ -226,9 +229,12 @@ let check_const q =
try let _ = QualEnv.find q g_env.consts in true with Not_found -> false
(** { 3 Qualify functions [qualify_* name] return the qualified name
matching [name] in the global env scope (current module :: opened modules).
@raise [Not_found] if not in scope } *)
(** {3 Qualify functions}
[qualify_* name] return the qualified name matching [name] in the global env
scope (current module :: opened modules).
@raise Not_found if not in scope *)
let _qualify env name =
let tries m =
@ -247,11 +253,11 @@ let qualify_const name = _qualify g_env.consts name
(** @return the name as qualified with the current module
(should not be used..)*)
(should not be used..)*)
let current_qual n = { qual = g_env.current_mod; name = n }
(** { 3 Fresh functions return a fresh qualname for the current module } *)
(** {3 Fresh functions return a fresh qualname for the current module} *)
let rec fresh_value pass_name name =
let fname =
@ -306,7 +312,9 @@ let rec fresh_constr pass_name name =
exception Undefined_type of qualname
(** @return the unaliased version of a type. @raise Undefined_type *)
(** @return the unaliased version of a type.
@raise Undefined_type . *)
let rec unalias_type t = match t with
| Tid ({ qual = q } as ty_name) ->
_load_module q;
@ -320,7 +328,7 @@ let rec unalias_type t = match t with
| Tinvalid -> Tinvalid
(** Return the current module as a [module_object] *)
(** Return the current module as a {!module_object} *)
let current_module () =
(* Filter and transform a qualified env into the current module object env *)
let unqualify env = (* unqualify and filter env keys *)
@ -342,4 +350,3 @@ let current_module () =
m_constrs = unqualify_all g_env.constrs;
m_fields = unqualify_all g_env.fields;
m_format_version = g_env.format_version }

2
compiler/global/names.ml
View file

@ -96,7 +96,7 @@ let rec modul_of_string_list = function
let qualname_of_string s =
let q_l_n = Misc.split_string s "." in
match List.rev q_l_n with
| [] -> Misc.internal_error "Names"
| [] -> (* Misc.internal_error "Names" *)raise Exit
| n::q_l -> { qual = modul_of_string_list q_l; name = n }
let modul_of_string s =

5
compiler/global/signature.ml
View file

@ -77,7 +77,7 @@ type type_def =
type const_def = { c_type : ty; c_value : static_exp }
(** { 3 Signature helper functions } *)
(** {3 Signature helper functions} *)
let rec ck_to_sck ck =
let ck = Clocks.ck_repr ck in
@ -120,6 +120,3 @@ let rec field_assoc f = function
| { f_name = n; f_type = ty }::l ->
if f = n then ty
else field_assoc f l

10
compiler/global/static.ml
View file

@ -28,9 +28,8 @@
(***********************************************************************)
(** This module defines static expressions, used in params and for constants.
const n: int = 3;
var x : int^n; var y : int^(n + 2);
x[n - 1], x[1 + 3],... *)
[const n: int = 3;
var x : int^n; var y : int^(n + 2); x[n - 1], x[1 + 3],...] *)
open Names
open Format
@ -193,14 +192,14 @@ let rec simplify_type env ty = match ty with
(** [eval env e] does the same as [simplify]
but if it returns, there are no variables nor op left.
@raise [Errors.Error] when it cannot fully evaluate. *)
@raise Errors.Error when it cannot fully evaluate. *)
let eval env se =
try eval_core false env se
with exn -> message exn
(** [int_of_static_exp env e] returns the value of the expression
[e] in the environment [env], mapping vars to integers.
@raise [Errors.Error] if it cannot be computed.*)
@raise Errors.Error if it cannot be computed.*)
let int_of_static_exp env se = match (eval env se).se_desc with
| Sint i -> i
| _ -> Misc.internal_error "static int_of_static_exp"
@ -258,4 +257,3 @@ let instanciate_constr m constr =
| Cfalse -> Cfalse in
List.map (replace_one m) constr
*)

9
compiler/global/types.ml
View file

@ -28,7 +28,6 @@
(***********************************************************************)
open Names
open Misc
open Location
@ -43,9 +42,9 @@ and static_exp_desc =
| Sconstructor of constructor_name
| Sfield of field_name
| Stuple of static_exp list
| Sarray_power of static_exp * (static_exp list) (** power : 0^n^m : [[0,0,..],[0,0,..],..] *)
| Sarray of static_exp list (** [ e1, e2, e3 ] *)
| Srecord of (field_name * static_exp) list (** { f1 = e1; f2 = e2; ... } *)
| Sarray_power of static_exp * (static_exp list) (** power : [0^n^m : [[0,0,..],[0,0,..],..]] *)
| Sarray of static_exp list (** [[ e1, e2, e3 ]] *)
| Srecord of (field_name * static_exp) list (** [{ f1 = e1; f2 = e2; ... }] *)
| Sop of fun_name * static_exp list (** defined ops for now in pervasives *)
and ty =
@ -66,5 +65,3 @@ let unprod = function
let mk_static_exp ?(loc = no_location) ty desc = (*note ~ty: replace as first arg*)
{ se_desc = desc; se_ty = ty; se_loc = loc }

3
compiler/heptagon/_tags
View file

@ -1,4 +1,5 @@
<parsing>:include
<analysis>:include
<transformations>:include
<main>:include
<main>:include
<ctrln>:include

7
compiler/heptagon/analysis/causal.ml
View file

@ -29,10 +29,7 @@
(* causality check of scheduling constraints *)
open Misc
open Names
open Idents
open Heptagon
open Location
open Sgraph
open Format
@ -148,7 +145,7 @@ let rec ctuple l =
norm_tuple l before (ac::newl)
| ((Aac _) as ac)::l ->
norm_tuple l (cand before ac) newl
| (Aor _)::l -> assert false
| (Aor _)::_ -> assert false
in
norm_tuple l Aempty []
@ -217,7 +214,7 @@ let build ac =
with
| Not_found -> () in
let rec add_dependence g = function
let add_dependence g = function
| Aread(n) -> attach g n; attach_lin g n
| Alinread(n) -> attach g n
| _ -> ()

19
compiler/heptagon/analysis/causality.ml
View file

@ -30,11 +30,8 @@
(* causality check *)
open Misc
open Names
open Idents
open Heptagon
open Location
open Sgraph
open Linearity
open Causal
@ -227,7 +224,7 @@ and typing_automaton state_handlers =
cseq t2 (cseq tb t1) in
corlist (List.map handler state_handlers)
and typing_block { b_local = dec; b_equs = eq_list; b_loc = loc } =
and typing_block { b_local = _dec; b_equs = eq_list; b_loc = _loc } =
(*let teq = typing_eqs eq_list in
Causal.check loc teq;
clear (build dec) teq *)
@ -236,10 +233,10 @@ and typing_block { b_local = dec; b_equs = eq_list; b_loc = loc } =
let typing_contract loc contract =
match contract with
| None -> cempty
| Some { c_block = b;
| Some { c_block = b;
c_assume = e_a;
c_assume_loc = e_a_loc;
c_enforce = e_g;
c_objectives = objs;
c_enforce_loc = e_g_loc;
} ->
let teq = typing_eqs b.b_equs in
@ -247,10 +244,11 @@ let typing_contract loc contract =
cseq
teq
(ctuplelist
[(typing e_a);
(typing e_g);
(typing e_a_loc);
(typing e_g_loc)]) in
((typing e_a) ::
(typing e_a_loc) ::
(typing e_g_loc) ::
(List.map (fun o -> typing o.o_exp) objs)
)) in
Causal.check loc t_contract;
let t_contract = clear (build b.b_local) t_contract in
t_contract
@ -264,4 +262,3 @@ let typing_node { n_contract = contract;
let program ({ p_desc = pd } as p) =
List.iter (function Pnode n -> typing_node n | _ -> ()) pd;
p

51
compiler/heptagon/analysis/hept_clocking.ml
View file

@ -37,21 +37,21 @@
*)
open Misc
open Names
open Idents
open Heptagon
open Hept_utils
open Global_printer
open Hept_printer
open Signature
open Types
open Clocks
open Location
open Format
(** Error Kind *)
type error_kind = | Etypeclash of ct * ct | Eclockclash of ck * ck | Edefclock
type error_kind =
| Etypeclash of ct * ct
| Eclockclash of Clocks.ck * Clocks.ck
| Edefclock
let error_message loc = function
| Etypeclash (actual_ct, expected_ct) ->
@ -113,11 +113,11 @@ let rec typing h pat e =
typing h pat e
| Ewhen (e,c,n) ->
let ck_n = ck_of_name h n in
let base = expect h pat (skeleton ck_n e.e_ty) e in
skeleton (Con (ck_n, c, n)) e.e_ty, Con (ck_n, c, n)
let _base = expect h pat (skeleton ck_n e.e_ty) e in
skeleton (Clocks.Con (ck_n, c, n)) e.e_ty, Clocks.Con (ck_n, c, n)
| Emerge (x, c_e_list) ->
let ck = ck_of_name h x in
List.iter (fun (c,e) -> expect h pat (Ck(Con (ck,c,x))) e) c_e_list;
List.iter (fun (c,e) -> expect h pat (Ck(Clocks.Con (ck,c,x))) e) c_e_list;
Ck ck, ck
| Estruct l ->
let ck = fresh_clock () in
@ -134,7 +134,7 @@ let rec typing h pat e =
typing_app h base_ck pat op (pargs@args)
| Imapi -> (* clocking the node with the extra i input on [ck_r] *)
let il (* stubs i as 0 *) =
List.map (fun x -> mk_exp
List.map (fun _ -> mk_exp
(Econst (Initial.mk_static_int 0))
~ct_annot:(Some(Ck(base_ck)))
Initial.tint
@ -145,12 +145,12 @@ let rec typing h pat e =
| Ifold | Imapfold ->
(* clocking node with equality constaint on last input and last output *)
let ct = typing_app h base_ck pat op (pargs@args) in
Misc.optional (unify (Ck(Clocks.last_clock ct)))
(Misc.last_element args).e_ct_annot;
ignore (Misc.optional (unify (Ck(Clocks.last_clock ct)))
(Misc.last_element args).e_ct_annot);
ct
| Ifoldi -> (* clocking the node with the extra i and last in/out constraints *)
let il (* stubs i as 0 *) =
List.map (fun x -> mk_exp
List.map (fun _ -> mk_exp
(Econst (Initial.mk_static_int 0))
~ct_annot:(Some(Ck(base_ck)))
Initial.tint
@ -163,8 +163,8 @@ let rec typing h pat e =
| h::l -> h::(insert_i l)
in
let ct = typing_app h base_ck pat op (pargs@(insert_i args)) in
Misc.optional (unify (Ck (Clocks.last_clock ct)))
(Misc.last_element args).e_ct_annot;
ignore (Misc.optional (unify (Ck (Clocks.last_clock ct)))
(Misc.last_element args).e_ct_annot);
ct
in
ct, base_ck
@ -183,7 +183,7 @@ let rec typing h pat e =
ct, base
and expect h pat expected_ct e =
let actual_ct,base = typing h pat e in
let actual_ct,_base = typing h pat e in
(try unify actual_ct expected_ct
with Unify -> error_message e.e_loc (Etypeclash (actual_ct, expected_ct)))
@ -207,8 +207,8 @@ and typing_app h base pat op e_list = match op with
| None -> build_env a_l v_l env
| Some n -> build_env a_l v_l ((n,v)::env))
| _ ->
Printf.printf "Fun/node : %s\n" (Names.fullname f);
Misc.internal_error "Clocking, non matching signature"
Misc.internal_error ("Clocking, non matching signature in call of "^
Names.fullname f);
in
let env_pat = build_env node.node_outputs pat_id_list [] in
let env_args = build_env node.node_inputs e_list [] in
@ -237,7 +237,7 @@ and typing_app h base pat op e_list = match op with
let append_env h vds =
List.fold_left (fun h { v_ident = n; v_clock = ck } -> Env.add n ck h) h vds
let rec typing_eq h ({ eq_desc = desc; eq_loc = loc } as eq) =
let rec typing_eq h ({ eq_desc = desc; eq_loc = loc } as _eq) =
match desc with
| Eeq(pat,e) ->
let ct,_ = typing h pat e in
@ -253,7 +253,7 @@ let rec typing_eq h ({ eq_desc = desc; eq_loc = loc } as eq) =
and typing_eqs h eq_list = List.iter (typing_eq h) eq_list
and typing_block h
({ b_local = l; b_equs = eq_list; b_loc = loc } as b) =
({ b_local = l; b_equs = eq_list } as _b) =
let h' = append_env h l in
typing_eqs h' eq_list;
h'
@ -263,14 +263,14 @@ let typing_contract h contract =
| None -> h
| Some { c_block = b;
c_assume = e_a;
c_enforce = e_g;
c_objectives = objs;
c_controllables = c_list } ->
let h' = typing_block h b in
(* assumption *)
expect h' (Etuplepat []) (Ck Cbase) e_a;
expect h' (Etuplepat []) (Ck Clocks.Cbase) e_a;
(* property *)
expect h' (Etuplepat []) (Ck Cbase) e_g;
List.iter (fun o -> expect h' (Etuplepat []) (Ck Clocks.Cbase) o.o_exp) objs;
append_env h c_list
let typing_local_contract h contract =
@ -279,9 +279,9 @@ let typing_local_contract h contract =
| Some { c_assume_loc = e_a_loc;
c_enforce_loc = e_g_loc } ->
(* assumption *)
expect h (Etuplepat []) (Ck Cbase) e_a_loc;
expect h (Etuplepat []) (Ck Clocks.Cbase) e_a_loc;
(* property *)
expect h (Etuplepat []) (Ck Cbase) e_g_loc
expect h (Etuplepat []) (Ck Clocks.Cbase) e_g_loc
(* check signature causality and update it in the global env *)
let update_signature h node =
@ -302,7 +302,7 @@ let typing_node node =
let h = typing_block h node.n_block in
typing_local_contract h node.n_contract;
(* synchronize input and output on base : find the free vars and set them to base *)
Env.iter (fun _ ck -> unify_ck Cbase (root_ck_of ck)) h0;
Env.iter (fun _ ck -> unify_ck Clocks.Cbase (root_ck_of ck)) h0;
(*update clock info in variables descriptions *)
let set_clock vd = { vd with v_clock = ck_repr (Env.find vd.v_ident h) } in
let node = { node with n_input = List.map set_clock node.n_input;
@ -318,4 +318,3 @@ let program p =
| _ -> pd
in
{ p with p_desc = List.map program_desc p.p_desc; }

13
compiler/heptagon/analysis/initialization.ml
View file

@ -39,12 +39,10 @@
(* Requis : typage *)
open Misc
open Names
open Idents
open Heptagon
open Types
open Location
open Format
type typ =
| Iproduct of typ list
@ -190,7 +188,6 @@ let rec less left_ty right_ty =
module Printer = struct
open Format
open Pp_tools
open Global_printer
let rec print_init ff i = match !i with
| Izero -> fprintf ff "initialized"
@ -214,8 +211,6 @@ module Printer = struct
end
module Error = struct
open Location
type error = | Eclash of root * typ * typ
exception Error of location * error
@ -349,7 +344,7 @@ and typing_automaton h state_handlers =
let initialized h { s_block = { b_defnames = l } } =
let env_update x h =
try
let xl = IEnv.find_last x h in (* it's a last in the env, good. *)
let _xl = IEnv.find_last x h in (* it's a last in the env, good. *)
IEnv.add_last x (IEnv.find_var x h) h
with Not_found -> h (* nothing to do *)
in
@ -392,14 +387,14 @@ let typing_contract h contract =
| None -> h
| Some { c_block = b;
c_assume = e_a;
c_enforce = e_g;
c_objectives = objs;
c_controllables = c } ->
let h' = build h b.b_local in
typing_eqs h' b.b_equs;
(* assumption *)
expect h' e_a (skeleton izero e_a.e_ty);
(* property *)
expect h' e_g (skeleton izero e_g.e_ty);
List.iter (fun o -> expect h' o.o_exp (skeleton izero o.o_exp.e_ty)) objs;
build_initialized h c
let typing_node { n_input = i_list; n_output = o_list;
@ -412,5 +407,3 @@ let typing_node { n_input = i_list; n_output = o_list;
let program ({ p_desc = pd } as p) =
List.iter (function Pnode n -> typing_node n | _ -> ()) pd;
p

10
compiler/heptagon/analysis/linear_typing.ml
View file

@ -32,7 +32,6 @@ open Names
open Location
open Misc
open Signature
open Modules
open Heptagon
type error =
@ -203,7 +202,7 @@ let check_fresh_lin_var (env, used_vars, init_vars) loc lin =
(** Substitutes linearity variables (Lvar r) with their value
given by the map. *)
let rec subst_lin m lin_list =
let subst_lin m lin_list =
let subst_one = function
| Lvar r ->
(try
@ -253,7 +252,7 @@ let subst_from_lin (s,m) expect_lin lin =
)
| _, _ -> s,m
let rec not_linear_for_exp e =
let not_linear_for_exp e =
lin_skeleton Ltop e.e_ty
let check_init env loc init lin =
@ -399,7 +398,7 @@ let rec fuse_args_lin args_lin collect_lins =
(** [extract_not_lin_var_exp args_lin e_list] returns the linearities
and expressions from e_list that are not yet set to Lvar r.*)
let rec extract_not_lin_var_exp args_lin e_list =
let extract_not_lin_var_exp args_lin e_list =
match args_lin, e_list with
| [], [] -> [], []
| arg_lin::args_lin, e::e_list ->
@ -791,7 +790,7 @@ and typing_eq env eq =
| Eeq(Evarpat y, { e_desc = Efby(e_1, e_2) }) ->
let lin = lin_of_ident y env in
let _, env = check_init env eq.eq_loc eq.eq_inits lin in
safe_expect env Ltop e_1;
ignore (safe_expect env Ltop e_1);
safe_expect env lin e_2
| Eeq(pat, e) ->
let lin_pat = typing_pat env pat in
@ -917,4 +916,3 @@ let node f =
let program ({ p_desc = pd } as p) =
List.iter (function Pnode n -> node n | _ -> ()) pd;
p

17
compiler/heptagon/analysis/stateful.ml
View file

@ -27,7 +27,6 @@
(* *)
(***********************************************************************)
(* Checks that a node declared stateless is stateless, and set possible nodes as stateless. *)
open Names
open Location
open Signature
open Modules
@ -64,36 +63,36 @@ let edesc funs stateful ed =
| Eapp({ a_op = (Enode f | Efun f) } as app, e_list, r) ->
let ty_desc = find_value f in
let op = if ty_desc.node_stateful then Enode f else Efun f in
Eapp({ app with a_op = op }, e_list, r), ty_desc.node_stateful or stateful
Eapp({ app with a_op = op }, e_list, r), ty_desc.node_stateful || stateful
| Eiterator(it, ({ a_op = (Enode f | Efun f) } as app), n, pe_list, e_list, r) ->
let ty_desc = find_value f in
let op = if ty_desc.node_stateful then Enode f else Efun f in
Eiterator(it, { app with a_op = op }, n, pe_list, e_list, r),
ty_desc.node_stateful or stateful
ty_desc.node_stateful || stateful
| _ -> ed, stateful
(* Automatons have an hidden state whatever *)
let eqdesc funs stateful eqd =
let eqd, stateful = Hept_mapfold.eqdesc funs stateful eqd in
let is_automaton = match eqd with | Eautomaton _ -> true | _ -> false in
eqd, stateful or is_automaton
eqd, stateful || is_automaton
(* update eq_stateful field *)
let eq funs acc eq =
let eq, stateful = Hept_mapfold.eq funs false eq in
{ eq with eq_stateful = stateful }, stateful or acc
{ eq with eq_stateful = stateful }, stateful || acc
(* update b_stateful field *)
let block funs acc b =
let b, stateful = Hept_mapfold.block funs false b in
{ b with b_stateful = stateful }, acc or stateful
{ b with b_stateful = stateful }, acc || stateful
(* Strong preemption should be decided with stateles expressions *)
let escape_unless funs acc esc =
let esc, stateful = Hept_mapfold.escape funs false esc in
if stateful then
message esc.e_cond.e_loc Eexp_should_be_stateless;
esc, acc or stateful
esc, acc || stateful
(* Present conditions should be stateless *)
let present_handler funs acc ph =
@ -108,8 +107,8 @@ let present_handler funs acc ph =
let node_dec funs _ n =
Idents.enter_node n.n_name;
let n, stateful = Hept_mapfold.node_dec funs false n in
if stateful & (not n.n_stateful) then message n.n_loc Eshould_be_a_node;
if not stateful & n.n_stateful (* update the global env if stateful is not necessary *)
if stateful && (not n.n_stateful) then message n.n_loc Eshould_be_a_node;
if not stateful && n.n_stateful (* update the global env if stateful is not necessary *)
then Modules.replace_value n.n_name
{ (Modules.find_value n.n_name) with Signature.node_stateful = false };
{ n with n_stateful = stateful }, false (* set stateful only if needed *)

32
compiler/heptagon/analysis/typing.ml
View file

@ -39,7 +39,6 @@ open Static
open Types
open Global_printer
open Heptagon
open Hept_mapfold
open Pp_tools
open Format
@ -440,7 +439,7 @@ let rec _unify cenv t1 t2 =
_unify cenv ty1 ty2
| _ -> raise Unify
(** { 3 Constraints related functions } *)
(** {3 Constraints related functions} *)
and (curr_constrnt : constrnt list ref) = ref []
and solve ?(unsafe=false) c_l =
@ -1173,12 +1172,16 @@ and build cenv h dec =
in
mapfold var_dec (Env.empty, h) dec
let typing_objective cenv h obj =
let typed_e = expect cenv h (Tid Initial.pbool) obj.o_exp in
{ obj with o_exp = typed_e }
let typing_contract cenv h contract =
match contract with
| None -> None,h
| Some ({ c_block = b;
c_assume = e_a;
c_enforce = e_g;
c_objectives = objs;
c_assume_loc = e_a_loc;
c_enforce_loc = e_g_loc;
c_controllables = c }) ->
@ -1189,15 +1192,20 @@ let typing_contract cenv h contract =
(* assumption *)
let typed_e_a = expect cenv h' (Tid Initial.pbool) e_a in
let typed_e_a_loc = expect cenv h' (Tid Initial.pbool) e_a_loc in
(* property *)
let typed_e_g = expect cenv h' (Tid Initial.pbool) e_g in
(* objectives *)
let typed_objs =
List.map
(fun o ->
let typed_exp = expect cenv h' (Tid Initial.pbool) o.o_exp in
{ o with o_exp = typed_exp; })
objs in
let typed_e_g_loc = expect cenv h' (Tid Initial.pbool) e_g_loc in
let typed_c, (c_names, h) = build cenv h c in
let typed_c, (_c_names, h) = build cenv h c in
Some { c_block = typed_b;
c_assume = typed_e_a;
c_enforce = typed_e_g;
c_objectives = typed_objs;
c_assume_loc = typed_e_a_loc;
c_enforce_loc = typed_e_g_loc;
c_controllables = typed_c }, h
@ -1205,7 +1213,7 @@ let typing_contract cenv h contract =
let build_node_params cenv l =
let check_param env p =
let ty = check_type cenv p.p_type in
let ty = check_type env p.p_type in
let p = { p with p_type = ty } in
let n = Names.local_qn p.p_name in
p, QualEnv.add n ty env
@ -1222,7 +1230,7 @@ let node ({ n_name = f; n_input = i_list; n_output = o_list;
try
let typed_params, cenv =
build_node_params QualEnv.empty node_params in
let typed_i_list, (input_names, h) = build cenv Env.empty i_list in
let typed_i_list, (_input_names, h) = build cenv Env.empty i_list in
let typed_o_list, (output_names, h) = build cenv h o_list in
(* typing contract *)
@ -1253,11 +1261,11 @@ let node ({ n_name = f; n_input = i_list; n_output = o_list;
| TypingError(error) -> message loc error
let typing_const_dec cd =
let ty = check_type QualEnv.empty cd.c_type in
let se = expect_static_exp QualEnv.empty ty cd.c_value in
let ty = check_type QualEnv.empty cd.Heptagon.c_type in
let se = expect_static_exp QualEnv.empty ty cd.Heptagon.c_value in
let const_def = { Signature.c_type = ty; Signature.c_value = se } in
Modules.replace_const cd.c_name const_def;
{ cd with c_value = se; c_type = ty }
{ cd with Heptagon.c_value = se; Heptagon.c_type = ty }
let typing_typedec td =
let tydesc = match td.t_desc with

13
compiler/heptagon/analysis/unsafe.ml
View file

@ -27,7 +27,6 @@
(* *)
(***********************************************************************)
(* Checks that a node not declared unsafe is safe, and set app unsafe flag. *)
open Names
open Location
open Signature
open Modules
@ -58,17 +57,17 @@ let exp funs unsafe e =
let e, unsafe = Hept_mapfold.exp funs unsafe e in
match e.e_desc with
| Eapp({ a_op = op } as app, e_l, r) ->
let u = (unsafe_op op) or app.a_unsafe in
if u & (not unsafe)
let u = (unsafe_op op) || app.a_unsafe in
if u && (not unsafe)
then message e.e_loc Eshould_be_unsafe
else {e with e_desc = Eapp({ app with a_unsafe = u }, e_l, r)}, (unsafe or u)
else {e with e_desc = Eapp({ app with a_unsafe = u }, e_l, r)}, (unsafe || u)
| Eiterator(it, ({ a_op = op } as app), n, pe_list, e_list, r) ->
let u = (unsafe_op op) or app.a_unsafe in
if u & (not unsafe)
let u = (unsafe_op op) || app.a_unsafe in
if u && (not unsafe)
then message e.e_loc Eshould_be_unsafe
else
{e with e_desc = Eiterator(it, { app with a_unsafe = u }, n, pe_list, e_list, r)}
, (unsafe or u)
, (unsafe || u)
| _ -> e, unsafe
(* unsafe nodes are rejected if they are not declared unsafe *)

421
compiler/heptagon/ctrln/ctrlNbacAsEpt.ml Normal file
View file

@ -0,0 +1,421 @@
(***********************************************************************)
(* *)
(* Heptagon *)
(* *)
(* Gwenael Delaval, LIG/INRIA, UJF *)
(* Leonard Gerard, Parkas, ENS *)
(* Adrien Guatto, Parkas, ENS *)
(* Cedric Pasteur, Parkas, ENS *)
(* Marc Pouzet, Parkas, ENS *)
(* Nicolas Berthier, SUMO, INRIA *)
(* *)
(* Copyright 2014 ENS, INRIA, UJF *)
(* *)
(* This file is part of the Heptagon compiler. *)
(* *)
(* Heptagon is free software: you can redistribute it and/or modify it *)
(* under the terms of the GNU General Public License as published by *)
(* the Free Software Foundation, either version 3 of the License, or *)
(* (at your option) any later version. *)
(* *)
(* Heptagon is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU General Public License for more details. *)
(* *)
(* You should have received a copy of the GNU General Public License *)
(* along with Heptagon. If not, see <http://www.gnu.org/licenses/> *)
(* *)
(***********************************************************************)
open Format
open Signature
open Types
open Names
open Idents
open Heptagon
open CtrlNbac
open AST
exception Untranslatable of string * Loc.t option
(* --- *)
(** Private record gathering temporary generation data *)
type 'f gen_data =
{
decls: ('f, 'f var_spec) decls;
ltyps: (typ * 'f option) SMap.t;
qname: string -> qualname;
typ_symbs: type_name SMap.t;
mutable env: var_dec Env.t;
mutable var_names: ident SMap.t;
}
let no_typ_symbs: type_name SMap.t = SMap.empty
(* --- *)
let mk_gen_data qualname typ_symbs decls typdefs =
{
decls;
ltyps = label_typs typdefs;
qname = (fun name -> { qual = modul qualname; name });
typ_symbs;
env = Env.empty;
var_names = SMap.empty;
}
(* --- *)
let opt_decl_loc gd v = match SMap.find v gd.decls with | _, _, loc -> loc
let translate_typ gd vdecl = function
| `Bool -> Initial.tbool
| `Int -> Initial.tint
| `Real -> Initial.tfloat
| `Enum tn -> Tid (SMap.find tn gd.typ_symbs)
| t -> raise (Untranslatable (asprintf "type %a" print_typ t,
opt_decl_loc gd vdecl))
let symb_typ gd s = try match SMap.find s gd.decls with | typ, _, _ -> typ with
| Not_found -> fst (SMap.find s gd.ltyps)
let symb_typ' gd s = translate_typ gd s (symb_typ gd s)
let ts gd v = try SMap.find v gd.var_names with Not_found ->
failwith (asprintf "Variable name `%a' unavailable; \
was it an output of the main node?" Symb.print v)
let pat_of_var gd v = Evarpat (ts gd v)
(* --- *)
let mkp t e =
{
e_desc = e;
e_ty = t;
e_ct_annot = None;
e_level_ck = Clocks.Cbase;
e_linearity = Linearity.Ltop;
e_loc = Location.no_location;
}
let mkb = mkp Initial.tbool
let mk_app op =
{
a_op = op;
a_params = [];
a_unsafe = false; (* ??? *)
a_inlined = true; (* ??? *)
}
let mk_uapp op e = Eapp (mk_app op, [e] , None)
let mk_bapp op e f = Eapp (mk_app op, [e; f] , None)
let mk_ite c t e = Eapp (mk_app Eifthenelse, [c; t; e] , None)
let apptyp = function
| Eapp ({ a_op = Eifthenelse }, _ :: { e_ty } :: _, _) -> e_ty
| _ -> assert false
let eqrel: eqrel -> fun_name = function
| `Eq -> Initial.mk_pervasives "="
| `Ne -> Initial.mk_pervasives "<>"
let float_typ t = Modules.unalias_type t = Initial.tfloat
let totrel t : totrel -> fun_name =
if float_typ t
then function
| `Lt -> Initial.mk_pervasives "<."
| `Le -> Initial.mk_pervasives "<=."
| `Gt -> Initial.mk_pervasives ">."
| `Ge -> Initial.mk_pervasives ">=."
| `Eq -> Initial.mk_pervasives "=." (* XXX: error case? *)
| `Ne -> Initial.mk_pervasives "<>." (* ibid *)
else function
| `Lt -> Initial.mk_pervasives "<"
| `Le -> Initial.mk_pervasives "<="
| `Gt -> Initial.mk_pervasives ">"
| `Ge -> Initial.mk_pervasives ">="
| #eqrel as r -> eqrel r
let nuop t : nuop -> fun_name =
if float_typ t
then function
| `Opp -> Initial.mk_pervasives "~-."
else function
| `Opp -> Initial.mk_pervasives "~-"
let nnop t : nnop -> fun_name =
if float_typ t
then function
| `Sum -> Initial.mk_pervasives "+."
| `Sub -> Initial.mk_pervasives "-."
| `Mul -> Initial.mk_pervasives "*."
| `Div -> Initial.mk_pervasives "/."
else function
| `Sum -> Initial.mk_pervasives "+"
| `Sub -> Initial.mk_pervasives "-"
| `Mul -> Initial.mk_pervasives "*"
| `Div -> Initial.mk_pervasives "/"
let buop: buop -> fun_name = function
| `Neg -> Initial.pnot
let bnop: bnop -> fun_name = function
| `Conj -> Initial.pand
| `Disj -> Initial.por
| `Excl -> failwith "TODO: translation of exclusion operator"
let translate_expr gd e =
let mkb_bapp_eq ?flag tr e f l =
let e = tr ?flag e in
let mkcmp a b = mkb (mk_bapp (Efun (eqrel `Eq)) a b) in
let mkcmp' f = mkcmp e (tr ?flag f) in
let disj = mk_bapp (Efun Initial.por) in
List.fold_left (fun acc f -> mkb (disj acc (mkcmp' f))) (mkcmp' f) l
and mkb_bapp ?flag op tr e f l =
let op = mk_bapp op in
List.fold_left (fun acc e -> mkb (op acc (tr ?flag e))) (tr ?flag e) (f::l)
and trcond ?flag tb tr = ignore flag; function
| `Ite (c, t, e) -> let e = mk_ite (tb c) (tr t) (tr e) in mkp (apptyp e) e
in
let rec tb ?flag = function
| `Ref v -> mkb (Evar (ts gd v))
| `Bool b -> mkb (Econst (Initial.mk_static_bool b))
| `Buop (op, e) -> mkb (mk_uapp (Efun (buop op)) (tb e))
| `Bnop (op, e, f, l) -> mkb_bapp ?flag (Efun (bnop op)) tb e f l
| `Bcmp (re, e, f) -> mkb (mk_bapp (Efun (eqrel re)) (tb e) (tb f))
| `Ecmp (re, e, f) -> mkb (mk_bapp (Efun (eqrel re)) (te e) (te f))
| `Pcmp (re, e, f) -> mkb (mk_bapp (Efun (eqrel re)) (tp e) (tp f))
| `Ncmp (re, e, f) -> mkb_ncmp re e f
| `Pin (e, f, l) -> mkb_bapp_eq ?flag tp e f l
| `Bin (e, f, l) -> mkb_bapp_eq ?flag tb e f l
| `Ein (e, f, l) -> mkb_bapp_eq ?flag te e f l
| `BIin _ -> raise (Untranslatable ("bounded Integer membership", flag))
| #cond as c -> trcond ?flag tb tb c
| #flag as e -> apply' tb e
and te ?flag = ignore flag; function
| `Ref v -> mkp (symb_typ' gd v) (Evar (ts gd v))
| `Enum l -> let s = label_symb l in
let t = symb_typ' gd s in
let c = gd.qname (Symb.to_string s) in
mkp t (Econst (mk_static_exp t (Sconstructor c)))
| #cond as c -> trcond ?flag tb te c
| #flag as e -> apply' te e
and tn ?flag = function
| `Ref v -> mkp (symb_typ' gd v) (Evar (ts gd v))
| `Int i -> mkp Initial.tint (Econst (Initial.mk_static_int i))
| `Real r -> mkp Initial.tfloat (Econst (Initial.mk_static_float r))
| `Mpq r -> tn ?flag (`Real (Mpqf.to_float r))
| `Bint (s, w, _) -> raise (Untranslatable (asprintf "constant of type \
%a" print_typ (`Bint (s, w)), flag))
| `Nuop (op, e) -> mk_nuapp ?flag op e
| `Nnop (op, e, f, l) -> mk_nnapp ?flag op e f l
| #cond as c -> trcond ?flag tb tn c
| #flag as e -> apply' tn e
and mkb_ncmp ?flag re e f =
let { e_ty } as e = tn ?flag e and f = tn f in
mkb (mk_bapp (Efun (totrel e_ty re)) e f)
and mk_nuapp ?flag op e =
let { e_ty } as e = tn ?flag e in
mkp e_ty (mk_uapp (Efun (nuop e_ty op)) e)
and mk_nnapp ?flag op e f l =
let { e_ty } as e = tn ?flag e in
let op = mk_bapp (Efun (nnop e_ty op)) in
List.fold_left (fun acc e -> mkp e_ty (op acc (tn ?flag e))) e (f::l)
and tp ?flag : 'f AST.exp -> _ = function
| `Bexp e -> tb ?flag e
| `Eexp e -> te ?flag e
| `Nexp e -> tn ?flag e
| `Ref v -> (match symb_typ gd v with
| `Enum _ -> te ?flag (`Enum (mk_label v))
| t -> mkp (translate_typ gd v t) (Evar (ts gd v)))
| #cond as c -> trcond ?flag tb tp c
| #flag as e -> apply' tp e
in
tp e
(* --- *)
let decl_typs modul_name typdefs =
let qualify name = { qual = modul modul_name; name } in
fold_typdefs begin fun tname tdef (types, typ_symbs) ->
let name = qualify (Symb.to_string tname |> String.uncapitalize) in
match tdef with
| EnumDef labels, _ ->
let constrs = List.map (fun (l, _) ->
qualify (Symb.to_string (label_symb l))) labels in
(Ptype { t_name = name;
t_desc = Type_enum constrs;
t_loc = Location.no_location } :: types,
SMap.add tname name typ_symbs)
end typdefs ([], no_typ_symbs)
let decl_typs_from_module_itf modul_name =
(* Note we need to sort type declarations according to their respective
dependencies; hence the implicit topological traversal of the type
definitions. *)
let rec decl_types rem acc =
if QualEnv.is_empty rem then
acc
else
let t_name, tdef = QualEnv.choose rem in
let rem, acc = decl_typ t_name tdef rem acc in
decl_types rem acc
and decl_typ t_name tdef rem ((types, typ_symbs) as acc) =
let rem = QualEnv.remove t_name rem in
if t_name.qual <> modul_name then
rem, acc
else
let t_desc, rem, (types, typ_symbs) = match tdef with
| Tenum cl ->
(* Compiler_utils.info "declaring enum type %s" (shortname t_name); *)
let name = Symb.of_string (String.capitalize (shortname t_name)) in
(Type_enum cl, rem, (types, SMap.add name t_name typ_symbs))
| Talias (Tid tn) when tn.qual = t_name.qual -> (* declare deps 1st *)
(* Compiler_utils.info "declaring alias type %s" (shortname t_name); *)
let tdef = QualEnv.find tn rem in
let rem, acc = decl_typ tn tdef (QualEnv.remove tn rem) acc in
(Type_alias (Tid tn), rem, acc)
| Talias t ->
(* Compiler_utils.info "declaring alias type %s" (shortname t_name); *)
(Type_alias t, rem, acc)
| Tstruct _ ->
failwith (asprintf "Unexpected struct type `%s' in module interface"
(shortname t_name))
| Tabstract -> assert false
in
rem, (Ptype { t_name; t_desc; t_loc = Location.no_location } :: types,
typ_symbs)
in
Modules.open_module modul_name;
decl_types Modules.g_env.Modules.types ([], no_typ_symbs)
(* --- *)
let decl_var' gd v id t =
let vd = {
v_ident = id;
v_type = t;
v_linearity = Linearity.Ltop;
v_clock = Clocks.Cbase;
v_last = Var;
v_loc = Location.no_location;
} in
gd.env <- Env.add id vd gd.env;
gd.var_names <- SMap.add v id gd.var_names;
vd
let decl_ident gd id t =
let v = mk_symb (name id) in
decl_var' gd v id t
let decl_symb_acc gd v t acc =
let ident = ident_of_name (Symb.to_string v) in
let vd = decl_var' gd v ident (translate_typ gd v t) in
vd :: acc
(* --- *)
let translate_equ_acc gd v e acc =
{
eq_desc = Eeq (pat_of_var gd v, translate_expr gd e);
eq_stateful = false; (* ??? *)
eq_inits = Linearity.Lno_init;
eq_loc = Location.no_location; (* first-level flag of e: (flagof e) *)
} :: acc
(* --- *)
let block_of_func gd { fni_local_vars; fni_all_specs } =
let locals = SMap.fold (decl_symb_acc gd) fni_local_vars [] in
let equs = SMap.fold (translate_equ_acc gd) fni_all_specs [] in
{
b_local = locals;
b_equs = List.rev equs; (* for readability... *)
b_defnames = gd.env;
b_stateful = false;
b_loc = Location.no_location;
}
(* --- *)
let scmp a b = String.compare (Symb.to_string a) (Symb.to_string b)
let io_of_func gd { fni_io_vars } =
let i, o = List.fold_left (fun (i, o) { fnig_input_vars; fnig_output_vars } ->
(List.rev_append (SMap.bindings fnig_input_vars) i,
List.rev_append (SMap.bindings fnig_output_vars) o)) ([], []) fni_io_vars
in
let i = List.sort (fun (a, _) (b, _) -> scmp b a) i in (* rev. *)
let i = List.fold_left (fun acc (v, t) -> decl_symb_acc gd v t acc) [] i in
let o = List.sort (fun (a, _) (b, _) -> scmp b a) o in (* rev. *)
let o = List.fold_left (fun acc (v, t) -> decl_symb_acc gd v t acc) [] o in
i, o
(* --- *)
(* XXX /!\ Inputs omitted in the signature w.r.t the Controllable-Nbac model
should not appear anywhere in equations... *)
let io_of_func_match gd { node_inputs; node_outputs } =
let decl_arg = function
| { a_name = Some n; a_type = ty } -> decl_ident gd (ident_of_name n) ty
| _ -> failwith "Missing argument names in signature"
in
let i = List.map decl_arg node_inputs in
let o = List.map decl_arg node_outputs in
i, o
(* --- *)
let node_of_func gd ?node_sig n_name func =
enter_node n_name; (* ??? *)
let fi = gather_func_info func in
let n_input, n_output = match node_sig with
| None -> io_of_func gd fi
| Some s -> io_of_func_match gd s
in
let block = block_of_func gd fi in
Pnode {
n_name;
n_stateful = false;
n_unsafe = false;
n_input;
n_output;
n_contract = None; (* <- TODO: assume? *)
n_block = block;
n_loc = Location.no_location;
n_params = [];
n_param_constraints = [];
}
(* --- *)
let gen_func ?typ_symbs ?node_sig ~node_name func =
let { fn_typs; fn_decls } = func_desc func in
let fn_decls = (fn_decls :> ('f, 'f var_spec) decls) in
let typs, typ_symbs = match typ_symbs with
| None -> decl_typs node_name fn_typs
| Some typ_symbs -> [], typ_symbs
in
let gd = mk_gen_data node_name typ_symbs fn_decls fn_typs in
let node = node_of_func gd ?node_sig node_name func in
node :: typs
(* --- *)
let create_prog ?(open_modul = []) modul =
{
p_modname = modul;
p_opened = open_modul;
p_desc = [];
}
let add_to_prog e ({ p_desc } as p) =
(* TODO: check typ duplicates *)
{ p with p_desc = List.rev (e :: List.rev p_desc); }
(* --- *)

21
compiler/heptagon/hept_mapfold.ml
View file

@ -88,6 +88,7 @@ type 'a hept_it_funs = {
switch_handler : 'a hept_it_funs -> 'a -> switch_handler -> switch_handler * 'a;
var_dec : 'a hept_it_funs -> 'a -> var_dec -> var_dec * 'a;
last : 'a hept_it_funs -> 'a -> last -> last * 'a;
objective : 'a hept_it_funs -> 'a -> objective -> objective * 'a;
contract : 'a hept_it_funs -> 'a -> contract -> contract * 'a;
node_dec : 'a hept_it_funs -> 'a -> node_dec -> node_dec * 'a;
const_dec : 'a hept_it_funs -> 'a -> const_dec -> const_dec * 'a;
@ -216,7 +217,7 @@ and block_it funs acc b = funs.block funs acc b
and block funs acc b =
let b_local, acc = mapfold (var_dec_it funs) acc b.b_local in
let b_equs, acc = mapfold (eq_it funs) acc b.b_equs in
let b_defnames, acc =
let b_defnames, acc =
Idents.Env.fold
(fun v v_dec (env,acc) ->
let v, acc = var_ident_it funs.global_funs acc v in
@ -277,16 +278,21 @@ and last funs acc l = match l with
Last sto, acc
and objective_it funs acc o = funs.objective funs acc o
and objective funs acc o =
let e, acc = exp_it funs acc o.o_exp in
{ o with o_exp = e }, acc
and contract_it funs acc c = funs.contract funs acc c
and contract funs acc c =
let c_assume, acc = exp_it funs acc c.c_assume in
let c_enforce, acc = exp_it funs acc c.c_enforce in
let c_objectives, acc = mapfold (objective_it funs) acc c.c_objectives in
let c_assume_loc, acc = exp_it funs acc c.c_assume_loc in
let c_enforce_loc, acc = exp_it funs acc c.c_enforce_loc in
let c_block, acc = block_it funs acc c.c_block in
let c_controllables, acc = mapfold (var_dec_it funs) acc c.c_controllables in
{ c_assume = c_assume;
c_enforce = c_enforce;
c_objectives = c_objectives;
c_assume_loc = c_assume_loc;
c_enforce_loc = c_enforce_loc;
c_block = c_block;
@ -332,7 +338,7 @@ and program_desc_it funs acc pd =
with Fallback -> program_desc funs acc pd
and program_desc funs acc pd = match pd with
| Pconst cd -> let cd, acc = const_dec_it funs acc cd in Pconst cd, acc
| Ptype td -> pd, acc (* TODO types *)
| Ptype _td -> pd, acc (* TODO types *)
| Pnode n -> let n, acc = node_dec_it funs acc n in Pnode n, acc
let defaults = {
@ -350,6 +356,7 @@ let defaults = {
switch_handler = switch_handler;
var_dec = var_dec;
last = last;
objective = objective;
contract = contract;
node_dec = node_dec;
const_dec = const_dec;
@ -374,14 +381,10 @@ let defaults_stop = {
switch_handler = stop;
var_dec = stop;
last = stop;
objective = stop;
contract = stop;
node_dec = stop;
const_dec = stop;
program = stop;
program_desc = stop;
global_funs = Global_mapfold.defaults_stop }

29
compiler/heptagon/hept_printer.ml
View file

@ -28,18 +28,12 @@
(***********************************************************************)
(* The Heptagon printer *)
open Location
open Misc
open Names
open Idents
open Modules
open Static
open Format
open Global_printer
open Pp_tools
open Types
open Linearity
open Signature
open Heptagon
let iterator_to_string i =
@ -191,7 +185,7 @@ and print_app ff (app, args) =
match app.a_op with
| Etuple -> print_exp_tuple ff args
(* we need a special case for '*' and '*.' as printing (_*_) is incorrect *)
| Efun { name = n } when (n = "*" or n = "*.") ->
| Efun { name = n } when (n = "*" || n = "*.") ->
let a1, a2 = assert_2 args in
fprintf ff "@[%a@, %s@, %a@]" print_exp a1 n print_exp a2
| Efun ({ qual = Pervasives; name = n } as f) when (is_infix n) ->
@ -334,7 +328,7 @@ and print_sblock sep ff { b_local = v_list; b_equs = eqs } =
fprintf ff "@[<v>%a@,%a@]" (print_local_vars sep) v_list print_eq_list eqs
let rec print_type_def ff { t_name = name; t_desc = tdesc } =
let print_type_def ff { t_name = name; t_desc = tdesc } =
let print_type_desc ff = function
| Type_abs -> ()
| Type_alias ty -> fprintf ff " =@ %a" print_type ty
@ -344,13 +338,24 @@ let rec print_type_def ff { t_name = name; t_desc = tdesc } =
fprintf ff " =@ %a" (print_record print_field) f_ty_list in
fprintf ff "@[<2>type %a%a@]@." print_qualname name print_type_desc tdesc
let print_objective_kind ff = function
| Obj_enforce -> fprintf ff "enforce"
| Obj_reachable -> fprintf ff "reachable"
| Obj_attractive -> fprintf ff "attractive"
let print_objective ff o =
fprintf ff "@[<2>%a@ %a]"
print_objective_kind o.o_kind
print_exp o.o_exp
let print_contract ff { c_block = b;
c_assume = e_a; c_enforce = e_g;
c_controllables = c} =
fprintf ff "@[<v2>contract@\n%a@ assume %a@ enforce %a@ with (%a)@\n@]"
c_assume = e_a;
c_objectives = objs;
c_controllables = c} =
fprintf ff "@[<v2>contract@\n%a@ assume %a%a@ with (%a)@\n@]"
(print_block " do ") b
print_exp e_a
print_exp e_g
(print_list print_objective "@ " "@ " "") objs
print_vd_tuple c
let print_node ff

10
compiler/heptagon/hept_utils.ml
View file

@ -28,10 +28,7 @@
(***********************************************************************)
(* the internal representation *)
open Location
open Misc
open Names
open Idents
open Static
open Signature
open Types
open Linearity
@ -41,7 +38,7 @@ open Heptagon
(* Helper functions to create AST. *)
(* TODO : After switch, all mk_exp should take care of level_ck *)
let mk_exp desc ?(level_ck = Cbase) ?(ct_annot = None) ?(loc = no_location) ty ~linearity =
let mk_exp desc ?(level_ck = Clocks.Cbase) ?(ct_annot = None) ?(loc = no_location) ty ~linearity =
{ e_desc = desc; e_ty = ty; e_ct_annot = ct_annot; e_linearity = linearity;
e_level_ck = level_ck; e_loc = loc; }
@ -112,7 +109,7 @@ let mk_node
let vars_pat pat =
let rec _vars_pat locals acc = function
| Evarpat x ->
if (IdentSet.mem x locals) or (IdentSet.mem x acc)
if (IdentSet.mem x locals) || (IdentSet.mem x acc)
then acc
else IdentSet.add x acc
| Etuplepat pat_list -> List.fold_left (_vars_pat locals) acc pat_list
@ -122,7 +119,7 @@ let vars_pat pat =
a list of [var_dec]. *)
let rec vd_mem n = function
| [] -> false
| vd::l -> vd.v_ident = n or (vd_mem n l)
| vd::l -> vd.v_ident = n || (vd_mem n l)
let args_of_var_decs =
(* before the clocking the clock is wrong in the signature *)
@ -139,4 +136,3 @@ let signature_of_node n =
node_param_constraints = n.n_param_constraints;
node_external = false;
node_loc = n.n_loc }

19
compiler/heptagon/heptagon.ml
View file

@ -28,15 +28,12 @@
(***********************************************************************)
(* the internal representation *)
open Location
open Misc
open Names
open Idents
open Static
open Signature
open Types
open Linearity
open Clocks
open Initial
type state_name = name
@ -51,7 +48,7 @@ type exp = {
e_desc : desc;
e_ty : ty;
mutable e_ct_annot : ct option; (* exists when a source annotation exists *)
e_level_ck : ck; (* set by the switch pass, represents the activation base of the expression *)
e_level_ck : Clocks.ck; (* set by the switch pass, represents the activation base of the expression *)
mutable e_linearity : linearity;
e_loc : location }
@ -144,7 +141,7 @@ and var_dec = {
v_ident : var_ident;
v_type : ty;
v_linearity : linearity;
v_clock : ck;
v_clock : Clocks.ck;
v_last : last;
v_loc : location }
@ -161,9 +158,18 @@ and type_dec_desc =
| Type_enum of constructor_name list
| Type_struct of structure
type objective_kind =
| Obj_enforce
| Obj_reachable
| Obj_attractive
type objective =
{ o_kind : objective_kind;
o_exp : exp }
type contract = {
c_assume : exp;
c_enforce : exp;
c_objectives : objective list;
c_assume_loc : exp;
c_enforce_loc : exp;
c_controllables : var_dec list;
@ -217,4 +223,3 @@ and interface_desc =
| Itypedef of type_dec
| Iconstdef of const_dec
| Isignature of signature

2
compiler/heptagon/main/hept_compiler.ml
View file

@ -29,8 +29,6 @@
open Compiler_options
open Compiler_utils
open Location
open Global_printer
let pp p = if !verbose then Hept_printer.print stdout p

2
compiler/heptagon/main/hept_parser_scoper.ml
View file

@ -30,7 +30,6 @@
open Compiler_options
open Compiler_utils
open Location
open Global_printer
let pp p = if !verbose then Hept_printer.print stdout p
@ -72,4 +71,3 @@ let parse_interface modname lexbuf =
(* Convert the parse tree to Heptagon AST *)
let i = do_silent_pass "Scoping" Hept_scoping.translate_interface i in
i

2
compiler/heptagon/parsing/_tags
View file

@ -1 +1 @@
<hept_parser.ml>: pkg_menhirLib
<hept_parser.ml>: package(menhirLib)

2
compiler/heptagon/parsing/hept_lexer.mll
View file

@ -79,6 +79,8 @@ List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [
"contract", CONTRACT;
"assume", ASSUME;
"enforce", ENFORCE;
"reachable", REACHABLE;
"attractive", ATTRACTIVE;
"with", WITH;
"inlined",INLINED;
"when", WHEN;

26
compiler/heptagon/parsing/hept_parser.mly
View file

@ -28,10 +28,8 @@
(* *)
(***********************************************************************)
open Signature
open Location
open Names
open Types
open Linearity
open Hept_parsetree
@ -68,6 +66,8 @@ open Hept_parsetree
%token CONTRACT
%token ASSUME
%token ENFORCE
%token REACHABLE
%token ATTRACTIVE
%token WITH
%token WHEN WHENOT MERGE ON ONOT
%token INLINED
@ -263,13 +263,13 @@ node_params:
contract:
| /* empty */ {None}
| CONTRACT b=opt_block a=opt_assume e=opt_enforce w=opt_with
| CONTRACT b=opt_block a=opt_assume ol=objectives w=opt_with
{ Some{ c_block = b;
c_assume = a;
c_enforce = e;
c_objectives = ol;
c_assume_loc = mk_constructor_exp ptrue (Loc($startpos,$endpos));
c_enforce_loc = mk_constructor_exp ptrue (Loc($startpos,$endpos));
c_controllables = w } }
c_controllables = w } }
;
opt_block:
@ -282,9 +282,19 @@ opt_assume:
| ASSUME exp { $2 }
;
opt_enforce:
| /* empty */ { mk_constructor_exp ptrue (Loc($startpos,$endpos)) }
| ENFORCE exp { $2 }
objectives:
| /* empty */ { [] }
| o=objective ol=objectives { o :: ol }
;
objective:
| objective_kind exp { mk_objective $1 $2 }
;
objective_kind:
| ENFORCE { Obj_enforce }
| REACHABLE { Obj_reachable }
| ATTRACTIVE { Obj_attractive }
;
opt_with:

21
compiler/heptagon/parsing/hept_parsetree.ml
View file

@ -29,7 +29,6 @@
open Location
open Signature
(** var_names will be converted to idents *)
type var_name = Names.name
@ -64,9 +63,9 @@ and static_exp_desc =
| Sconstructor of constructor_name
| Sfield of field_name
| Stuple of static_exp list
| Sarray_power of static_exp * (static_exp list) (** power : 0^n : [0,0,0,0,0,..] *)
| Sarray of static_exp list (** [ e1, e2, e3 ] *)
| Srecord of (field_name * static_exp) list (** { f1 = e1; f2 = e2; ... } *)
| Sarray_power of static_exp * (static_exp list) (** power : 0^n : [[0,0,0,0,0,..]] *)
| Sarray of static_exp list (** [[ e1, e2, e3 ]] *)
| Srecord of (field_name * static_exp) list (** [{ f1 = e1; f2 = e2; ... }] *)
| Sop of fun_name * static_exp list (** defined ops for now in pervasives *)
type iterator_type =
@ -189,9 +188,18 @@ and type_desc =
| Type_enum of dec_name list
| Type_struct of (dec_name * ty) list
type objective_kind =
| Obj_enforce
| Obj_reachable
| Obj_attractive
type objective =
{ o_kind : objective_kind;
o_exp : exp }
type contract =
{ c_assume : exp;
c_enforce : exp;
c_objectives : objective list;
c_assume_loc : exp;
c_enforce_loc : exp;
c_controllables : var_dec list;
@ -294,6 +302,9 @@ let mk_block locals eqs loc =
{ b_local = locals; b_equs = eqs;
b_loc = loc; }
let mk_objective kind exp =
{ o_kind = kind; o_exp = exp }
let mk_const_dec id ty e loc =
{ c_name = id; c_type = ty; c_value = e; c_loc = loc }

11
compiler/heptagon/parsing/hept_parsetree_mapfold.ml
View file

@ -52,6 +52,7 @@ type 'a hept_it_funs = {
var_dec : 'a hept_it_funs -> 'a -> var_dec -> var_dec * 'a;
arg : 'a hept_it_funs -> 'a -> arg -> arg * 'a;
last : 'a hept_it_funs -> 'a -> last -> last * 'a;
objective : 'a hept_it_funs -> 'a -> objective -> objective * 'a;
contract : 'a hept_it_funs -> 'a -> contract -> contract * 'a;
node_dec : 'a hept_it_funs -> 'a -> node_dec -> node_dec * 'a;
const_dec : 'a hept_it_funs -> 'a -> const_dec -> const_dec * 'a;
@ -253,17 +254,21 @@ and last funs acc l = match l with
let sto, acc = optional_wacc (exp_it funs) acc sto in
Last sto, acc
and objective_it funs acc o = funs.objective funs acc o
and objective funs acc o =
let e, acc = exp_it funs acc o.o_exp in
{ o with o_exp = e }, acc
and contract_it funs acc c = funs.contract funs acc c
and contract funs acc c =
let c_assume, acc = exp_it funs acc c.c_assume in
let c_enforce, acc = exp_it funs acc c.c_enforce in
let c_objectives, acc = mapfold (objective_it funs) acc c.c_objectives in
let c_assume_loc, acc = exp_it funs acc c.c_assume_loc in
let c_enforce_loc, acc = exp_it funs acc c.c_enforce_loc in
let c_block, acc = block_it funs acc c.c_block in
{ c with
c_assume = c_assume;
c_enforce = c_enforce;
c_objectives = c_objectives;
c_assume_loc = c_assume_loc;
c_enforce_loc = c_enforce_loc;
c_block = c_block }
@ -382,6 +387,7 @@ let defaults = {
switch_handler = switch_handler;
var_dec = var_dec;
last = last;
objective = objective;
contract = contract;
node_dec = node_dec;
const_dec = const_dec;
@ -414,6 +420,7 @@ let defaults_stop = {
switch_handler = Global_mapfold.stop;
var_dec = Global_mapfold.stop;
last = Global_mapfold.stop;
objective = Global_mapfold.stop;
contract = Global_mapfold.stop;
node_dec = Global_mapfold.stop;
const_dec = Global_mapfold.stop;

47
compiler/heptagon/parsing/hept_scoping.ml
View file

@ -54,7 +54,6 @@
op<a1,a2> (a3) ==> op <a1> (a2,a3) ==> op (a1,a2,a3) *)
open Location
open Types
open Hept_parsetree
open Names
open Idents
@ -67,13 +66,13 @@ module Error =
struct
type error =
| Evar_unbound of name
| Equal_notfound of name*qualname
| Equal_notfound of name*Names.qualname
| Equal_unbound of name*name
| Enot_last of name
| Evariable_already_defined of name
| Econst_variable_already_defined of name
| Estatic_exp_expected
| Eredefinition of qualname
| Eredefinition of Names.qualname
| Elinear_type_no_memalloc
let message loc kind =
@ -124,7 +123,7 @@ open Error
let safe_add loc add n x =
try ((add n x) : unit)
with Modules.Already_defined -> message loc (Eredefinition n)
with Modules.Already_defined -> Error.message loc (Eredefinition n)
(** {3 Qualify when ToQ and check when Q according to the global env } *)
@ -156,30 +155,29 @@ let qualify_const local_const c = match c with
module Rename =
struct
open Error
include
(Map.Make (struct type t = string let compare = String.compare end))
(** Rename a var *)
let var loc env n =
try fst (find n env)
with Not_found -> message loc (Evar_unbound n)
with Not_found -> Error.message loc (Evar_unbound n)
(** Rename a last *)
let last loc env n =
try
let id, last = find n env in
if not last then message loc (Enot_last n) else id
with Not_found -> message loc (Evar_unbound n)
if not last then Error.message loc (Enot_last n) else id
with Not_found -> Error.message loc (Evar_unbound n)
(** Adds a name to the list of used names and idents. *)
let add_used_name env n =
add n (ident_of_name n, false) env
(** Add a var *)
let add_var loc env n =
if mem n env then message loc (Evariable_already_defined n)
if mem n env then Error.message loc (Evariable_already_defined n)
else
add n (ident_of_name n, false) env
(** Add a last *)
let add_last loc env n =
if mem n env then message loc (Evariable_already_defined n)
if mem n env then Error.message loc (Evariable_already_defined n)
else
add n (ident_of_name n, true) env
(** Add a var dec *)
@ -221,7 +219,7 @@ let build_const loc vd_list =
List.fold_left build NamesSet.empty vd_list
(** { 3 Translate the AST into Heptagon. } *)
(** {3 Translate the AST into Heptagon} *)
let translate_iterator_type = function
| Imap -> Heptagon.Imap
| Imapi -> Heptagon.Imapi
@ -234,9 +232,9 @@ let rec translate_static_exp se =
let se_d = translate_static_exp_desc se.se_loc se.se_desc in
Types.mk_static_exp Types.Tinvalid ~loc:se.se_loc se_d
with
| ScopingError err -> message se.se_loc err
| ScopingError err -> Error.message se.se_loc err
and translate_static_exp_desc loc ed =
and translate_static_exp_desc _loc ed =
let t = translate_static_exp in
match ed with
| Svar (Q q) -> Types.Svar q
@ -257,7 +255,7 @@ and translate_static_exp_desc loc ed =
let expect_static_exp e = match e.e_desc with
| Econst se -> translate_static_exp se
| _ -> message e.e_loc Estatic_exp_expected
| _ -> Error.message e.e_loc Estatic_exp_expected
let rec translate_type loc ty =
try
@ -271,7 +269,7 @@ let rec translate_type loc ty =
| Tinvalid -> Types.Tinvalid
)
with
| ScopingError err -> message loc err
| ScopingError err -> Error.message loc err
let rec translate_some_clock loc env ck = match ck with
| None -> Clocks.fresh_clock()
@ -294,7 +292,7 @@ let rec translate_exp env e =
Heptagon.e_level_ck = Clocks.Cbase;
Heptagon.e_ct_annot = Misc.optional (translate_ct e.e_loc env) e.e_ct_annot;
Heptagon.e_loc = e.e_loc }
with ScopingError(error) -> message e.e_loc error
with ScopingError(error) -> Error.message e.e_loc error
and translate_desc loc env = function
| Econst c -> Heptagon.Econst (translate_static_exp c)
@ -425,7 +423,7 @@ and translate_switch_handler loc env sh =
{ Heptagon.w_name = qualify_constrs sh.w_name;
Heptagon.w_block = fst (translate_block env sh.w_block) }
with
| ScopingError err -> message loc err
| ScopingError err -> Error.message loc err
and translate_var_dec env vd =
(* env is initialized with the declared vars before their translation *)
@ -445,6 +443,17 @@ and translate_last = function
| Last (None) -> Heptagon.Last None
| Last (Some e) -> Heptagon.Last (Some (expect_static_exp e))
let translate_objective_kind obj =
match obj with
| Obj_enforce -> Heptagon.Obj_enforce
| Obj_reachable -> Heptagon.Obj_reachable
| Obj_attractive -> Heptagon.Obj_attractive
let translate_objective env obj =
{ Heptagon.o_kind = translate_objective_kind obj.o_kind;
Heptagon.o_exp = translate_exp env obj.o_exp
}
let translate_contract env opt_ct =
match opt_ct with
| None -> None, env
@ -452,7 +461,7 @@ let translate_contract env opt_ct =
let env' = Rename.append env ct.c_controllables in
let b, env = translate_block env ct.c_block in
Some { Heptagon.c_assume = translate_exp env ct.c_assume;
Heptagon.c_enforce = translate_exp env ct.c_enforce;
Heptagon.c_objectives = List.map (translate_objective env) ct.c_objectives;
Heptagon.c_assume_loc = translate_exp env ct.c_assume_loc;
Heptagon.c_enforce_loc = translate_exp env ct.c_enforce_loc;
Heptagon.c_controllables = translate_vd_list env' ct.c_controllables;
@ -579,7 +588,7 @@ let translate_signature s =
let p, _ = params_of_var_decs Rename.empty s.sig_params in
let c = List.map translate_constrnt s.sig_param_constraints in
let sig_node =
Signature.mk_node
Signature.mk_node
~extern:s.sig_external s.sig_loc i o s.sig_stateful s.sig_unsafe p in
Check_signature.check_signature sig_node;
safe_add s.sig_loc add_value n sig_node;

5
compiler/heptagon/parsing/hept_static_scoping.ml
View file

@ -56,7 +56,7 @@ let qualify_pervasive q =
begin
try
match (Modules.qualify_value name) with
| { Names.qual = Names.Pervasives } as qn ->
| { Names.qual = Names.Pervasives } as qn ->
Q qn
| _ -> raise Not_static
with Not_found -> raise Not_static
@ -80,7 +80,7 @@ let exp funs local_const e =
let sed =
match e.e_desc with
| Evar n ->
(try Svar (Q (qualify_const local_const (ToQ n)))
(try Svar (Q (Hept_scoping.qualify_const local_const (ToQ n)))
with Error.ScopingError _ -> raise Not_static)
| Eapp({ a_op = Earray_fill; a_params = n_list }, [e]) ->
Sarray_power (assert_se e, List.map assert_se n_list)
@ -124,4 +124,3 @@ let interface i =
List.iter open_module i.i_opened;
let i, _ = Hept_parsetree_mapfold.interface_it funs Names.NamesSet.empty i in
i

14
compiler/heptagon/transformations/automata.ml
View file

@ -30,7 +30,6 @@
(* TODO deal correctly with [stateful] and [unsafe] *)
open Misc
open Types
open Names
open Idents
@ -38,7 +37,6 @@ open Heptagon
open Hept_utils
open Hept_mapfold
open Initial
open Modules
type var = S | NS | R | NR | PNR
let fresh = Idents.gen_fresh "automata"
@ -92,7 +90,7 @@ let intro_type type_name state_env =
Moore automatons doesn't have strong transitions,
Mealy automatons may have some. *)
let no_strong_transition state_handlers =
let handler no_strong { s_unless = l } = no_strong & (l = []) in
let handler no_strong { s_unless = l } = no_strong && (l = []) in
List.fold_left handler true state_handlers
@ -130,9 +128,9 @@ let translate_automaton v eq_list handlers =
in
let strong { s_state = n; s_unless = su } =
let rst_vd = mk_var_dec resetname (Tid Initial.pbool) Linearity.Ltop in
let rst_vd = mk_var_dec resetname (Tid Initial.pbool) ~linearity:Linearity.Ltop in
let defnames = Env.add resetname rst_vd Env.empty in
let state_vd = mk_var_dec statename tstatetype Linearity.Ltop in
let state_vd = mk_var_dec statename tstatetype ~linearity:Linearity.Ltop in
let defnames = Env.add statename state_vd defnames in
let st_eq = mk_simple_equation
(Etuplepat[Evarpat(statename); Evarpat(resetname)])
@ -142,9 +140,9 @@ let translate_automaton v eq_list handlers =
in
let weak { s_state = n; s_block = b; s_until = su } =
let nextrst_vd = mk_var_dec next_resetname (Tid Initial.pbool) Linearity.Ltop in
let nextrst_vd = mk_var_dec next_resetname (Tid Initial.pbool) ~linearity:Linearity.Ltop in
let defnames = Env.add next_resetname nextrst_vd b.b_defnames in
let nextstate_vd = mk_var_dec next_statename tstatetype Linearity.Ltop in
let nextstate_vd = mk_var_dec next_statename tstatetype ~linearity:Linearity.Ltop in
let defnames = Env.add next_statename nextstate_vd defnames in
let ns_eq = mk_simple_equation
(Etuplepat[Evarpat(next_statename); Evarpat(next_resetname)])
@ -195,7 +193,7 @@ let translate_automaton v eq_list handlers =
(mk_exp_fby_false (boolvar (next_resetname))) in
v, ns_switch_eq :: switch_eq :: pnr_eq :: eq_list
let rec eq funs (v, eq_list) eq =
let eq funs (v, eq_list) eq =
let eq, (v, eq_list) = Hept_mapfold.eq funs (v, eq_list) eq in
match eq.eq_desc with
| Eautomaton state_handlers ->

58
compiler/heptagon/transformations/boolean.ml
View file

@ -324,15 +324,15 @@ let rec on_list ck bl vtree =
| [], _ -> ck
| b::bl', VNode(v,t0,t1) ->
let (c,t) = if b then (ctrue,t1) else (cfalse,t0) in
on_list (Con(ck,c,v)) bl' t
on_list (Clocks.Con(ck,c,v)) bl' t
| _::_, Vempty -> failwith("on_list: non-coherent boolean list and tree")
let rec translate_ck env ck =
match ck with
| Cbase -> Cbase
| Cvar {contents = Clink(ck)} -> translate_ck env ck
| Cvar {contents = Cindex(_)} -> ck
| Con(ck,c,n) ->
| Clocks.Cbase -> Clocks.Cbase
| Clocks.Cvar {contents = Clink(ck)} -> translate_ck env ck
| Clocks.Cvar {contents = Cindex(_)} -> ck
| Clocks.Con(ck,c,n) ->
let ck = translate_ck env ck in
begin
try
@ -341,7 +341,7 @@ let rec translate_ck env ck =
on_list ck bl info.clocked_var
with Not_found ->
(* Boolean clock *)
Con(ck,c,n)
Clocks.Con(ck,c,n)
end
let rec translate_ct env ct =
@ -418,21 +418,21 @@ let rec when_list e bl vtree =
let ck = assert_ck e.e_ct_annot in
(* let e_v = mk_exp (Evar v) ~ct_annot:(Some(Ck(ck))) ty_bool in *)
let e_when = { e with
e_ct_annot = Some (Ck(Con(ck,c,v)));
e_ct_annot = Some (Ck(Clocks.Con(ck,c,v)));
e_desc = Ewhen(e,c,v) } in
when_list e_when bl' t
| _::_, Vempty -> failwith("when_list: non-coherent boolean list and tree")
let rec when_ck desc li ty ck =
match ck with
| Cbase | Cvar _ ->
| Clocks.Cbase | Clocks.Cvar _ ->
{ e_desc = desc;
e_level_ck = ck;
e_ct_annot = Some(Ck(ck));
e_linearity = li;
e_ty = ty;
e_loc = no_location }
| Con(ck',c,v) ->
| Clocks.Con(ck',c,v) ->
let e = when_ck desc li ty ck' in
(* let e_v = mk_exp (Evar v) ~ct_annot:(Some(Ck(ck'))) ty_bool in *)
{ e_desc = Ewhen(e,c,v);
@ -480,7 +480,7 @@ let rec base_value ck li ty =
let e_list = aux [] n in
{ e_desc = mk_tuple e_list;
e_ty = Tprod(List.map (fun _ -> ty_bool) e_list);
e_level_ck = Cbase;
e_level_ck = Clocks.Cbase;
e_ct_annot = Some(Ck(ck));
e_linearity = li;
e_loc = no_location }
@ -492,7 +492,7 @@ let rec base_value ck li ty =
let e_list = List.map (base_value ck li) ty_list in
{ e_desc = mk_tuple e_list;
e_ty = Tprod(List.map (fun e -> e.e_ty) e_list);
e_level_ck = Cbase;
e_level_ck = Clocks.Cbase;
e_ct_annot = Some(Ck(ck));
e_linearity = li;
e_loc = no_location;
@ -501,7 +501,7 @@ let rec base_value ck li ty =
let e = base_value ck li ty in
{ e_desc = Eapp((mk_app ~params:[se] Earray_fill), [e], None);
e_ty = Tarray(e.e_ty,se);
e_level_ck = Cbase;
e_level_ck = Clocks.Cbase;
e_ct_annot = Some(Ck(ck));
e_linearity = li;
e_loc = no_location;
@ -515,13 +515,13 @@ let rec merge_tree ck ty li e_map btree vtree =
let e = QualEnv.find name e_map in
{ e with e_ct_annot = Some(Ck(ck)) }
| Tree(t1,t2), VNode(v,vt1,vt2) ->
let e1 = merge_tree (Con(ck,cfalse,v)) ty li e_map t1 vt1
and e2 = merge_tree (Con(ck,ctrue,v)) ty li e_map t2 vt2
let e1 = merge_tree (Clocks.Con(ck,cfalse,v)) ty li e_map t1 vt1
and e2 = merge_tree (Clocks.Con(ck,ctrue,v)) ty li e_map t2 vt2
in
(* let e_v = mk_exp (Evar v) ~ct_annot:(Some(Ck(ck))) ty_bool in *)
{ e_desc = Emerge(v,[(cfalse,e1);(ctrue,e2)]);
e_ty = ty;
e_level_ck = Cbase;
e_level_ck = Clocks.Cbase;
e_ct_annot = Some(Ck(ck));
e_linearity = li;
e_loc = no_location }
@ -672,7 +672,7 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n =
e_ty = ty_bool;
e_linearity = var_from.v_linearity;
e_loc = no_location }
| _ckvar::l, Con(ck',c,v) ->
| _ckvar::l, Clocks.Con(ck',c,v) ->
(* assert v = _ckvar *)
let e = when_ck l ck' var in
(* let e_v = mk_exp (Evar v) ~ct_annot:(Some(Ck(ck'))) ty_bool in *)
@ -718,7 +718,7 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n =
| v1::v_list, [] ->
(* Root : no new id, only rec calls for sons *)
(* Build left son (ck on False(vi_...)) *)
let ck_0 = Con(ck,cfalse,v1) in
let ck_0 = Clocks.Con(ck,cfalse,v1) in
let acc_loc,acc_eq,t0 =
clocked_tree
(acc_loc,acc_eq)
@ -726,7 +726,7 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n =
("_0")
v_list ck_0 in
(* Build right son (ck on True(vi_...))*)
let ck_1 = Con(ck,ctrue,v1) in
let ck_1 = Clocks.Con(ck,ctrue,v1) in
let acc_loc,acc_eq,t1 =
clocked_tree
(acc_loc,acc_eq)
@ -750,7 +750,7 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n =
(mk_equation (Eeq(Evarpat(id),(when_ck acc_var ck vi))))
::acc_eq in
(* Build left son (ck on False(vi_...)) *)
let ck_0 = Con(ck,cfalse,id) in
let ck_0 = Clocks.Con(ck,cfalse,id) in
let acc_loc,acc_eq,t0 =
clocked_tree
(acc_loc,acc_eq)
@ -758,7 +758,7 @@ let var_dec_list (acc_vd,acc_loc,acc_eq) var_from n =
(suffix ^ "_0")
v_list ck_0 in
(* Build right son (ck on True(vi_...))*)
let ck_1 = Con(ck,ctrue,id) in
let ck_1 = Clocks.Con(ck,ctrue,id) in
let acc_loc,acc_eq,t1 =
clocked_tree
(acc_loc,acc_eq)
@ -796,7 +796,7 @@ let buildenv_var_dec (acc_vd,acc_loc,acc_eq,env) ({v_type = ty} as v) =
v info.ty_nb_var in
let env =
Env.add
v.v_ident
v.v_ident
{ var_enum = info;
var_list = vl;
clocked_var = t }
@ -850,11 +850,21 @@ and translate_eqs env eq_list =
(fun context eq ->
translate_eq env context eq) ([],[]) eq_list
let translate_objectives env context objs =
let context, objs =
List.fold_left
(fun (context,ol) o ->
let context, e = translate env context o.o_exp in
context, { o with o_exp = e } :: ol)
(context, [])
objs in
context, List.rev objs
let translate_contract env contract =
match contract with
| None -> None, env
| Some { c_assume = e_a;
c_enforce = e_g;
c_objectives = objs;
c_assume_loc = e_a_loc;
c_enforce_loc = e_g_loc;
c_controllables = cl;
@ -866,14 +876,14 @@ let translate_contract env contract =
= translate_block env cl_loc cl_eq b in
let context, e_a = translate env' (v,eqs) e_a in
let context, e_a_loc = translate env' context e_a_loc in
let context, e_g = translate env' context e_g in
let context, objs = translate_objectives env' context objs in
let context, e_g_loc = translate env' context e_g_loc in
let (d_list,eq_list) = context in
Some { c_block = { b with
b_local = d_list;
b_equs = eq_list };
c_assume = e_a;
c_enforce = e_g;
c_objectives = objs;
c_assume_loc = e_a_loc;
c_enforce_loc = e_g_loc;
c_controllables = cl },

7
compiler/heptagon/transformations/completion.ml
View file

@ -28,9 +28,7 @@
(***********************************************************************)
(* complete partial definitions with [x = last(x)] *)
open Misc
open Heptagon
open Global_mapfold
open Hept_utils
open Hept_mapfold
open Idents
@ -67,7 +65,7 @@ let funs_collect =
(* adds an equation [x = last(x)] for every partially defined variable *)
(* in a control structure *)
let complete_with_last defined_names local_defined_names eq_list =
let last n vd = mk_exp (Elast n) vd.v_type Linearity.Ltop in
let last n vd = mk_exp (Elast n) vd.v_type ~linearity:Linearity.Ltop in
let equation n vd eq_list =
(mk_equation (Eeq(Evarpat n, last n vd)))::eq_list in
let d = Env.diff defined_names local_defined_names in
@ -86,11 +84,10 @@ let eqdesc funs _ ed = match ed with
let ed, defnames =
Hept_mapfold.eqdesc funs_collect Env.empty ed in
(* add missing defnames *)
let ed, defnames = Hept_mapfold.eqdesc funs defnames ed in
let ed, _defnames = Hept_mapfold.eqdesc funs defnames ed in
ed, Env.empty
| _ -> raise Errors.Fallback
let funs = { Hept_mapfold.defaults with eqdesc = eqdesc; block = block; }
let program p = let p, _ = program_it funs Env.empty p in p

50
compiler/heptagon/transformations/contracts.ml
View file

@ -47,6 +47,17 @@ open Linearity
let fresh = Idents.gen_var "contracts"
let not_exp e = mk_exp (mk_op_app (Efun pnot) [e]) tbool ~linearity:Ltop
let (&&&) e1 e2 = mk_exp (mk_op_app (Efun pand) [e1;e2]) tbool ~linearity:Ltop
let (|||) e1 e2 = mk_exp (mk_op_app (Efun por) [e1;e2]) tbool ~linearity:Ltop
let (=>) e1 e2 = (not_exp e1) ||| e2
let var_exp v = mk_exp (Evar v) tbool ~linearity:Ltop
let true_exp = mk_exp (Econst (mk_static_bool true)) tbool ~linearity:Ltop
let mk_unique_node nd =
let mk_bind vd =
let id = fresh (Idents.name vd.v_ident) in
@ -93,7 +104,7 @@ let mk_unique_node nd =
let subst_contract funs subst c =
let c_block, subst' = subst_contract_block funs subst c.c_block in
let c_assume, subst' = exp_it funs subst' c.c_assume in
let c_enforce, subst' = exp_it funs subst' c.c_enforce in
let c_objectives, _subst' = mapfold (objective_it funs) subst' c.c_objectives in
let subst =
List.fold_left
(fun subst vd ->
@ -104,7 +115,7 @@ let mk_unique_node nd =
let c_assume_loc = c.c_assume_loc in
let c_enforce_loc = c.c_enforce_loc in
{ c_assume = c_assume;
c_enforce = c_enforce;
c_objectives = c_objectives;
c_assume_loc = c_assume_loc;
c_enforce_loc = c_enforce_loc;
c_block = c_block;
@ -224,9 +235,22 @@ let exp funs (env, newvars, newequs, cont_vars, contracts) exp =
(* variable declarations for assume/guarantee *)
let vd_a = mk_vd_bool v_a in
let vd_g = mk_vd_bool v_g in
(* Build an expression composed of every "enforce" objective of the contract *)
let rec build_enforce o_list =
match o_list with
[] -> true_exp
| [o] -> o.o_exp
| o :: l -> o.o_exp &&& (build_enforce l) in
(* Currently, only the enforce part is used for modularity *)
let enforce_exp =
build_enforce
(List.filter (fun o -> o.o_kind = Obj_enforce) ci.c_objectives) in
(* equations for assume/guarantee *)
let eq_a = mk_equation (Eeq (Evarpat v_a, ci.c_assume)) in
let eq_g = mk_equation (Eeq (Evarpat v_g, ci.c_enforce)) in
let eq_g = mk_equation (Eeq (Evarpat v_g, enforce_exp)) in
let newvars = ni.n_input @ ci.c_block.b_local @ ni.n_output @ newvars
@ -261,26 +285,15 @@ let block funs (env, newvars, newequs, cont_vars, contracts) blk =
let defnames = List.fold_left
(fun env v -> Env.add v.v_ident v env)
blk.b_defnames cont_vars' in
({ blk with
({ blk with
b_local = newvars' @ blk.b_local;
b_equs = newequs' @ blk.b_equs;
b_defnames = defnames;
},
(env, newvars, newequs, (cont_vars @ cont_vars'), contracts'))
let not_exp e = mk_exp (mk_op_app (Efun pnot) [e]) tbool ~linearity:Ltop
let (&&&) e1 e2 = mk_exp (mk_op_app (Efun pand) [e1;e2]) tbool ~linearity:Ltop
let (|||) e1 e2 = mk_exp (mk_op_app (Efun por) [e1;e2]) tbool ~linearity:Ltop
let (=>) e1 e2 = (not_exp e1) ||| e2
let var_exp v = mk_exp (Evar v) tbool ~linearity:Ltop
let true_exp = mk_exp (Econst (mk_static_bool true)) tbool ~linearity:Ltop
let node_dec funs (env, newvars, newequs, cont_vars, contracts) nd =
let nd, (env, newvars, newequs, cont_vars, contracts) =
let nd, (env, newvars, newequs, _cont_vars, contracts) =
Hept_mapfold.node_dec funs (env, newvars, newequs, cont_vars, contracts) nd in
(* Build assume and guarantee parts from contract list (list of
@ -308,7 +321,7 @@ let node_dec funs (env, newvars, newequs, cont_vars, contracts) nd =
c,[] -> c
| None,_::_ ->
Some { c_assume = true_exp;
c_enforce = true_exp;
c_objectives = [];
c_assume_loc = assume_loc;
c_enforce_loc = enforce_loc;
c_controllables = [];
@ -330,10 +343,9 @@ let node_dec funs (env, newvars, newequs, cont_vars, contracts) nd =
let program p =
let funs =
{ defaults with exp = exp; block = block; node_dec = node_dec; eq = eq; } in
let (p, (_, newvars, newequs, cont_vars, contracts)) =
let (p, (_, newvars, newequs, _cont_vars, contracts)) =
Hept_mapfold.program funs (QualEnv.empty, [], [], [], []) p in
assert (newvars = []);
assert (newequs = []);
assert (contracts = []);
p

8
compiler/heptagon/transformations/itfusion.ml
View file

@ -56,7 +56,7 @@ let anon_nodes = ref QualEnv.empty
let add_anon_node inputs outputs locals eqs =
let n = mk_fresh_node_name () in
let b = mk_block ~locals:locals eqs in
let nd = mk_node ~input:inputs ~output:outputs n b in
let nd = Hept_utils.mk_node ~input:inputs ~output:outputs n b in
anon_nodes := QualEnv.add n nd !anon_nodes;
n
@ -95,7 +95,7 @@ let tuple_of_vd_list l =
mk_exp (Eapp (mk_app Etuple, el, None)) ty ~linearity:lin
let vd_of_arg ad =
mk_var_dec (fresh_vd_of_arg ad) ad.a_type ad.a_linearity
mk_var_dec (fresh_vd_of_arg ad) ad.a_type ~linearity:ad.a_linearity
(** @return the lists of inputs and outputs (as var_dec) of
an app object. *)
@ -150,7 +150,7 @@ let edesc funs acc ed =
let new_inp, e, acc_eq_list = mk_call g acc_eq_list in
new_inp @ inp, acc_eq_list, e::largs, local_args @ args, true
| _ ->
let vd = mk_var_dec (fresh_var ()) e.e_ty e.e_linearity in
let vd = mk_var_dec (fresh_var ()) e.e_ty ~linearity:e.e_linearity in
vd::inp, acc_eq_list, (exp_of_vd vd)::largs, e::args, b
in
@ -162,7 +162,7 @@ let edesc funs acc ed =
let _, outp = get_node_inp_outp f in
let f_out_type = type_of_vd_list outp in
let f_out_lin = linearity_of_vd_list outp in
let call = mk_exp (Eapp(f, largs, None)) f_out_type f_out_lin in
let call = mk_exp (Eapp(f, largs, None)) f_out_type ~linearity:f_out_lin in
let eq = mk_equation (Eeq(pat_of_vd_list outp, call)) in
(* create the lambda *)
let anon = mk_app

5
compiler/heptagon/transformations/last.ml
View file

@ -46,10 +46,11 @@ let last (eq_list, env, v) { v_ident = n; v_type = t; v_linearity = lin; v_last
let eq =
mk_equation (Eeq (Evarpat lastn,
mk_exp (Epre (default,
mk_exp (Evar n) t Linearity.Ltop)) t lin)) in
mk_exp (Evar n) t ~linearity:Linearity.Ltop))
t ~linearity:lin)) in
eq:: eq_list,
Env.add n lastn env,
(mk_var_dec lastn t lin) :: v
(mk_var_dec lastn t ~linearity:lin) :: v
let extend_env env v = List.fold_left last ([], env, []) v

34
compiler/heptagon/transformations/normalize.ml
View file

@ -27,14 +27,11 @@
(* *)
(***********************************************************************)
open Misc
open Names
open Idents
open Location
open Heptagon
open Hept_utils
open Hept_mapfold
open Types
open Clocks
open Linearity
open Format
@ -86,7 +83,7 @@ let flatten_e_list l =
let equation (d_list, eq_list) e =
let add_one_var ty lin d_list =
let n = Idents.gen_var "normalize" "v" in
let d_list = (mk_var_dec n ty lin) :: d_list in
let d_list = (mk_var_dec n ty ~linearity:lin) :: d_list in
n, d_list
in
match e.e_ty with
@ -102,7 +99,7 @@ let equation (d_list, eq_list) e =
let pat_list = List.map (fun n -> Evarpat n) var_list in
let eq_list = (mk_equation (Eeq (Etuplepat pat_list, e))) :: eq_list in
let e_list = Misc.map3
(fun n ty lin -> mk_exp (Evar n) ty lin) var_list ty_list lin_list in
(fun n ty lin -> mk_exp (Evar n) ty ~linearity:lin) var_list ty_list lin_list in
let e = Eapp(mk_app Etuple, e_list, None) in
(d_list, eq_list), e
| _ ->
@ -111,7 +108,7 @@ let equation (d_list, eq_list) e =
(d_list, eq_list), Evar n
(* [(e1,...,ek) when C(n) = (e1 when C(n),...,ek when C(n))] *)
let rec whenc context e c n e_orig =
let whenc context e c n e_orig =
let when_on_c c n context e =
(* If memalloc is activated, there cannot be a stateful exp inside a when. Indeed,
the expression inside the when will be called on a fast rhythm and write its result
@ -178,6 +175,18 @@ let rec translate kind context e =
merge context e n tag_e_list
| Eapp({ a_op = Eifthenelse }, [e1; e2; e3], _) ->
ifthenelse context e e1 e2 e3
(* XXX Huge hack to avoid comparing tuples... (temporary, until this is
fixed where it should be) *)
| Eapp({ a_op = (Efun ({ Names.qual = Names.Pervasives; Names.name = "=" }) as op)},
[x;y], reset) when is_list x ->
let x = e_to_e_list x and y = e_to_e_list y in
let xy = List.fold_left2 (fun acc x y ->
let cmp = mk_exp (mk_op_app op [x; y] ~reset) Initial.tbool ~linearity:Ltop in
mk_exp (mk_op_app (Efun Initial.pand) [acc; cmp] ~reset) Initial.tbool ~linearity:Ltop)
dtrue
x y
in
translate kind context xy
| Eapp(app, e_list, r) ->
let context, e_list = translate_list ExtValue context e_list in
context, { e with e_desc = Eapp(app, flatten_e_list e_list, r) }
@ -268,7 +277,7 @@ and merge context e x c_e_list =
let context, e = translate ExtValue context e in
(tag, e), context
in
let rec mk_merge x c_list e_lists =
let mk_merge x c_list e_lists =
let ty = (List.hd (List.hd e_lists)).e_ty in
let lin = (List.hd (List.hd e_lists)).e_linearity in
let rec build_c_e_list c_list e_lists =
@ -347,7 +356,7 @@ and translate_eq_list d_list eq_list =
(fun context eq -> translate_eq context eq)
(d_list, []) eq_list
let eq funs context eq =
let eq _funs context eq =
let context = translate_eq context eq in
eq, context
@ -361,13 +370,18 @@ let contract funs context c =
(* Non-void context could mean lost equations *)
assert (void_context=([],[]));
let context, e_a = translate ExtValue ([],[]) c.c_assume in
let context, e_e = translate ExtValue context c.c_enforce in
let context, e_e =
mapfold_right
(fun o context ->
let context, e = translate ExtValue context o.o_exp in
context, { o with o_exp = e })
c.c_objectives context in
let local_context, e_a_loc = translate ExtValue ([],[]) c.c_assume_loc in
let local_context, e_e_loc = translate ExtValue local_context c.c_enforce_loc in
let (d_list, eq_list) = context in
{ c with
c_assume = e_a;
c_enforce = e_e;
c_objectives = e_e;
c_assume_loc = e_a_loc;
c_enforce_loc = e_e_loc;
c_block = { b with

3
compiler/heptagon/transformations/present.ml
View file

@ -34,7 +34,7 @@ open Hept_mapfold
let translate_present_handlers handlers cont =
let translate_present_handler { p_cond = e; p_block = b } cont =
let stateful = b.b_stateful or cont.b_stateful in
let stateful = b.b_stateful || cont.b_stateful in
mk_block ~stateful:stateful ~defnames:b.b_defnames
[mk_switch_equation e
[{ w_name = Initial.ptrue; w_block = b };
@ -52,4 +52,3 @@ let program p =
let funs = { Hept_mapfold.defaults with eqdesc = eqdesc } in
let p, _ = Hept_mapfold.program_it funs false p in
p

14
compiler/heptagon/transformations/reset.ml
View file

@ -31,7 +31,6 @@
(* REQUIRES automaton stateful present *)
open Misc
open Idents
open Heptagon
open Hept_utils
open Types
@ -77,7 +76,16 @@ let default e =
| _ -> None
let edesc funs ((res,_) as acc) ed = match ed with
let edesc funs ((res,_) as acc) ed =
match ed with
| Epre (Some c, e) ->
let e,_ = Hept_mapfold.exp_it funs acc e in
(match res with
| None -> Epre(Some c, e)
| Some _ ->
ifres res
(mk_exp (Econst c) (e.e_ty) ~linearity:Linearity.Ltop)
{ e with e_desc = Epre(Some c,e) }), acc
| Efby (e1, e2) ->
let e1,_ = Hept_mapfold.exp_it funs acc e1 in
let e2,_ = Hept_mapfold.exp_it funs acc e2 in
@ -117,7 +125,7 @@ let block funs (res,_) b =
(* Transform reset blocks in blocks with reseted exps,
create a var to store the reset condition evaluation if not already a var. *)
let eqdesc funs (res,stateful) = function
| Ereset(b, ({ e_desc = Evar x } as e)) ->
| Ereset(b, ({ e_desc = Evar _ } as e)) ->
let r = if stateful then merge_resets res (Some e) else res in
let b, _ = Hept_mapfold.block_it funs (r,stateful) b in
Eblock(b), (res,stateful)

11
compiler/heptagon/transformations/switch.ml
View file

@ -59,7 +59,6 @@ with one defined var y ( defnames = {y} ) and used var x
open Misc
open Heptagon
open Hept_utils
open Hept_mapfold
@ -81,7 +80,6 @@ module Env = struct
open Idents
open Names
open Clocks
type t = Base | Level of ck * IdentSet.t * t
@ -152,7 +150,7 @@ let level_up defnames constr h =
let add_to_locals vd_env locals h =
let add_one n nn (locals,vd_env) =
let orig_vd = Idents.Env.find n vd_env in
let vd_nn = mk_var_dec nn orig_vd.v_type orig_vd.v_linearity in
let vd_nn = mk_var_dec nn orig_vd.v_type ~linearity:orig_vd.v_linearity in
vd_nn::locals, Idents.Env.add vd_nn.v_ident vd_nn vd_env
in
fold add_one h (locals, vd_env)
@ -197,7 +195,7 @@ let eqdesc funs (vd_env,env,h) eqd = match eqd with
(* create a clock var corresponding to the switch condition [e] *)
let ck = fresh_clock_id () in
let e, (vd_env,env,h) = exp_it funs (vd_env,env,h) e in
let locals = [mk_var_dec ck e.e_ty e.e_linearity] in
let locals = [mk_var_dec ck e.e_ty ~linearity:e.e_linearity] in
let equs = [mk_equation (Eeq (Evarpat ck, e))] in
(* typing have proved that defined variables are the same among states *)
@ -246,8 +244,3 @@ let program p =
exp = exp; eq = eq; eqdesc = eqdesc } in
let p, _ = program_it funs (Idents.Env.empty,Env.Base,Rename.empty) p in
p

260
compiler/main/ctrl2ept.ml Normal file
View file

@ -0,0 +1,260 @@
open Format
open Filename
open CtrlNbac
open Compiler_utils
open Compiler_options
(* -------------------------------------------------------------------------- *)
let report_msgs ?filename =
let report_msg = Parser.Reporting.report_msg ?filename err_formatter in
List.iter begin function
| #CtrlNbac.Parser.msg as msg -> report_msg msg
| `TError info -> report_msg (`MError info)
end
let abort ?filename n msgs =
report_msgs ?filename msgs;
error "Aborting due to errors in %s" n;
exit 1
(* -------------------------------------------------------------------------- *)
(** File extensions officially understood by the tool, with associated input
types. *)
let ityps_alist = [
"ctrlf", `Ctrlf; "cf", `Ctrlf;
"ctrls", `Ctrlf; "cs", `Ctrlf; (* No need to discriminate between weaved and
split functions (for now). *)
]
(** name of official input types as understood by the tool. *)
let ityps = List.map fst ityps_alist
let set_input_type r t =
try r := Some (List.assoc t ityps_alist) with
| Not_found -> raise (Arg.Bad (asprintf "Unknown input file type: `%s'" t))
let inputs = ref []
let output = ref ""
let input_type = ref None
let node = ref ""
exception Help
let usage = "Usage: ctrl2ept [options] { [-i] <filename> | -n <node> } \
[ -- { <filename> } ]"
let print_vers () =
fprintf err_formatter "ctrl2ept, version %s (compiled on %s)@." version date;
exit 0
let anon x = inputs := x :: !inputs
let it = Arg.Symbol (ityps, set_input_type input_type)
let options = Arg.align
[
"-i", Arg.String anon, "<file> Input file (`-' means standard input)";
"-input-type", it, " Input file type";
"--input-type", it, "";
"-o", Arg.Set_string output, "<file> Select output file (`-' means \
standard output)";
"-n", Arg.Set_string node, "<node> Select base input node";
"--", Arg.Rest anon, " Treat all remaining arguments as input files";
"-where", Arg.Unit locate_stdlib, doc_locate_stdlib;
"-stdlib", Arg.String set_stdlib, doc_stdlib;
"-v",Arg.Set verbose, " Set verbose mode";
"-version", Arg.Unit print_vers, " Print the version of the compiler";
"--version", Arg.Unit print_vers, "";
"-h", Arg.Unit (fun _ -> raise Help), "";
]
(* -------------------------------------------------------------------------- *)
type out =
{
out_mult: bool; (* Are multiple calls to `out_exec' allowed? *)
out_exec: string -> out_channel * (unit -> unit); (* oc * close *)
}
(* --- *)
let mk_oc basename =
{
out_exec = (fun ext ->
let filename = asprintf "%s%s" basename ext in
let oc = open_out filename in
info "Outputting into `%s'…" filename;
oc, (fun () -> flush oc; close_out oc));
out_mult = true;
}
let mk_oc' filename =
{
out_exec = (fun _ ->
let oc = open_out filename in
info "Outputting into `%s'…" filename;
oc, (fun () -> flush oc; close_out oc));
out_mult = false;
}
let mk_std_oc =
{
out_exec = (fun _ ->
info "Outputting onto standard output…";
stdout, (fun () -> flush stdout));
out_mult = true;
}
(* --- *)
(** Parses the given input file. *)
let parse_input ?filename (parse: ?filename:string -> _) =
try
let s, n, msgs = parse ?filename () in
report_msgs ?filename msgs;
s, n
with
| CtrlNbac.Parser.Error (n, msgs) -> abort ?filename n msgs
(* -------------------------------------------------------------------------- *)
exception Error of string
let parse_n_gen_ept_node ?filename ?node_name ?node_sig ?typ_symbs () =
let name, func = parse_input ?filename CtrlNbac.Parser.Unsafe.parse_func in
let node_name = match node_name with Some n -> n
| None -> match name with None -> assert false
| Some n -> Names.local_qn (n ^ "_ctrlr")
in
name, CtrlNbacAsEpt.gen_func ?typ_symbs ~node_name ?node_sig func
let handle_ctrlf ?filename mk_oc =
let _, decls = parse_n_gen_ept_node ?filename () in
let prog = CtrlNbacAsEpt.create_prog Names.LocalModule in (* don't care? *)
let prog = List.fold_right CtrlNbacAsEpt.add_to_prog decls prog in
let oc, close = mk_oc.out_exec "ept" in
Hept_printer.print oc prog;
close ()
(* -------------------------------------------------------------------------- *)
let parse_nodename nn = try Names.qualname_of_string nn with
| Exit -> raise (Error (sprintf "Invalid node name: `%s'" nn))
let output_prog prog modul =
Modules.select modul;
let filename = String.uncapitalize (Names.modul_to_string modul) ^ ".ept" in
let oc = open_out filename in
info "Outputting into `%s'…" filename;
Hept_printer.print oc prog;
close_out oc
let input_function prog typ_symbs filename node_name node_sig =
info "Reading function from `%s'…" filename;
let _, decls = parse_n_gen_ept_node ~filename ~node_name ~node_sig ~typ_symbs () in
(* XXX: check types are also in signature? actually, we only use the types
declared in the signature instead, as long as the controller synthesis tool
does not introduce new types. *)
List.fold_right CtrlNbacAsEpt.add_to_prog decls prog
let try_ctrlf typ_symbs nn prog =
let node_name = Ctrln_utils.controller_node nn in
if Modules.check_value node_name then
let filename = Ctrln_utils.ctrlf_for_node nn in
let node_sig = Modules.find_value node_name in
input_function prog typ_symbs filename node_name node_sig
else
raise (Error "Unable to load any controller function.")
let try_ctrls typ_symbs nn prog =
let rec try_ctrls num prog =
let node_name = Ctrln_utils.controller_node ~num nn in
if Modules.check_value node_name then
let filename = Ctrln_utils.ctrls_for_node nn num in
if num = 0 && not (Sys.file_exists filename) then
raise Exit; (* abort *)
let node_sig = Modules.find_value node_name in
let prog = input_function prog typ_symbs filename node_name node_sig in
try_ctrls (succ num) prog
else
prog
in
try_ctrls 0 prog
let handle_node arg =
let nn = parse_nodename arg in
let mo = Names.modul nn in
if mo = Names.Pervasives || mo = Names.LocalModule then
raise (Error (sprintf "Invalid node specification: `%s'." arg));
Modules.open_module Names.Pervasives;
info "Loading module of controllers for node %s…" (Names.fullname nn);
let om = Ctrln_utils.controller_modul mo in
info "Translating type declarations of module %s…" (Names.modul_to_string om);
let typs, typ_symbs = CtrlNbacAsEpt.decl_typs_from_module_itf om in
let prog = CtrlNbacAsEpt.create_prog ~open_modul:[ ] om in
let prog = List.fold_right CtrlNbacAsEpt.add_to_prog typs prog in
let prog = try try_ctrls typ_symbs nn prog with
| Exit -> try_ctrlf typ_symbs nn prog in
output_prog prog om
(* -------------------------------------------------------------------------- *)
let ityp_name_n_handle = function
(* | `Ctrln -> "node", handle_ctrln *)
| `Ctrlf -> "function", handle_ctrlf
(* | `Ctrlr -> "predicate", handle_ctrlr *)
let guesstyp_n_output filename =
try
let typ = match !input_type with
| Some t -> t
| None -> snd (List.find (fun (suff, _) -> check_suffix filename suff)
ityps_alist)
in
let basename_extra = match typ with
| `Ctrlf -> "_ctrlr"
in
typ,
(match !output with
| "-" -> mk_std_oc
| "" -> (try chop_extension filename ^ basename_extra |> mk_oc with
| Invalid_argument _ when filename <> "" -> mk_oc filename
| Invalid_argument _ -> mk_std_oc)
| o -> mk_oc' o)
with
| Not_found ->
raise (Arg.Bad (sprintf "Cannot guess input type of `%s'" filename))
let handle_input_file filename =
let ityp, mk_oc = guesstyp_n_output filename in
let itypname, handle = ityp_name_n_handle ityp in
info "Reading %s from `%s'…" itypname filename;
handle ~filename mk_oc
let handle_input_stream = function
| None ->
info "Reading function from standard input…";
handle_ctrlf mk_std_oc
| Some ityp ->
let itypname, handle = ityp_name_n_handle ityp in
info "Reading %s from standard input…" itypname;
handle mk_std_oc
(** [main] function to be launched *)
let main () =
Arg.parse options anon usage;
match List.rev !inputs with
| [] when !node <> "" -> handle_node !node
| [] -> handle_input_stream !input_type
| lst -> (if !node <> "" then handle_node !node;
List.iter handle_input_file lst)
(* -------------------------------------------------------------------------- *)
(** Launch the [main] *)
let _ =
(* CtrlNbac.Symb.reset (); <- not needed as we have only one input file. *)
try
main ()
with
| Help -> Arg.usage options usage
| Errors.Error -> error "aborted."; exit 2
| Error s | Arg.Bad s | Sys_error s -> error "%s" s; exit 2

23
compiler/main/hept2mls.ml
View file

@ -33,14 +33,11 @@ open Location
open Misc
open Names
open Idents
open Static
open Types
open Clocks
open Format
open Minils
open Mls_utils
open Signature
module Error =
struct
@ -84,7 +81,7 @@ let translate_iterator_type = function
| Heptagon.Ifoldi -> Ifoldi
| Heptagon.Imapfold -> Imapfold
let rec translate_op = function
let translate_op = function
| Heptagon.Eifthenelse -> Eifthenelse
| Heptagon.Efun f -> Efun f
| Heptagon.Enode f -> Enode f
@ -111,7 +108,7 @@ let translate_app app =
let mk_extvalue e w =
let clock = match e.Heptagon.e_ct_annot with
| None -> fresh_clock ()
| Some ct -> assert_1 (unprod ct)
| Some ct -> assert_1 (Clocks.unprod ct)
in
mk_extvalue ~loc:e.Heptagon.e_loc ~linearity:e.Heptagon.e_linearity
~ty:e.Heptagon.e_ty ~clock:clock w
@ -180,7 +177,7 @@ let rec translate_pat = function
| Heptagon.Evarpat(n) -> Evarpat n
| Heptagon.Etuplepat(l) -> Etuplepat (List.map translate_pat l)
let rec translate_eq { Heptagon.eq_desc = desc; Heptagon.eq_loc = loc } =
let translate_eq { Heptagon.eq_desc = desc; Heptagon.eq_loc = loc } =
match desc with
| Heptagon.Eeq(p, e) ->
begin match e.Heptagon.e_desc with
@ -193,20 +190,29 @@ let rec translate_eq { Heptagon.eq_desc = desc; Heptagon.eq_loc = loc } =
| Heptagon.Epresent _ | Heptagon.Eautomaton _ | Heptagon.Ereset _ ->
Error.message loc Error.Eunsupported_language_construct
let translate_objective o =
let e = translate_extvalue o.Heptagon.o_exp in
let kind =
match o.Heptagon.o_kind with
| Heptagon.Obj_enforce -> Obj_enforce
| Heptagon.Obj_reachable -> Obj_reachable
| Heptagon.Obj_attractive -> Obj_attractive in
{ o_kind = kind; o_exp = e }
let translate_contract contract =
match contract with
| None -> None
| Some { Heptagon.c_block = { Heptagon.b_local = v;
Heptagon.b_equs = eq_list };
Heptagon.c_assume = e_a;
Heptagon.c_enforce = e_g;
Heptagon.c_objectives = objs;
Heptagon.c_assume_loc = e_a_loc;
Heptagon.c_enforce_loc = e_g_loc;
Heptagon.c_controllables = l_c } ->
Some { c_local = List.map translate_var v;
c_eq = List.map translate_eq eq_list;
c_assume = translate_extvalue e_a;
c_enforce = translate_extvalue e_g;
c_objectives = List.map translate_objective objs;
c_assume_loc = translate_extvalue e_a_loc;
c_enforce_loc = translate_extvalue e_g_loc;
c_controllables = List.map translate_var l_c }
@ -219,7 +225,6 @@ let node n =
n_input = List.map translate_var n.Heptagon.n_input;
n_output = List.map translate_var n.Heptagon.n_output;
n_contract = translate_contract n.Heptagon.n_contract;
n_controller_call = ([],[]);
n_local = List.map translate_var n.Heptagon.n_block.Heptagon.b_local;
n_equs = List.map translate_eq n.Heptagon.n_block.Heptagon.b_equs;
n_loc = n.Heptagon.n_loc ;

12
compiler/main/heptc.ml
View file

@ -28,9 +28,6 @@
(***********************************************************************)
open Misc
open Modules
open Location
open Compiler_utils
open Compiler_options
@ -117,7 +114,9 @@ let compile source_f =
(** [main] function to be launched *)
let main () =
let read_qualname f = Arg.String (fun s -> f (Names.qualname_of_string s)) in
let read_qualname f =
Arg.String (fun s -> f (try Names.qualname_of_string s with
| Exit -> raise (Arg.Bad ("Invalid name: "^ s)))) in
try
Arg.parse
[
@ -158,6 +157,11 @@ let main () =
"-O", Arg.Unit do_optim, doc_optim;
"-mall", Arg.Set interf_all, doc_interf_all;
"-time", Arg.Set time_passes, doc_time_passes;
"-abstract-infinite", Arg.Set abstract_infinite, doc_abstract_infinite;
("-Wno-untranslatable", Arg.Clear warn_untranslatable,
doc_no_warn_untranslat);
("-Wno-abstract", Arg.Clear warn_abstractions,
doc_no_warn_abstractions);
]
compile errmsg;
with

19
compiler/main/hepts.ml
View file

@ -145,12 +145,11 @@ class enum_input mod_name value_list (table:GPack.table) n : input =
let _ = List.iter
(fun (v,b) ->
let prefixed_value = mod_name ^ "_" ^ v in
let click () =
if not !click_processed then
begin
click_processed := true;
value := prefixed_value;
value := v;
!active_button#set_active false;
b#set_active true;
active_button := b;
@ -260,13 +259,13 @@ let create_input v_name v_ty n (table:GPack.table) =
match v_ty with
| Tid{ qual = Pervasives; name = "int" } ->
new scale_input
0.0 0. 120.float_of_string
0. (-60.) 60. float_of_string
(fun v ->
string_of_int (int_of_float v))
0
table n
| Tid{ qual = Pervasives; name = "float" } ->
new scale_input 0. 0. 100. float_of_string string_of_float 1 table n
new scale_input 0. (-100.) 100. float_of_string string_of_float 1 table n
| Tid{ qual = Pervasives; name = "bool" } ->
new boolean_input table n
| Tid(name) ->
@ -360,13 +359,11 @@ let main () =
(fun s -> raise (Arg.Bad ("Invalid argument: " ^ s)))
usage_msg;
if (!mod_name = "")
or (!node_name = "")
or (!exec_name = "") then
begin
Arg.usage arg_list usage_msg;
raise Error
end;
if (!mod_name = "") || (!node_name = "") || (!exec_name = "") then
begin
Arg.usage arg_list usage_msg;
raise Error
end;
open_module (Module !mod_name);

37
compiler/main/mls2obc.ml
View file

@ -37,7 +37,6 @@ open Obc_utils
open Obc_mapfold
open Types
open Clocks
open Static
open Initial
@ -67,9 +66,7 @@ let var_from_name map x =
assert false
end
let ext_value_exp_from_name map x =
let w = ext_value_of_pattern (var_from_name map x) in
mk_exp w.w_ty (Eextvalue w)
let ext_value_exp_from_name map x = exp_of_pattern (var_from_name map x)
(* let lvar_from_name map ty x = mk_pattern ty (Lvar (var_from_name map x)) *)
@ -83,7 +80,7 @@ let fresh_for = fresh_for "mls2obc"
let op_from_string op = { qual = Pervasives; name = op; }
let rec pattern_of_idx_list p l =
let pattern_of_idx_list p l =
let rec aux p l = match Modules.unalias_type p.pat_ty, l with
| _, [] -> p
| Tarray (ty',_), idx :: l -> aux (mk_pattern ty' (Larray (p, idx))) l
@ -103,7 +100,7 @@ let rec extvalue_of_idx_list w l = match Modules.unalias_type w.w_ty, l with
extvalue_of_idx_list (mk_ext_value ty' (Warray (w, idx))) l
| _ -> internal_error "mls2obc extvalue_of_idx_list"
let rec ext_value_of_trunc_idx_list p l =
let ext_value_of_trunc_idx_list p l =
let mk_between idx se =
mk_exp_int (Eop (mk_pervasives "between", [idx; mk_ext_value_exp se.se_ty (Wconst se)]))
in
@ -116,7 +113,7 @@ let rec ext_value_of_trunc_idx_list p l =
let rec ty_of_idx_list ty idx_list = match ty, idx_list with
| _, [] -> ty
| Tarray(ty, _), idx::idx_list -> ty_of_idx_list ty idx_list
| Tarray(ty, _), _idx::idx_list -> ty_of_idx_list ty idx_list
| _, _ -> internal_error "mls2obc ty_of_idx_list"
let mk_static_array_power ty c params = match params with
@ -133,7 +130,7 @@ let array_elt_of_exp idx e =
mk_ext_value_exp ty (Warray(ext_value_of_exp e, idx))
| _ -> internal_error "mls2obc array_elt_of_exp"
let rec array_elt_of_exp_list idx_list e =
let array_elt_of_exp_list idx_list e =
match e.e_desc, Modules.unalias_type e.e_ty with
| Eextvalue { w_desc = Wconst { se_desc = Sarray_power (c, params) } }, Tarray (ty,n) ->
let new_params, _ = Misc.split_at (List.length params - List.length idx_list) params in
@ -217,9 +214,9 @@ let ssa_update_record dest src f v =
List.map assgn_act fields
let rec control map ck s = match ck with
| Cbase | Cvar { contents = Cindex _ } -> s
| Clocks.Cbase | Cvar { contents = Cindex _ } -> s
| Cvar { contents = Clink ck } -> control map ck s
| Con(ck, c, n) ->
| Clocks.Con(ck, c, n) ->
let x = ext_value_exp_from_name map n in
control map ck (Acase(x, [(c, mk_block [s])]))
@ -244,7 +241,7 @@ let rec translate_extvalue map w = match w.Minils.w_desc with
| _ ->
let desc = match w.Minils.w_desc with
| Minils.Wconst v -> Wconst v
| Minils.Wvar x -> assert false
| Minils.Wvar _ -> assert false
| Minils.Wfield (w1, f) -> Wfield (translate_extvalue map w1, f)
| Minils.Wwhen (w1, _, _) | Minils.Wreinit(_, w1) -> (translate_extvalue map w1).w_desc
in
@ -318,7 +315,7 @@ and translate_act map pat
let cpt1, cpt1d = fresh_it () in
let cpt2, cpt2d = fresh_it () in
let x = var_from_name map x in
let t = x.pat_ty in
let _t = x.pat_ty in
(match e1.Minils.w_ty, e2.Minils.w_ty with
| Tarray (t1, n1), Tarray (t2, n2) ->
let e1 = translate_extvalue_to_exp map e1 in
@ -391,7 +388,7 @@ and translate_act map pat
| Minils.Evarpat x, Minils.Eapp ({ Minils.a_op = Minils.Eselect_trunc }, e1::idx, _) ->
let x = var_from_name map x in
let bounds = Mls_utils.bounds_list e1.Minils.w_ty in
let _bounds = Mls_utils.bounds_list e1.Minils.w_ty in
let e1 = translate_extvalue map e1 in
let idx = List.map (translate_extvalue_to_exp map) idx in
let w = ext_value_of_trunc_idx_list e1 idx in
@ -459,7 +456,7 @@ let rec translate_eq map call_context
(v, si, j, s) =
let { Minils.e_desc = desc; Minils.e_loc = loc } = e in
match (pat, desc) with
| pat, Minils.Ewhen (e,_,_) ->
| _pat, Minils.Ewhen (e,_,_) ->
translate_eq map call_context {eq with Minils.eq_rhs = e} (v, si, j, s)
(* TODO Efby and Eifthenelse should be dealt with in translate_act, no ? *)
| Minils.Evarpat n, Minils.Efby (opt_c, e) ->
@ -485,7 +482,7 @@ let rec translate_eq map call_context
let action = mk_ifthenelse cond true_act false_act in
v, si, j, (control map ck action) :: s
| pat, Minils.Eapp({ Minils.a_op =
| _pat, Minils.Eapp({ Minils.a_op =
Minils.Efun ({ qual = Module "Iostream"; name = "printf" | "fprintf" } as q)},
args, _) ->
let action = Aop (q, List.map (translate_extvalue_to_exp map) args) in
@ -772,10 +769,10 @@ let translate_ty_def { Minils.t_name = name; Minils.t_desc = tdesc;
let translate_const_def { Minils.c_name = name; Minils.c_value = se;
Minils.c_type = ty; Minils.c_loc = loc } =
{ c_name = name;
c_value = se;
c_type = ty;
c_loc = loc }
{ Obc.c_name = name;
Obc.c_value = se;
Obc.c_type = ty;
Obc.c_loc = loc }
let program { Minils.p_modname = p_modname; Minils.p_opened = p_o; Minils.p_desc = pd; } =
build_anon pd;
@ -784,7 +781,7 @@ let program { Minils.p_modname = p_modname; Minils.p_opened = p_o; Minils.p_desc
| Minils.Pnode n when not (Itfusion.is_anon_node n.Minils.n_name) ->
Pclass (translate_node n) :: acc
(* dont't translate anonymous nodes, they will be inlined *)
| Minils.Pnode n -> acc
| Minils.Pnode _ -> acc
| Minils.Ptype t -> Ptype (translate_ty_def t) :: acc
| Minils.Pconst c -> Pconst (translate_const_def c) :: acc
in

25
compiler/main/mls2seq.ml
View file

@ -29,9 +29,6 @@
open Compiler_utils
open Compiler_options
open Obc
open Minils
open Misc
(** Definition of a target. A target starts either from
dataflow code (ie Minils) or sequential code (ie Obc),
@ -41,6 +38,7 @@ type program_target =
| Obc_no_params of (Obc.program -> unit)
| Minils of (Minils.program -> unit)
| Minils_no_params of (Minils.program -> unit)
| Disabled_target
type interface_target =
| IObc of (Obc.interface -> unit)
@ -79,6 +77,14 @@ let java_conf () =
Compiler_options.do_scalarize := true;
()
;; IFDEF ENABLE_CTRLN THEN
let ctrln_targets =
[ mk_target "ctrln" (Minils_no_params ignore) ]
;; ELSE
let ctrln_targets =
[ mk_target "ctrln" Disabled_target ]
;; ENDIF
let targets =
[ mk_target ~interface:(IObc Cmain.interface) "c" (Obc_no_params Cmain.program);
mk_target ~load_conf:java_conf "java" (Obc Java_main.program);
@ -87,6 +93,7 @@ let targets =
mk_target "obc" (Obc write_obc_file);
mk_target "obc_np" (Obc_no_params write_obc_file);
mk_target "epo" (Minils write_object_file) ]
@ ctrln_targets
let find_target s =
try
@ -100,11 +107,11 @@ let generate_target p s =
comment "Unfolding";
if !Compiler_options.verbose
then List.iter (Mls_printer.print stderr) p_list in*)
let target = (find_target s).t_program in
let { t_program = program; t_name = name } = find_target s in
let callgraph p = do_silent_pass "Callgraph" Callgraph.program p in
let mls2obc p = do_silent_pass "Translation into MiniLS" Mls2obc.program p in
let mls2obc_list p_l = do_silent_pass "Translation into MiniLS" (List.map Mls2obc.program) p_l in
match target with
let mls2obc p = do_silent_pass "Translation from MiniLS" Mls2obc.program p in
let mls2obc_list p_l = do_silent_pass "Translation from MiniLS" (List.map Mls2obc.program) p_l in
match program with
| Minils convert_fun ->
do_silent_pass "Code generation from MiniLS" convert_fun p
| Obc convert_fun ->
@ -113,12 +120,14 @@ let generate_target p s =
do_silent_pass "Code generation from Obc" convert_fun o
| Minils_no_params convert_fun ->
let p_list = callgraph p in
do_silent_pass "Code generation from Obc (w/o params)" (List.iter convert_fun) p_list
do_silent_pass "Code generation from Minils (w/o params)" (List.iter convert_fun) p_list
| Obc_no_params convert_fun ->
let p_list = callgraph p in
let o_list = mls2obc_list p_list in
let o_list = List.map Obc_compiler.compile_program o_list in
do_silent_pass "Code generation from Obc (w/o params)" List.iter convert_fun o_list
| Disabled_target ->
warn "ignoring unavailable target `%s'." name
let generate_interface i s =
let target = (find_target s).t_interface in

3
compiler/minils/_tags
View file

@ -1,2 +1,3 @@
<analysis> or <transformations> or <main> or <parsing>:include
<sigali>:include
<sigali>:include
<ctrln>:include

1
compiler/minils/analysis/_tags
View file

@ -1 +0,0 @@
<interference.ml>:use_ocamlgraph

37
compiler/minils/analysis/clocking.ml
View file

@ -37,20 +37,21 @@
*)
open Misc
open Idents
open Names
open Minils
open Global_printer
open Mls_printer
open Signature
open Types
open Clocks
open Location
open Format
(** Error Kind *)
type error_kind = | Etypeclash of ct * ct | Eclockclash of ck * ck | Edefclock
type error_kind =
| Etypeclash of ct * ct
| Eclockclash of Clocks.ck * Clocks.ck
| Edefclock
let error_message loc = function
| Etypeclash (actual_ct, expected_ct) ->
@ -90,7 +91,7 @@ let rec typing_extvalue h w =
| Wwhen (w1, c, n) ->
let ck_n = ck_of_name h n in
expect_extvalue h ck_n w1;
Con (ck_n, c, n)
Clocks.Con (ck_n, c, n)
| Wfield (w1, _) ->
typing_extvalue h w1
| Wreinit (w1, w2) ->
@ -136,7 +137,8 @@ let typing_app h base pat op w_list = match op with
| a::a_l, v::v_l -> (match a.a_name with
| None -> build_env a_l v_l env
| Some n -> build_env a_l v_l ((n,v)::env))
| _ -> Misc.internal_error "Clocking, non matching signature"
| _ -> Misc.internal_error ("Clocking, non matching signature in call of " ^
Names.fullname f)
in
let env_pat = build_env node.node_outputs pat_id_list [] in
let env_args = build_env node.node_inputs w_list [] in
@ -179,12 +181,12 @@ let typing_eq h ({ eq_lhs = pat; eq_rhs = e; eq_loc = loc } as eq) =
Ck ck, ck
| Ewhen (e,c,n) ->
let ck_n = ck_of_name h n in
let base = expect (skeleton ck_n e.e_ty) e in
let base_ck = if stateful e then ck_n else Con (ck_n, c, n) in
skeleton (Con (ck_n, c, n)) e.e_ty, base_ck
let _base = expect (skeleton ck_n e.e_ty) e in
let base_ck = if stateful e then ck_n else Clocks.Con (ck_n, c, n) in
skeleton (Clocks.Con (ck_n, c, n)) e.e_ty, base_ck
| Emerge (x, c_e_list) ->
let ck = ck_of_name h x in
List.iter (fun (c,e) -> expect_extvalue h (Con (ck,c,x)) e) c_e_list;
List.iter (fun (c,e) -> expect_extvalue h (Clocks.Con (ck,c,x)) e) c_e_list;
Ck ck, ck
| Estruct l ->
let ck = fresh_clock () in
@ -201,7 +203,7 @@ let typing_eq h ({ eq_lhs = pat; eq_rhs = e; eq_loc = loc } as eq) =
typing_app h base_ck pat op (pargs@args)
| Imapi -> (* clocking the node with the extra i input on [ck_r] *)
let il (* stubs i as 0 *) =
List.map (fun x -> mk_extvalue ~ty:Initial.tint ~linearity:Linearity.Ltop
List.map (fun _ -> mk_extvalue ~ty:Initial.tint ~linearity:Linearity.Ltop
~clock:base_ck (Wconst (Initial.mk_static_int 0))) nl
in
typing_app h base_ck pat op (pargs@args@il)
@ -212,7 +214,7 @@ let typing_eq h ({ eq_lhs = pat; eq_rhs = e; eq_loc = loc } as eq) =
ct
| Ifoldi -> (* clocking the node with the extra i and last in/out constraints *)
let il (* stubs i as 0 *) =
List.map (fun x -> mk_extvalue ~ty:Initial.tint ~linearity:Linearity.Ltop
List.map (fun _ -> mk_extvalue ~ty:Initial.tint ~linearity:Linearity.Ltop
~clock:base_ck (Wconst (Initial.mk_static_int 0))) nl
in
let rec insert_i args = match args with
@ -259,7 +261,7 @@ let typing_contract h0 h contract =
| Some ({ c_local = l_list;
c_eq = eq_list;
c_assume = e_a;
c_enforce = e_g;
c_objectives = objs;
c_assume_loc = e_a_loc;
c_enforce_loc = e_g_loc;
c_controllables = c_list } as contract) ->
@ -267,10 +269,10 @@ let typing_contract h0 h contract =
(* assumption *)
(* property *)
let eq_list = typing_eqs h' eq_list in
expect_extvalue h' Cbase e_a;
expect_extvalue h' Cbase e_g;
expect_extvalue h Cbase e_a_loc;
expect_extvalue h Cbase e_g_loc;
expect_extvalue h' Clocks.Cbase e_a;
List.iter (fun o -> expect_extvalue h' Clocks.Cbase o.o_exp) objs;
expect_extvalue h Clocks.Cbase e_a_loc;
expect_extvalue h Clocks.Cbase e_g_loc;
let h = append_env h c_list in
Some { contract with c_eq = eq_list }, h
@ -283,7 +285,7 @@ let typing_node node =
(* let h = append_env h node.n_local in *)
let equs = typing_eqs h node.n_equs in
(* synchronize input and output on base : find the free vars and set them to base *)
Env.iter (fun _ ck -> unify_ck Cbase (root_ck_of ck)) h0;
Env.iter (fun _ ck -> unify_ck Clocks.Cbase (root_ck_of ck)) h0;
(*update clock info in variables descriptions *)
let set_clock vd = { vd with v_clock = ck_repr (Env.find vd.v_ident h) } in
let node = { node with n_input = List.map set_clock node.n_input;
@ -303,4 +305,3 @@ let program p =
| _ -> pd
in
{ p with p_desc = List.map program_desc p.p_desc; }

21
compiler/minils/analysis/interference.ml
View file

@ -34,7 +34,6 @@ open Minils
open Linearity
open Interference_graph
open Containers
open Printf
let print_interference_graphs = false
let verbose_mode = false
@ -113,8 +112,8 @@ module InterfRead = struct
exception Const_extvalue
let rec vars_ck acc = function
| Con(ck2, _, n) -> (Ivar n)::(vars_ck acc ck2)
| Cbase | Cvar { contents = Cindex _ } -> acc
| Clocks.Con(ck2, _, n) -> (Ivar n)::(vars_ck acc ck2)
| Clocks.Cbase | Cvar { contents = Cindex _ } -> acc
| Cvar { contents = Clink ck } -> vars_ck acc ck
let rec vars_ct acc ct = match ct with
@ -344,7 +343,7 @@ let all_ivars_list ivs =
let is_fast_memory x =
match ck_repr (World.ivar_clock (Imem x)) with
| Cbase -> false
| Clocks.Cbase -> false
| _ -> true
(* TODO: variables with no use ?? *)
@ -406,7 +405,7 @@ let should_interfere (ivx, ivy) =
not ((x_is_mem && not x_is_when) ||
(y_is_mem && not y_is_when)) && Clocks.are_disjoint ckx cky
in
not (disjoint_clocks or are_copies)
not (disjoint_clocks || are_copies)
)
let should_interfere = Misc.memoize_couple should_interfere
@ -418,10 +417,10 @@ let should_interfere = Misc.memoize_couple should_interfere
let init_interference_graph () =
let add_tyenv env iv =
let ty = Static.simplify_type Names.QualEnv.empty (World.ivar_type iv) in
TyEnv.add_element ty (mk_node iv) env
TyEnv.add_element ty (Interference_graph.mk_node iv) env
in
(** Adds a node for the variable and all fields of a variable. *)
let rec add_ivar env iv ty =
let add_ivar env iv ty =
let ivars = all_ivars [] iv None ty in
List.fold_left add_tyenv env ivars
in
@ -440,9 +439,9 @@ let init_interference_graph () =
the list. If force is true, then interference is added
whatever the variables are, without checking if interference
is real. *)
let rec add_interferences_from_list force vars =
let add_interferences_from_list force vars =
let add_interference ivx ivy =
if force or should_interfere (ivx, ivy) then
if force || should_interfere (ivx, ivy) then
add_interference_link_from_ivar ivx ivy
in
Misc.iter_couple add_interference vars
@ -629,10 +628,10 @@ let add_init_return_eq f =
(** a_1,..,a_p = __init__ *)
let eq_init = mk_equation false (pat_from_dec_list f.n_input)
(mk_extvalue_exp Cbase Initial.tint Ltop (Wconst (Initial.mk_static_int 0))) in
(mk_extvalue_exp Clocks.Cbase Initial.tint ~linearity:Ltop (Wconst (Initial.mk_static_int 0))) in
(** __return__ = o_1,..,o_q, mem_1, ..., mem_k *)
let eq_return = mk_equation false (Etuplepat [])
(mk_exp Cbase Tinvalid Ltop (tuple_from_dec_and_mem_list f.n_output)) in
(mk_exp Clocks.Cbase Tinvalid ~linearity:Ltop (tuple_from_dec_and_mem_list f.n_output)) in
(eq_init::f.n_equs)@[eq_return]
(** Coalesce Imem x and Ivar x *)

1
compiler/minils/ctrln/_tags Normal file
View file

@ -0,0 +1 @@
<*.mli>: doc_use_interf_n_implem, merge(A)

724
compiler/minils/ctrln/ctrlNbacGen.ml Normal file
View file

@ -0,0 +1,724 @@
(***********************************************************************)
(* *)
(* Heptagon *)
(* *)
(* Gwenael Delaval, LIG/INRIA, UJF *)
(* Leonard Gerard, Parkas, ENS *)
(* Adrien Guatto, Parkas, ENS *)
(* Cedric Pasteur, Parkas, ENS *)
(* Marc Pouzet, Parkas, ENS *)
(* Nicolas Berthier, SUMO, INRIA *)
(* *)
(* Copyright 2013 ENS, INRIA, UJF *)
(* *)
(* This file is part of the Heptagon compiler. *)
(* *)
(* Heptagon is free software: you can redistribute it and/or modify it *)
(* under the terms of the GNU General Public License as published by *)
(* the Free Software Foundation, either version 3 of the License, or *)
(* (at your option) any later version. *)
(* *)
(* Heptagon is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU General Public License for more details. *)
(* *)
(* You should have received a copy of the GNU General Public License *)
(* along with Heptagon. If not, see <http://www.gnu.org/licenses/> *)
(* *)
(***********************************************************************)
(** Translation from the source language to Controllable-Nbac
@author Nicolas Berthier *)
(* -------------------------------------------------------------------------- *)
open Compiler_utils
open Ctrln_utils
open Signature
open Types
open Names
open Idents
open Minils
open CtrlNbac
open AST
let (&) f g = f g
exception Untranslatable of string (* XXX not catched yet! *)
(* --- *)
let tt = mk_bcst' true
let ff = mk_bcst' false
(* --- *)
(** Private record gathering temporary generation data *)
type 'f gen_data =
{
typdefs: 'f typdefs;
decls: 'f node_decls;
base: (var_ident * ty) SMap.t;
local: (var_ident * ty) SMap.t;
contrs: (var_ident * ty) SMap.t;
output: IdentSet.t;
init_cond: 'f bexp;
init_state: 'f bexp;
assertion: 'f bexp;
invariant: 'f bexp;
reachable: 'f bexp option;
attractive: 'f bexp option;
remaining_contrs: SSet.t; (* All controllable inputs that has not yet
been assigned to a U/C group. *)
local_contr_deps: SSet.t SMap.t; (* All variables that depend on a
controllable. *)
extra_inputs: SSet.t;
uc_groups: (SSet.t * SSet.t) list;
}
(* --- *)
let mk_gen_data typdefs decls input local output init_cond =
{
typdefs;
decls;
base = input;
local;
contrs = SMap.empty;
output;
remaining_contrs = SSet.empty;
local_contr_deps = SMap.empty;
extra_inputs = SSet.empty;
uc_groups = [];
init_cond;
init_state = tt;
assertion = tt;
invariant = tt;
reachable = None;
attractive = None;
}
(* --- *)
let translate_constr { name } = mk_label & mk_symb name (* XXX use qual name? *)
let translate_constrs cl = mk_etyp (List.map translate_constr cl)
(* --- *)
let rec translate_typ typ = match Modules.unalias_type typ with
| Tid ({ qual = Pervasives; name = "bool" }) -> `Bool
| Tid ({ qual = Pervasives; name = "int" }) -> `Int
| Tid ({ qual = Pervasives; name = "float" }) -> `Real
| Tid ({ name = tn } as t) -> (match Modules.find_type t with
| Tenum _ -> `Enum (mk_typname (mk_symb tn))
| Talias t -> translate_typ t (* XXX? *)
| _ -> raise & Untranslatable ("type "^ fullname t))
| Tprod _ -> raise & Untranslatable ("product type")
| Tarray _ -> raise & Untranslatable ("array type")
| Tinvalid -> failwith "Encountered an invalid type!"
let rec fintypp typ = match Modules.unalias_type typ with
| Tid ({ qual = Pervasives; name = "bool" }) -> true
| Tid t -> (match Modules.find_type t with
| Tenum _ -> true
| Talias t -> fintypp t (* XXX? *)
| _ -> false)
| _ -> false
let ref_of_ty ty = match translate_typ ty with
| `Bool -> mk_bref
| `Enum _ -> mk_eref
| `Int | `Real -> mk_nref
(* --- *)
let simplify_static_exp se = (Static.simplify QualEnv.empty se).se_desc
let translate_static_bexp se = match simplify_static_exp se with
| Sbool true | Sconstructor { qual = Pervasives; name = "true" } -> tt
| Sbool false | Sconstructor { qual = Pervasives; name = "false" } -> ff
| _ -> failwith (Format.asprintf "Boolean static expression expected! (found@ \
`%a')" Global_printer.print_static_exp se)
let translate_static_eexp se = match simplify_static_exp se with
| Sconstructor { qual = Pervasives; name = "true" as n }
| Sconstructor { qual = Pervasives; name = "false" as n } ->
failwith ("Enum static expression expected! (found `"^n^"')")
| Sconstructor c -> `Enum (translate_constr c)
| _ -> failwith (Format.asprintf "Enum static expression expected! (found@ \
`%a')" Global_printer.print_static_exp se)
let translate_static_nexp se = match simplify_static_exp se with
| Sint v -> `Int v
| Sfloat v -> `Real v
| Sop ({ qual = Pervasives; name="~-" },[{ se_desc = Sint v }]) -> `Int (-v)
| Sop ({ qual = Pervasives; name="~-." },[{ se_desc=Sfloat v }]) -> `Real (-.v)
| _ -> failwith (Format.asprintf "Numerical static expression expected! (found\
@ `%a')" Global_printer.print_static_exp se)
(* --- *)
let rec translate_ext_bexp ~pref : _ -> 'f bexp = function
| Wconst se -> translate_static_bexp se
| Wvar id -> mk_bref' (pref & mk_symb & name id)
| Wfield _ -> failwith "TODO Unsupported Boolean `field' expression!"
| Wwhen (ev, _, _) -> translate_ext_bexp ~pref ev.w_desc
| Wreinit _ -> failwith "TODO Unsupported Boolean `reinit' expression!"
and translate_ext_eexp ~pref : _ -> 'f eexp = function
| Wconst se -> translate_static_eexp se
| Wvar id -> mk_eref' (pref & mk_symb & name id)
| Wwhen (ev, _, _) -> translate_ext_eexp ~pref ev.w_desc
| _ -> failwith "TODO Unsupported Enum expression!"
and translate_ext_nexp ~pref : _ -> 'f nexp = function
| Wconst se -> translate_static_nexp se
| Wvar id -> mk_nref' (pref & mk_symb & name id)
| Wwhen (ev, _, _) -> translate_ext_nexp ~pref ev.w_desc
| _ -> failwith "TODO Unsupported Numerical expression!"
let translate_ext ~pref ext = match translate_typ ext.w_ty with
| `Bool -> `Bexp (translate_ext_bexp ~pref ext.w_desc)
| `Enum _ -> `Eexp (translate_ext_eexp ~pref ext.w_desc)
| `Int | `Real -> `Nexp (translate_ext_nexp ~pref ext.w_desc)
(* --- *)
let translate_app ~pref op el =
let pervasives = function
| "not", [e] -> mk_neg e
|("~-" | "~-."), [e] -> mk_opp e
| "or", e::l -> mk_disj e l
| "&", e::l -> mk_conj e l
| "xor", [e;f] -> mk_xor e f
| "=", [e;f] -> mk_eq e f
| "<>", [e;f] -> mk_ne e f
|("<" | "<."), [e;f] -> mk_lt e f
|("<=" | "<=."), [e;f] -> mk_le e f
|(">" | ">."), [e;f] -> mk_gt e f
|(">=" | ">=."), [e;f] -> mk_ge e f
|("+" | "+."), e::f::l -> mk_sum e f l
|("-" | "-."), e::f::l -> mk_sub e f l
|("*" | "*."), e::f::l -> mk_mul e f l
|("/" | "/."), e::f::l -> mk_div e f l
| name, _ -> raise (Untranslatable name)
in
match op, List.map (translate_ext ~pref) el with
| Eequal, [e;f] -> mk_eq e f
| Efun { qual = Pervasives; name }, el -> pervasives (name, el)
| Eifthenelse, [c;t;e] -> mk_cond c t e
| _ -> failwith "Unsupported application!"
(** [translate_exp gd e] translates the {e memoryless} expression [e] into its
Controllable Nbac representation. *)
let rec translate_exp ~pref ({ e_desc = desc }) = (* XXX clock? *)
match desc with
| Eextvalue ext -> translate_ext ~pref ext
| Eapp ({ a_op }, el, _) -> translate_app ~pref a_op el
| Emerge (v, (_c, e) :: l) ->
let v = pref & mk_symb & name v in
List.fold_left
(fun x (c, e) -> mk_cond
(mk_eq (mk_eref v) (mk_ecst (translate_constr c)))
(translate_ext ~pref e) x)
(translate_ext ~pref e)
l
| Ewhen (exp, _, _) -> translate_exp ~pref exp
| Efby _ -> failwith "TODO: translate_exp (fby)"
| Estruct _ -> failwith "TODO: translate_exp (struct)"
| _ -> failwith "TODO: translate_exp"
(* --- *)
let rec translate_clk ~pref on off = function
| Clocks.Cbase | Clocks.Cvar { contents = Clocks.Cindex _ } -> on
| Clocks.Cvar { contents = Clocks.Clink ck } -> translate_clk ~pref on off ck
| Clocks.Con (ck, {name = cstr}, v) ->
let v = pref & mk_symb & name v in
let c = mk_eq (mk_eref v) (mk_ecst (mk_label (mk_symb cstr))) in
translate_clk ~pref (mk_cond c on off) off ck
(* --- *)
let acc_dependencies_on vars deps_on_vars i e = fold_exp_dependencies
(fun v s ->
if SSet.mem v vars then SSet.add v s
else try SSet.union s (SMap.find v deps_on_vars) with
| Not_found -> s)
e i
(* --- *)
let add_state_var' ~pref gd id ty exp init =
let v = pref & mk_symb & name id in
let typ = translate_typ ty in
let mk_init = match typ, init with
| _, None -> (fun b -> b)
| `Bool, Some i -> mk_and' (mk_beq' (mk_bref' v) (translate_static_bexp i))
| `Enum _, Some i -> mk_and' (mk_eeq' (mk_eref' v) (translate_static_eexp i))
| #ntyp, Some i -> mk_and' (mk_neq' (mk_nref' v) (translate_static_nexp i))
in
{ gd with
decls = SMap.add v (typ, `State (exp, None), None) gd.decls;
init_state = mk_init gd.init_state; }, v
let add_state_var ~pref gd id ty exp init =
let gd, v = add_state_var' ~pref gd id ty exp init in
{ gd with base = SMap.add v (id, ty) gd.base; }
let add_output_var ~pref gd id ty exp =
add_state_var' ~pref gd id ty exp None |> fst
let add_local_var ~pref gd id ty exp =
let v = pref & mk_symb & name id in
let typ = translate_typ ty in
let ldeps = fold_exp_dependencies (fun v acc ->
if SSet.mem v gd.remaining_contrs then SSet.add v acc
else try SSet.union acc (SMap.find v gd.local_contr_deps) with
| Not_found -> acc)
exp
SSet.empty
in
let local_contr_deps = SMap.add v ldeps gd.local_contr_deps in
{ gd with
decls = SMap.add v (typ, `Local (exp, None), None) gd.decls;
local_contr_deps; }
let declare_additional_input ~pref gd id =
let l = mk_symb & name id in
try
let v = pref l in
let t = SMap.find l gd.local |> snd |> translate_typ in
{ gd with
decls = SMap.add v (t, `Input one, None) gd.decls;
extra_inputs = SSet.add v gd.extra_inputs; }
with
| Not_found -> (* output of the main node. *)
assert (IdentSet.mem id gd.output);
gd
(* --- *)
let close_uc_group gd defined_contrs =
let rem = SSet.diff gd.remaining_contrs defined_contrs in
let lcd = SMap.map (SSet.inter rem) gd.local_contr_deps in
let lcd = SMap.filter (fun _ d -> not (SSet.is_empty d)) lcd in
{ gd with
remaining_contrs = rem;
extra_inputs = SSet.empty;
local_contr_deps = lcd;
uc_groups = (gd.extra_inputs, defined_contrs) :: gd.uc_groups; }
(* --- *)
let pat_ids pat =
let rec acc_pat acc = function
| Evarpat id -> ((* pref & *)(* mk_symb & name *)id) :: acc
| Etuplepat pats -> List.fold_left acc_pat acc pats
in
acc_pat [] pat |> List.rev
let translate_abstract_app ~pref gd pat _f args =
let results = pat_ids (* ~pref *) pat in
let args = List.map (translate_ext ~pref) args in
let gd =
(* in case of dependencies on remainging controllable variables, switch to
next U/C group. *)
let depc = List.fold_left
(acc_dependencies_on gd.remaining_contrs gd.local_contr_deps)
SSet.empty args
in
if SSet.is_empty depc then gd else close_uc_group gd depc
in
(* declare extra inputs. *)
List.fold_left (declare_additional_input ~pref) gd results
(* --- *)
let translate_eq ~pref (gd, equs)
({ eq_lhs = pat;
eq_rhs = { e_desc = exp; e_ty = ty } as rhs;
eq_base_ck = clk } as eq)
=
let abstract_infinite_state = !Compiler_options.abstract_infinite in
match pat with
| Evarpat id ->
begin match exp with
| Efby _ when (abstract_infinite_state && not (fintypp ty)) ->
warn ~cond:(!Compiler_options.warn_abstractions)
"Abstracting@ %a@ state@ variable@ %s@ as@ non-controllable@ \
input." Global_printer.print_type ty (name id);
(declare_additional_input ~pref gd id, eq :: equs)
| Efby (init, ev) ->
let v = pref & mk_symb & name id in
let ev = translate_ext ~pref ev in
let ev = translate_clk ~pref ev (ref_of_ty ty v) clk in
(add_state_var ~pref gd id ty ev init, eq :: equs)
| Eapp ({ a_op = (Enode f | Efun f) }, args, None)
when f.qual <> Pervasives ->
(translate_abstract_app ~pref gd pat f args, eq :: equs)
| _ when IdentSet.mem id gd.output ->
let exp = translate_exp ~pref rhs in
(add_output_var ~pref gd id ty exp, eq :: equs)
| _ ->
let exp = translate_exp ~pref rhs in
(add_local_var ~pref gd id ty exp, eq :: equs)
end
| Etuplepat _ ->
begin match exp with
| Eapp ({ a_op = (Enode f | Efun f) }, args, None)
when f.qual <> Pervasives ->
(translate_abstract_app ~pref gd pat f args, eq :: equs)
| _ -> failwith "TODO: Minils.Etuplepat construct!"
end
let translate_eqs ~pref acc equs =
let gd, equs = List.fold_left (translate_eq ~pref) acc equs in
gd, List.rev equs
(* --- *)
let prefix_vars ~pref vars : symb -> symb =
let vars = List.fold_left begin fun acc { v_ident = id } ->
let v = mk_symb & name id in
SMap.add v (mk_symb ("c_" ^ Symb.to_string v)) acc
end (SMap.empty) vars in
fun p -> pref (try SMap.find p vars with Not_found -> p)
let declare_contr (decls, contrs, vds)
({ v_ident = id; v_type = ty } as vd) rank =
let v = mk_symb & name id in
SMap.add v (translate_typ ty, `Contr (one, rank, None), None) decls,
SMap.add v (id, ty) contrs,
vd :: vds
let declare_contrs acc cl =
fst & List.fold_left
(fun (acc, rank) c -> (declare_contr acc c rank, AST.succ rank))
(acc, one) cl
(** Contract translation *)
let translate_contract ~pref gd
({ c_local; c_eq = equs;
c_assume = a; c_objectives = objs;
c_assume_loc = a'; c_enforce_loc = g';
c_controllables = cl } as contract)
=
let pref = prefix_vars ~pref c_local in
let decls, contrs, locals = declare_contrs (gd.decls, SMap.empty, []) cl in
let c = SMap.fold (fun v _ -> SSet.add v) contrs SSet.empty in
let gd = { gd with decls; contrs; remaining_contrs = c; } in
let gd, equs' = translate_eqs ~pref (gd, []) equs in
let ak = as_bexp & mk_and (translate_ext ~pref a) (translate_ext ~pref a')
and ok = as_bexp & translate_ext ~pref g' in
let gd, ok, locals = (* Generate error variable if needed: *)
if !Compiler_options.nosink
then (gd, ok, locals)
else let sink = gen_var "cn" "ok" in
let sink_expr = mk_bref' & pref & mk_symb & name sink in
let ok = `Bexp (mk_bcond' gd.init_cond tt ok) in
(add_state_var ~pref gd sink Initial.tbool ok None, sink_expr,
mk_var_dec sink Initial.tbool Linearity.Ltop Clocks.Cbase :: locals)
in
let gd = { gd with
assertion = mk_and' gd.assertion ak;
invariant = mk_and' gd.invariant ok; } in
let opt_and opt_e e' =
match opt_e with
None -> Some e'
| Some e -> Some (mk_and' e e') in
let add_objective gd o =
let e = as_bexp & translate_ext ~pref o.o_exp in
match o.o_kind with
| Obj_enforce -> { gd with invariant = mk_and' gd.invariant e; }
| Obj_reachable -> { gd with reachable = opt_and gd.reachable e; }
| Obj_attractive -> { gd with attractive = opt_and gd.attractive e; } in
let gd = List.fold_left add_objective gd objs in
(gd, { contract with c_eq = equs'; }, locals)
(* --- *)
let declare_output s { v_ident = id } =
IdentSet.add id s
let declare_input m { v_ident = id; v_type = typ } =
SMap.add (mk_symb & name id) (translate_typ typ, `Input one, None) m
let register_var_typ m { v_ident = id; v_type = typ } =
SMap.add (mk_symb & name id) (id, typ) m
(* --- *)
let finalize_uc_groups gd =
let gd = if SSet.is_empty gd.remaining_contrs then gd else
(* switch to last U/C group here, and declare controller call. *)
close_uc_group gd gd.remaining_contrs
in
if SSet.is_empty gd.extra_inputs then gd else
{ gd with
extra_inputs = SSet.empty;
uc_groups = (gd.extra_inputs, SSet.empty) :: gd.uc_groups; }
(* Note uc_groups are reversed in gd BEFORE the call to this function. *)
let assign_uc_groups gd =
let gd = finalize_uc_groups gd in
let uc_groups = List.rev gd.uc_groups in (* start from the first group *)
let decls, _ =
if uc_groups = [] then
gd.decls, one (* no group to change *)
else
List.fold_left begin fun (decls, group) (u, c) ->
let decls = SSet.fold (fun u decls -> match SMap.find u decls with
| (t, `Input _, l) ->
SMap.add u (t, `Input group, l) decls
| _ -> decls) u decls
in
let decls = SSet.fold (fun c decls -> match SMap.find c decls with
| (t, `Contr (_, r, l'), l) ->
SMap.add c (t, `Contr (group, r, l'), l) decls
| _ -> decls) c decls
in
decls, AST.succ group
end (gd.decls, AST.succ one) (List.tl uc_groups)
in
{ gd with decls; uc_groups }
(* --- *)
let scmp a b = String.compare (Symb.to_string a) (Symb.to_string b)
let var_exp v ty =
mk_extvalue ~ty ~clock:Clocks.Cbase ~linearity:Linearity.Ltop (Wvar v)
let decl_arg (v, t) =
mk_arg (Some (name v)) t Linearity.Ltop Signature.Cbase
let gen_ctrlf_calls ~requal_types gd node_name equs =
let equs, _, _ = List.fold_left begin fun (equs, ubase, num) (u, c) ->
(* Controllable inputs of the current U/C group *)
let c = SSet.elements c in
let c = List.sort scmp c in (* XXX now optional (x) *)
let o = List.map (fun v -> SMap.find v gd.contrs) c in
let os = List.map decl_arg o in
let ov, ot = List.split o in
let ov = Etuplepat (List.map (fun v -> Evarpat v) ov) in
(* Accumulate state variables and all non-controllable inputs from the
beginning, plus all controllables from previous U/C groups *)
let u = SSet.fold (fun v -> SMap.add v (SMap.find v gd.local)) u ubase in
let i = SMap.bindings u in
let i = List.sort (fun (a, _) (b, _) -> scmp b a) i in (* rev. i + ibid (x) *)
let is = List.rev_map (fun (_, p) -> decl_arg p) i in
let i = List.rev_map (fun (_, (v, t)) -> var_exp v t) i in
(* Build controller call *)
let func_name = controller_node ~num node_name in
let app = Eapp (mk_app (Efun func_name), i, None) in
let exp = mk_exp ~linearity:Linearity.Ltop Clocks.Cbase (Tprod ot) app in
let equ = mk_equation false ov exp in
let is, os = if requal_types then
(* Optional requalification of types declared in the exported module: *)
let requal_arg = function
| { a_type = Tid { qual; name } } as arg when qual = node_name.qual ->
{ arg with a_type = Tid { qual = func_name.qual; name } }
| a -> a
in
List.map requal_arg is, List.map requal_arg os
else
is, os
in
(* Declare new node *)
let node_sig = Signature.mk_node Location.no_location ~extern:false is os
false false [] in
Modules.add_value func_name node_sig;
(* Augment base non-controllble inputs with current controllables *)
let u = List.fold_left (fun u v -> SMap.add v (SMap.find v gd.contrs) u) u c in
(equ :: equs, u, num + 1)
end (equs, gd.base, 0) gd.uc_groups in
equs
(* --- *)
(** Node translation. Note the given node is not expored if it does not comprize a
contract. *)
let translate_node ~requal_types typdefs = function
| ({ n_contract = None } as node) -> node, None
| ({ n_name; n_params } as node) when n_params <> [] ->
warn ~cond:(!Compiler_options.warn_untranslatable)
"Unsupported@ translation@ of@ parametric@ node@ `%s'@ with@ \
contract@ into@ Controllable-Nbac!" (Names.fullname n_name);
node, None
| ({ n_name; n_input; n_output; n_local; n_equs;
n_contract = Some contr } as node) ->
enter_node n_name; (* for optional sink symbol generation. *)
let pref p = p in
let local = List.fold_left register_var_typ SMap.empty n_local in
let input = List.fold_left register_var_typ SMap.empty n_input in
let output = List.fold_left declare_output IdentSet.empty n_output in
let decls = List.fold_left declare_input SMap.empty n_input in
let init_cond_var = mk_symb init_cond_str in
let init_cond = mk_bref' init_cond_var in (* XXX what about gd.base? *)
let init_cond_spec = (`Bool, `State (`Bexp ff, None), None) in
let decls = SMap.add init_cond_var init_cond_spec decls in
let gd = mk_gen_data typdefs decls input local output init_cond in
let gd, contract, locals' = translate_contract ~pref gd contr in
let gd, equs' = translate_eqs ~pref (gd, []) n_equs in
let gd = assign_uc_groups gd in
let equs' = gen_ctrlf_calls ~requal_types gd n_name equs' in
let ctrln_node_desc =
{ cn_typs = typdefs;
cn_decls = gd.decls;
cn_init = mk_and' gd.init_state init_cond;
cn_assertion = (* mk_or' init_cond *)gd.assertion;
cn_invariant = Some (mk_or' init_cond gd.invariant);
cn_reachable = gd.reachable;
cn_attractive = gd.attractive; }
and node =
{ node with
n_equs = equs';
n_local = List.rev_append locals' n_local;
n_contract = Some contract; }
in
(node, Some (n_name, (`Desc ctrln_node_desc : 'f AST.node)))
(* --- *)
(** Moves all type declarations into the given module, declare aliases for them
(in cases). Also requalifies constructor names in the program, as well as
types of expressions to avoid some errors in code generation later on. *)
let requal_declared_types prog =
let cmodul = controller_modul prog.p_modname in
let requal m = m = prog.p_modname in
let requal_constr ({ qual; name } as cstr) =
if requal qual then { qual = cmodul; name } else cstr in
let requal_type = function (* requalify enum and alias types. *)
| Tid ({ qual; name } as ty) as t when requal qual ->
(match Modules.find_type ty with
| Tenum _ | Talias _ -> Tid { qual = cmodul; name }
| _ -> t)
| t -> t
in
let requal_type_dec = function
| { t_name = tn; t_desc } as t when requal tn.qual ->
let new_type = match t_desc with
| Type_enum cl -> Signature.Tenum (List.map requal_constr cl)
| Type_alias t -> Signature.Talias (requal_type t)
| _ -> raise Errors.Fallback
in
let tn' = { tn with qual = cmodul } in
let t = { t with t_name = tn; t_desc = Type_alias (Tid tn') } in
Modules.replace_type tn (Signature.Talias (Tid tn'));
Modules.add_type tn' new_type;
t
| _ -> raise Errors.Fallback
in
let open Mls_mapfold in
let open Global_mapfold in
let funcs = { Mls_mapfold.defaults with
type_dec = (fun _ () td -> requal_type_dec td, ());
edesc = (fun funs () -> function
| Ewhen (e, c, x) ->
Ewhen (exp_it funs () e |> fst, requal_constr c,
var_ident_it funs.global_funs () x |> fst), ()
| Emerge (i, l) ->
Emerge (var_ident_it funs.global_funs () i |> fst,
List.map (fun (c, x) -> requal_constr c,
extvalue_it funs () x |> fst) l), ()
| _ -> raise Errors.Fallback);
extvalue_desc = (fun funs () -> function
| Wwhen (w, c, v) ->
Wwhen (extvalue_it funs () w |> fst, requal_constr c,
var_ident_it funs.global_funs () v |> fst), ()
| _ -> raise Errors.Fallback);
global_funs = { Global_mapfold.defaults with
ty = (fun _ () ty -> requal_type ty, ());
ck = (fun funs () -> function
| Clocks.Con (ck, c, i) ->
Clocks.Con (ck_it funs () ck |> fst, requal_constr c,
var_ident_it funs () i |> fst), ()
| _ -> raise Errors.Fallback);
static_exp_desc = (fun _ () -> function
| Sconstructor c -> Sconstructor (requal_constr c), ()
| _ -> raise Errors.Fallback);
};
} in
program funcs () prog |> fst
(* --- *)
(** [gen p] translates all type definitions, plus the nodes comprizing a
contract, into Controllable-Nbac.
@return a Controllable-Nbac program comprizing one process for each node
necessitating controller synthesis), and a new Minils program, in which
those nodes have been transformed so that they "call" their respective
controller.
XXX The [requalify_declared_types] argument is here to avoid cyclic
dependencies between modules due to type declarations. Yet, a better idea
might be to integrate the generated controllers into the original program
later on. *)
let gen ?(requalify_declared_types = true) ({ p_desc } as p) =
let requal_types = requalify_declared_types in
let _cnp_typs, nodes, descs =
List.fold_left begin fun (typdefs, nodes, descs) -> function
| Pnode n ->
begin match translate_node ~requal_types typdefs n with
| node, Some n -> (typdefs, n :: nodes, Pnode node :: descs)
| node, None -> (typdefs, nodes, Pnode node :: descs)
end
| Ptype { t_name = ({ name }); t_desc = Type_enum cl } as ty ->
let tn = mk_typname & mk_symb name and typ = translate_constrs cl in
let typdefs = declare_typ tn typ typdefs in
(typdefs, nodes, ty :: descs)
| p -> (typdefs, nodes, p :: descs)
end (empty_typdefs, [], []) p_desc
in
let cnp_nodes = List.rev nodes and p_desc = List.rev descs in
let prog = { p with p_desc } in
let prog = (* moving types to controller module? *)
if requalify_declared_types
then requal_declared_types prog
else prog
in
cnp_nodes, prog

35
compiler/minils/ctrln/ctrlNbacGen.mli Normal file
View file

@ -0,0 +1,35 @@
(***********************************************************************)
(* *)
(* Heptagon *)
(* *)
(* Gwenael Delaval, LIG/INRIA, UJF *)
(* Leonard Gerard, Parkas, ENS *)
(* Adrien Guatto, Parkas, ENS *)
(* Cedric Pasteur, Parkas, ENS *)
(* Marc Pouzet, Parkas, ENS *)
(* Nicolas Berthier, SUMO, INRIA *)
(* *)
(* Copyright 2013 ENS, INRIA, UJF *)
(* *)
(* This file is part of the Heptagon compiler. *)
(* *)
(* Heptagon is free software: you can redistribute it and/or modify it *)
(* under the terms of the GNU General Public License as published by *)
(* the Free Software Foundation, either version 3 of the License, or *)
(* (at your option) any later version. *)
(* *)
(* Heptagon is distributed in the hope that it will be useful, *)
(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
(* GNU General Public License for more details. *)
(* *)
(* You should have received a copy of the GNU General Public License *)
(* along with Heptagon. If not, see <http://www.gnu.org/licenses/> *)
(* *)
(***********************************************************************)
(* Interface documentation is in `ctrlNbacGen.ml' only. *)
(** *)
val gen: ?requalify_declared_types:bool -> Minils.program ->
(Names.qualname * 'f CtrlNbac.AST.node) list * Minils.program

55
compiler/minils/main/mls_compiler.ml
View file

@ -7,6 +7,7 @@
(* Adrien Guatto, Parkas, ENS *)
(* Cedric Pasteur, Parkas, ENS *)
(* Marc Pouzet, Parkas, ENS *)
(* Nicolas Berthier, SUMO, INRIA *)
(* *)
(* Copyright 2012 ENS, INRIA, UJF *)
(* *)
@ -26,13 +27,47 @@
(* along with Heptagon. If not, see <http://www.gnu.org/licenses/> *)
(* *)
(***********************************************************************)
open Misc
open Location
open Compiler_utils
open Compiler_options
let pp p = if !verbose then Mls_printer.print stdout p
;; IFDEF ENABLE_CTRLN THEN
(* NB: I localize file name determination logics for CtrlNbac output into this
module, because its place is not in CtrlNbacGen... *)
(** [gen_n_output_ctrln p] translates the Minils program [p] into
Controllable-Nbac format, and then output its nodes separately in files
under a specific directory; typically, a node ["n"] in file ["f.ept"] is
output into a file called "f_ctrln/n.nbac" *)
let gen_n_output_ctrln p =
(* Main generation procedure. *)
let nodes, p = CtrlNbacGen.gen p in
(* Save the controller module. *)
Ctrln_utils.save_controller_modul_for p.Minils.p_modname;
(* Output Controllable-Nbac contoller. *)
ignore (clean_dir (Ctrln_utils.dirname_for_modul p.Minils.p_modname));
List.iter begin fun (node_name, node) ->
let oc = open_out (Ctrln_utils.ctrln_for_node node_name) in
let fmt = Format.formatter_of_out_channel oc in
CtrlNbac.AST.print_node ~print_header:print_header_info fmt node;
close_out oc
end nodes;
p
let maybe_ctrln_pass p =
let ctrln = List.mem "ctrln" !target_languages in
pass "Controllable Nbac generation" ctrln gen_n_output_ctrln p pp
;; ELSE
let maybe_ctrln_pass p = p
;; END
let compile_program p =
(* Clocking *)
let p =
@ -52,7 +87,7 @@ let compile_program p =
(* Dataglow minimization *)
let p =
let call_tomato = !tomato or (List.length !tomato_nodes > 0) in
let call_tomato = !tomato || (List.length !tomato_nodes > 0) in
let p = pass "Extended value inlining" call_tomato Inline_extvalues.program p pp in
pass "Data-flow minimization" call_tomato Tomato.program p pp in
@ -73,16 +108,22 @@ let compile_program p =
in
let z3z = List.mem "z3z" !target_languages in
let ctrln = List.mem "ctrln" !target_languages in
let ctrl = z3z || ctrln in
if z3z && ctrln then
warn "ignoring target `ctrln' (incompatible with target `z3z').";
let p = maybe_ctrln_pass p in
let p = pass "Sigali generation" z3z Sigalimain.program p pp in
(* Re-scheduling after sigali generation *)
(* Re-scheduling after generation *)
let p =
if not !Compiler_options.use_old_scheduler then
pass "Scheduling (with minimization of interferences)" z3z Schedule_interf.program p pp
pass "Scheduling (with minimization of interferences)" ctrl Schedule_interf.program p pp
else
pass "Scheduling" z3z Schedule.program p pp
pass "Scheduling" ctrl Schedule.program p pp
in
(* Memory allocation *)
let p = pass "Memory allocation" !do_mem_alloc Interference.program p pp in

68
compiler/minils/minils.ml
View file

@ -33,14 +33,13 @@ open Location
open Names
open Idents
open Signature
open Static
open Types
open Linearity
open Clocks
(** Warning: Whenever Minils ast is modified,
minils_format_version should be incremented. *)
let minils_format_version = "3"
let minils_format_version = "4"
type iterator_type =
| Imap
@ -62,7 +61,7 @@ and tdesc =
and extvalue = {
w_desc : extvalue_desc;
mutable w_ck: ck;
mutable w_ck: Clocks.ck;
w_ty : ty;
w_linearity : linearity;
w_loc : location }
@ -71,12 +70,12 @@ and extvalue_desc =
| Wconst of static_exp (*no tuple*)
| Wvar of var_ident
| Wfield of extvalue * field_name
| Wwhen of extvalue * constructor_name * var_ident (** extvalue when Constructor(ident) *)
| Wwhen of extvalue * constructor_name * var_ident (** {!extvalue} [when Constructor(ident)] *)
| Wreinit of extvalue * extvalue
and exp = {
e_desc : edesc;
e_level_ck : ck; (*when no data dep, execute the exp on this clock (set by [switch] *)
e_level_ck : Clocks.ck; (*when no data dep, execute the exp on this clock (set by [switch] *)
mutable e_ct : ct;
e_ty : ty;
e_linearity : linearity;
@ -85,17 +84,17 @@ and exp = {
and edesc =
| Eextvalue of extvalue
| Efby of static_exp option * extvalue
(** static_exp fby extvalue *)
(** {!static_exp} [fby] {!extvalue} *)
| Eapp of app * extvalue list * var_ident option
(** app ~args=(extvalue,extvalue...) reset ~r=ident *)
| Ewhen of exp * constructor_name * var_ident (** e when C(c) *)
(** [app ~args=(]{!extvalue}[,extvalue...) reset ~r=ident] *)
| Ewhen of exp * constructor_name * var_ident (** [e when C(c)] *)
| Emerge of var_ident * (constructor_name * extvalue) list
(** merge ident (Constructor -> extvalue)+ *)
(** [merge ident (Constructor -> ]{!extvalue}[)+] *)
| Estruct of (field_name * extvalue) list
(** { field=extvalue; ... } *)
(** [{ field=extvalue; ... }] *)
| Eiterator of iterator_type * app * static_exp list
* extvalue list * extvalue list * var_ident option
(** map f <<n>> <(extvalue)> (extvalue) reset ident *)
(** [map f <<n>> <(extvalue)> (extvalue) reset ident] *)
and app = { a_op: op;
a_params: static_exp list;
@ -106,19 +105,19 @@ and app = { a_op: op;
and be delicate about optimizations, !be careful! *)
and op =
| Eequal (** arg1 = arg2 *)
| Efun of fun_name (** "Stateless" longname <<a_params>> (args) reset r *)
| Enode of fun_name (** "Stateful" longname <<a_params>> (args) reset r *)
| Eifthenelse (** if arg1 then arg2 else arg3 *)
| Efield_update (** { arg1 with a_param1 = arg2 } *)
| Earray (** [ args ] *)
| Earray_fill (** [arg1^a_param1^..^a_paramn] *)
| Eselect (** arg1[a_params] *)
| Eselect_slice (** arg1[a_param1..a_param2] *)
| Eselect_dyn (** arg1.[arg3...] default arg2 *)
| Eselect_trunc (** arg1[>arg_2 ...<]*)
| Eupdate (** [ arg1 with arg3..arg_n = arg2 ] *)
| Econcat (** arg1@@arg2 *)
| Eequal (** [arg1 = arg2] *)
| Efun of fun_name (** "Stateless" [longname <<a_params>> (args) reset r] *)
| Enode of fun_name (** "Stateful" [longname <<a_params>> (args) reset r] *)
| Eifthenelse (** [if arg1 then arg2 else arg3] *)
| Efield_update (** [{ arg1 with a_param1 = arg2 }] *)
| Earray (** [[ args ]] *)
| Earray_fill (** [[arg1^a_param1^..^a_paramn]] *)
| Eselect (** [arg1[a_params]] *)
| Eselect_slice (** [arg1[a_param1..a_param2]] *)
| Eselect_dyn (** [arg1.[arg3...] default arg2] *)
| Eselect_trunc (** [arg1[>arg_2 ...<]]*)
| Eupdate (** [[ arg1 with arg3..arg_n = arg2 ]] *)
| Econcat (** [arg1\@\@arg2] *)
type pat =
| Etuplepat of pat list
@ -128,19 +127,28 @@ type eq = {
eq_lhs : pat;
eq_rhs : exp;
eq_unsafe : bool;
eq_base_ck : ck;
eq_base_ck : Clocks.ck;
eq_loc : location }
type var_dec = {
v_ident : var_ident;
v_type : ty;
v_linearity : linearity;
v_clock : ck;
v_clock : Clocks.ck;
v_loc : location }
type objective_kind =
| Obj_enforce
| Obj_reachable
| Obj_attractive
type objective =
{ o_kind : objective_kind;
o_exp : extvalue }
type contract = {
c_assume : extvalue;
c_enforce : extvalue;
c_objectives : objective list;
c_assume_loc : extvalue;
c_enforce_loc : extvalue;
c_controllables : var_dec list;
@ -154,8 +162,6 @@ type node_dec = {
n_input : var_dec list;
n_output : var_dec list;
n_contract : contract option;
(* GD: inglorious hack for controller call *)
mutable n_controller_call : string list * string list;
n_local : var_dec list;
n_equs : eq list;
n_loc : location;
@ -236,7 +242,7 @@ let mk_equation ?(loc = no_location) ?(base_ck=fresh_clock()) unsafe pat exp =
{ eq_lhs = pat; eq_rhs = exp; eq_unsafe = unsafe; eq_base_ck = base_ck; eq_loc = loc }
let mk_node
?(input = []) ?(output = []) ?(contract = None) ?(pinst = ([],[]))
?(input = []) ?(output = []) ?(contract = None)
?(local = []) ?(eq = [])
?(stateful = true) ~unsafe ?(loc = no_location) ?(param = []) ?(constraints = [])
?(mem_alloc=[])
@ -247,7 +253,6 @@ let mk_node
n_input = input;
n_output = output;
n_contract = contract;
n_controller_call = pinst;
n_local = local;
n_equs = eq;
n_loc = loc;
@ -264,4 +269,3 @@ let mk_const_dec id ty e loc =
let mk_app ?(params=[]) ?(unsafe=false) ?(id=None) ?(inlined=false) op =
{ a_op = op; a_params = params; a_unsafe = unsafe;
a_id = id; a_inlined = inlined }

18
compiler/minils/mls_mapfold.ml
View file

@ -47,6 +47,7 @@ type 'a mls_it_funs = {
pat: 'a mls_it_funs -> 'a -> Minils.pat -> Minils.pat * 'a;
var_dec: 'a mls_it_funs -> 'a -> Minils.var_dec -> Minils.var_dec * 'a;
var_decs: 'a mls_it_funs -> 'a -> Minils.var_dec list -> Minils.var_dec list * 'a;
objective: 'a mls_it_funs -> 'a -> Minils.objective -> Minils.objective * 'a;
contract: 'a mls_it_funs -> 'a -> Minils.contract -> Minils.contract * 'a;
node_dec: 'a mls_it_funs -> 'a -> Minils.node_dec -> Minils.node_dec * 'a;
const_dec: 'a mls_it_funs -> 'a -> Minils.const_dec -> Minils.const_dec * 'a;
@ -178,19 +179,23 @@ and var_dec funs acc vd =
and var_decs_it funs acc vds = funs.var_decs funs acc vds
and var_decs funs acc vds = mapfold (var_dec_it funs) acc vds
and objective_it funs acc o = funs.objective funs acc o
and objective funs acc o =
let e, acc = extvalue_it funs acc o.o_exp in
{ o with o_exp = e }, acc
and contract_it funs acc c = funs.contract funs acc c
and contract funs acc c =
let c_assume, acc = extvalue_it funs acc c.c_assume in
let c_assume_loc, acc = extvalue_it funs acc c.c_assume_loc in
let c_enforce, acc = extvalue_it funs acc c.c_enforce in
let c_objectives, acc = mapfold (objective_it funs) acc c.c_objectives in
let c_enforce_loc, acc = extvalue_it funs acc c.c_enforce_loc in
let c_local, acc = var_decs_it funs acc c.c_local in
let c_eq, acc = eqs_it funs acc c.c_eq in
{ c with
c_assume = c_assume;
c_enforce = c_enforce;
c_assume_loc = c_assume_loc;
c_assume = c_assume;
c_objectives = c_objectives;
c_assume_loc = c_assume_loc;
c_enforce_loc = c_enforce_loc;
c_local = c_local;
c_eq = c_eq }
@ -221,7 +226,9 @@ and const_dec funs acc c =
{ c with c_type = ty; c_value = se }, acc
and type_dec_it funs acc t = funs.type_dec funs acc t
and type_dec_it funs acc t =
try funs.type_dec funs acc t
with Fallback -> type_dec funs acc t
and type_dec funs acc t =
let tdesc, acc = tdesc_it funs acc t.t_desc in
{ t with t_desc = tdesc }, acc
@ -265,6 +272,7 @@ let defaults = {
pat = pat;
var_dec = var_dec;
var_decs = var_decs;
objective = objective;
contract = contract;
node_dec = node_dec;
const_dec = const_dec;

28
compiler/minils/mls_printer.ml
View file

@ -28,12 +28,7 @@
(***********************************************************************)
open Misc
open Names
open Signature
open Idents
open Types
open Linearity
open Clocks
open Static
open Format
open Global_printer
open Pp_tools
@ -58,7 +53,7 @@ let rec print_pat ff = function
fprintf ff "@[<2>(%a)@]" (print_list_r print_pat """,""") pat_list
let print_vd ?(show_ck=false) ff { v_ident = n; v_type = ty; v_linearity = lin; v_clock = ck } =
if show_ck or !Compiler_options.full_type_info then
if show_ck || !Compiler_options.full_type_info then
fprintf ff "%a : %a%a :: %a" print_ident n print_type ty print_linearity lin print_ck ck
else fprintf ff "%a : %a%a" print_ident n print_type ty print_linearity lin
@ -225,7 +220,7 @@ and print_eqs ff = function
let print_open_module ff name = fprintf ff "open %s@." (modul_to_string name)
let rec print_type_dec ff { t_name = name; t_desc = tdesc } =
let print_type_dec ff { t_name = name; t_desc = tdesc } =
let print_type_desc ff = function
| Type_abs -> ()
| Type_alias ty -> fprintf ff " =@ %a" print_type ty
@ -236,14 +231,25 @@ let rec print_type_dec ff { t_name = name; t_desc = tdesc } =
fprintf ff "@[<2>type %a%a@]@." print_qualname name print_type_desc tdesc
let print_objective_kind ff = function
| Obj_enforce -> fprintf ff "enforce"
| Obj_reachable -> fprintf ff "reachable"
| Obj_attractive -> fprintf ff "attractive"
let print_objective ff o =
fprintf ff "@[<2>%a@ %a]"
print_objective_kind o.o_kind
print_extvalue o.o_exp
let print_contract ff { c_local = l; c_eq = eqs;
c_assume = e_a; c_enforce = e_g;
c_controllables = c;} =
fprintf ff "@[<v2>contract@\n%a%a@ assume %a@ enforce %a@ with %a@\n@]"
c_assume = e_a;
c_objectives = objs;
c_controllables = c;} =
fprintf ff "@[<v2>contract@\n%a%a@ assume %a%a@ with %a@\n@]"
print_local_vars l
print_eqs eqs
print_extvalue e_a
print_extvalue e_g
(print_list print_objective "@ " "@ " "") objs
print_vd_tuple c

18
compiler/minils/mls_utils.ml
View file

@ -33,10 +33,8 @@ open Location
open Names
open Idents
open Signature
open Static
open Types
open Clocks
open Misc
(** Error Kind *)
type err_kind = | Enot_static_exp
@ -48,7 +46,7 @@ let err_message exp ?(loc=exp.e_loc) = function
print_exp exp;
raise Errors.Error
let rec static_exp_of_exp e =
let static_exp_of_exp e =
match e.e_desc with
| Eextvalue w -> (match w.w_desc with
| Wconst se -> se
@ -79,7 +77,7 @@ let rec vd_find n = function
a list of [var_dec]. *)
let rec vd_mem n = function
| [] -> false
| vd::l -> vd.v_ident = n or (vd_mem n l)
| vd::l -> vd.v_ident = n || (vd_mem n l)
(** @return whether [ty] corresponds to a record type. *)
@ -104,8 +102,8 @@ struct
let def acc { eq_lhs = pat } = vars_pat acc pat
let rec vars_ck acc = function
| Con(ck, _, n) -> vars_ck (add n acc) ck
| Cbase | Cvar { contents = Cindex _ } -> acc
| Clocks.Con(ck, _, n) -> vars_ck (add n acc) ck
| Clocks.Cbase | Cvar { contents = Cindex _ } -> acc
| Cvar { contents = Clink ck } -> vars_ck acc ck
let rec vars_ct acc = function
@ -180,9 +178,9 @@ struct
let head ck =
let rec headrec ck l =
match ck with
| Cbase
| Clocks.Cbase
| Cvar { contents = Cindex _ } -> l
| Con(ck, _, n) -> headrec ck (n :: l)
| Clocks.Con(ck, _, n) -> headrec ck (n :: l)
| Cvar { contents = Clink ck } -> headrec ck l
in
headrec ck []
@ -215,7 +213,7 @@ end
let node_memory_vars n =
let rec eq funs acc ({ eq_lhs = pat; eq_rhs = e } as equ) =
match pat, e.e_desc with
| Evarpat x, Ewhen(e,_,_) -> eq funs acc {equ with eq_rhs = e}
| Evarpat _, Ewhen(e,_,_) -> eq funs acc {equ with eq_rhs = e}
| Evarpat x, Efby(_, _) ->
let acc = (x, e.e_ty) :: acc in
equ, acc
@ -264,7 +262,7 @@ let remove_eqs_from_node nd ids =
let walk_vd vd vd_list = if IdentSet.mem vd.v_ident ids then vd_list else vd :: vd_list in
let walk_eq eq eq_list =
let defs = ident_list_of_pat eq.eq_lhs in
if (not eq.eq_unsafe) & List.for_all (fun v -> IdentSet.mem v ids) defs
if (not eq.eq_unsafe) && List.for_all (fun v -> IdentSet.mem v ids) defs
then eq_list
else eq :: eq_list
in

6
compiler/minils/sigali/sigali.ml
View file

@ -169,9 +169,6 @@ module Printer =
fprintf ff "%s@ " sep;
print_list ff print sep l
let print_string ff s =
fprintf ff "%s" s
let print_name ff n =
fprintf ff "%s" n
@ -435,7 +432,7 @@ module Printer =
fprintf ff "%s_triang : Triang(constraint(%s),controllables,phantom_vars);@,"
name name;
let states =
match !Compiler_options.nosink with
true -> states
@ -468,4 +465,3 @@ module Printer =
let print dir p_l =
List.iter (print_processus dir) p_l
end

81
compiler/minils/sigali/sigalimain.ml
View file

@ -44,12 +44,10 @@ type mtype = Tint | Tbool | Tother
exception Untranslatable
let untranslatable_warn e =
if e.Minils.e_loc <> no_location then
Format.eprintf "Warning: abstracted expression:@.%a"
Location.print_location e.Minils.e_loc
else
Format.eprintf "Warning: abstracted expression: @[<hov 2>%a@]@."
Mls_printer.print_exp e
let warn msg = warn ~cond:(!Compiler_options.warn_untranslatable) msg in
if e.Minils.e_loc <> no_location
then warn "abstracted expression:@.%a" print_location e.Minils.e_loc
else warn "abstracted expression: @[<hov 2>%a@]@." Mls_printer.print_exp e
let actual_ty ty =
match (Modules.unalias_type ty) with
@ -88,8 +86,8 @@ let rec translate_ck pref e = function
let e = translate_ck pref e ck in
Swhen(e,
match (shortname c) with
"true" -> Svar(pref ^ (name var))
| "false" -> Snot(Svar(pref ^ (name var)))
"true" -> Sigali.Svar(pref ^ (name var))
| "false" -> Snot(Sigali.Svar(pref ^ (name var)))
| _ -> assert false)
@ -105,9 +103,9 @@ let rec translate_ext prefix ({ Minils.w_desc = desc; Minils.w_ty = ty }) =
(* get variable iff it is Boolean or local *)
begin match (actual_ty ty) with
| Tbool ->
Svar(prefix ^ (name n))
Sigali.Svar(prefix ^ (name n))
| Tint when (IdentSet.mem n !current_locals) ->
Svar(prefix ^ (name n))
Sigali.Svar(prefix ^ (name n))
| _ ->
raise Untranslatable
end
@ -210,7 +208,7 @@ let rec translate prefix ({ Minils.e_desc = desc } as e) =
| "false" -> e2,e1
| _ -> assert false
end in
let var_ck = Svar(prefix ^ (name ck)) in
let var_ck = Sigali.Svar(prefix ^ (name ck)) in
begin match (actual_ty e.Minils.e_ty) with
| Tbool -> Sdefault(Swhen(e1,var_ck),e2)
| Tint -> a_part var_ck (a_const (Sconst(Cint(0)))) e1 e2
@ -258,7 +256,7 @@ let translate_eq f
let c = translate_static_exp c in
(extend
initialisations
(Slist[Sequal(Svar(sn),Sconst(c))]))::acc_eqs,
(Slist[Sequal(Sigali.Svar(sn),Sconst(c))]))::acc_eqs,
c::acc_init
in
let e_next = translate_ext prefix e' in
@ -268,7 +266,7 @@ let translate_eq f
acc_init,acc_inputs,
(extend
evolutions
(Slist[Sdefault(e_next,Svar(sn))]))
(Slist[Sdefault(e_next,Sigali.Svar(sn))]))
::acc_eqs
with Untranslatable ->
untranslatable_warn e;
@ -282,7 +280,8 @@ let translate_eq f
| _ ->
untranslatable_warn e;
(* Mark n as input: unusable as local variable *)
Format.printf "Adding non-bool variable %s in current_inputs@\n" (name n);
warn ~cond:(!Compiler_options.warn_abstractions)
"Adding non-bool variable %s in current_inputs@\n" (name n);
current_inputs := IdentSet.add n !current_inputs;
acc_states,acc_init,acc_inputs,acc_eqs
end
@ -346,27 +345,41 @@ let translate_contract f contract =
let body =
[{ stmt_name = var_g; stmt_def = Sconst(Ctrue) };
{ stmt_name = var_a; stmt_def = Sconst(Ctrue) }] in
[],[],[],body,(Svar(var_a),Svar(var_g)),[],[],[]
[],[],[],body,(Sigali.Svar(var_a),Sigali.Svar(var_g)),[],[],[],[]
| Some {Minils.c_local = locals;
Minils.c_eq = l_eqs;
Minils.c_assume = e_a;
Minils.c_enforce = e_g;
Minils.c_objectives = objs;
Minils.c_assume_loc = e_a_loc;
Minils.c_enforce_loc = e_g_loc;
Minils.c_controllables = cl} ->
let states,init,inputs,body = translate_eq_list f l_eqs in
let e_a = translate_ext prefix e_a in
let e_g = translate_ext prefix e_g in
let e_a_loc = translate_ext prefix e_a_loc in
let e_g_loc = translate_ext prefix e_g_loc in
(* separate reachability and attractivity and build one security objective [e_g] *)
let e_g,sig_objs =
List.fold_left
(fun (e_g,sig_objs) o ->
let e_obj = translate_ext prefix o.Minils.o_exp in
match o.Minils.o_kind with
| Minils.Obj_enforce -> (e_g &~ e_obj), sig_objs
| Minils.Obj_reachable -> e_g, (Reachability e_obj) :: sig_objs
| Minils.Obj_attractive -> e_g, (Attractivity e_obj) :: sig_objs)
(e_g_loc,[])
objs in
let sig_objs = List.rev sig_objs in
let body =
{stmt_name = var_g; stmt_def = e_g &~ e_g_loc } ::
{stmt_name = var_g; stmt_def = e_g } ::
{stmt_name = var_a; stmt_def = e_a &~ e_a_loc } ::
body in
let controllables =
List.map
(fun ({ Minils.v_ident = id } as v) -> v,(prefix ^ (name id))) cl in
states,init,inputs,body,(Svar(var_a),Svar(var_g)),controllables,(locals@cl),l_eqs
states,init,inputs,body,(Sigali.Svar(var_a),Sigali.Svar(var_g)),
controllables,(locals@cl),l_eqs,sig_objs
@ -394,7 +407,7 @@ let translate_node
(fun { Minils.v_ident = v } -> f ^ "_" ^ (name v)) o_list in
let states,init,add_inputs,body =
translate_eq_list f eq_list in
let states_c,init_c,inputs_c,body_c,(a_c,g_c),controllables,locals_c,eqs_c =
let states_c,init_c,inputs_c,body_c,(a_c,g_c),controllables,locals_c,eqs_c,objs =
translate_contract f contract in
let inputs = inputs @ add_inputs @ inputs_c in
let body = List.rev body in
@ -406,7 +419,7 @@ let translate_node
let mls_ctrl,sig_ctrl = List.split controllables in
let constraints =
List.map
(fun v -> Sequal(Ssquare(Svar(v)),Sconst(Ctrue)))
(fun v -> Sequal(Ssquare(Sigali.Svar(v)),Sconst(Ctrue)))
(sig_inputs@sig_ctrl) in
let constraints = constraints @ [Sequal (a_c,Sconst(Ctrue))] in
let body_sink, sig_states_full, obj_exp =
@ -422,13 +435,13 @@ let translate_node
let body_sink =
[(extend
initialisations
(Slist[Sequal(Svar(error_state_name),Sconst(Ctrue))]));
(Slist[Sequal(Sigali.Svar(error_state_name),Sconst(Ctrue))]));
(extend
evolutions
(Slist[g_c]))] in
(body_sink, sig_states_full, Svar(error_state_name))
(body_sink, sig_states_full, Sigali.Svar(error_state_name))
end in
let obj = Security(obj_exp) in
let objs = Security(obj_exp) :: objs in
let p = { proc_dep = [];
proc_name = f;
proc_inputs = sig_inputs@sig_ctrl;
@ -439,7 +452,7 @@ let translate_node
proc_init = init@init_c;
proc_constraints = constraints;
proc_body = body@body_c@body_sink;
proc_objectives = [obj] } in
proc_objectives = objs } in
if !Compiler_options.nbvars then
begin
(* Print out nb of vars *)
@ -521,12 +534,18 @@ let translate_node
let program p =
let acc_proc, acc_p_desc =
List.fold_left
(fun (acc_proc,acc_p_desc) p_desc ->
match p_desc with
| Minils.Pnode(node) ->
let (node,proc) = translate_node node in
(proc::acc_proc),((Minils.Pnode(node))::acc_p_desc)
| p -> (acc_proc,p::acc_p_desc))
(fun (acc_proc,acc_p_desc) -> function
| Minils.Pnode(node) as p when node.Minils.n_contract = None ->
(acc_proc,p::acc_p_desc)
| Minils.Pnode(node) as p when node.Minils.n_params <> [] ->
warn ~cond:(!Compiler_options.warn_untranslatable)
"Unsupported@ translation@ of@ parametric@ node@ `%s'@ with@ \
contract@ into@ Z/3Z!" (Names.fullname node.Minils.n_name);
(acc_proc,p::acc_p_desc)
| Minils.Pnode(node) ->
let (node,proc) = translate_node node in
(proc::acc_proc),((Minils.Pnode(node))::acc_p_desc)
| p -> (acc_proc,p::acc_p_desc))
([],[])
p.Minils.p_desc in
let procs = List.rev acc_proc in

1
compiler/minils/transformations/callgraph.ml
View file

@ -27,7 +27,6 @@
(* *)
(***********************************************************************)
open Names
open Idents
open Types
open Misc
open Location

6
compiler/minils/transformations/inline_extvalues.ml
View file

@ -27,18 +27,12 @@
(* *)
(***********************************************************************)
open Misc
open Names
open Idents
open Signature
open Minils
open Mls_utils
open Mls_printer
open Global_printer
open Types
open Clocks
open Pp_tools
open Mls_compare
(*
Help tomato by inlining extended values.

24
compiler/minils/transformations/normalize_mem.ml
View file

@ -27,26 +27,20 @@
(* *)
(***********************************************************************)
open Idents
open Signature
open Minils
open Mls_mapfold
open Mls_utils
(** Adds an extra equation for outputs that are also memories.
For instance, if o is an output, then:
o = v fby e
becomes
mem_o = v fby e;
o = mem_o
(** Adds an extra equation for outputs that are also memories. For instance, if
o is an output, then:
We also need to add one copy if two (or more) registers are defined by each other, eg:
x = v fby y;
y = v fby x;
becomes
mem_x = v fby y;
x = mem_x;
y = v fby x
*)
[ o = v fby e ] becomes [ mem_o = v fby e; o = mem_o; ]
We also need to add one copy if two (or more) registers are defined by each
other, eg:
[ x = v fby y; y = v fby x; ] becomes [ mem_x = v fby y; x = mem_x; y = v
fby x; ] *)
let normalize_outputs = ref true

3
compiler/minils/transformations/schedule.ml
View file

@ -29,11 +29,8 @@
(* scheduling of equations *)
open Misc
open Minils
open Mls_utils
open Sgraph
open Dep
(* possible overlapping between clocks *)
let join ck1 ck2 =

3
compiler/minils/transformations/schedule_interf.ml
View file

@ -31,7 +31,6 @@
open Idents
open Minils
open Mls_utils
open Misc
open Sgraph
(** In order to put together equations with the same control structure, we have to take into
@ -163,7 +162,7 @@ struct
let rec min_same_ck (min_eq, min_c, min_same_ctrl) l = match l with
| [] -> min_eq
| (eq, c, same_ctrl)::l ->
if (c < min_c) or (c = min_c && (same_ctrl && not min_same_ctrl)) then
if (c < min_c) || (c = min_c && (same_ctrl && not min_same_ctrl)) then
min_same_ck (eq, c, same_ctrl) l
else
min_same_ck (min_eq, min_c, min_same_ctrl) l

43
compiler/minils/transformations/tomato.ml
View file

@ -28,12 +28,10 @@
(***********************************************************************)
open Misc
open Names
open Idents
open Signature
open Minils
open Mls_utils
open Mls_printer
open Global_printer
open Types
open Clocks
@ -83,7 +81,7 @@ struct
{
mutable er_class : int;
er_clock_type : ct;
er_base_ck : ck;
er_base_ck : Clocks.ck;
er_pattern : pat;
er_head : exp;
er_children : class_ref list;
@ -98,7 +96,7 @@ struct
open Mls_printer
let print_class_ref fmt cr = match cr with
| Cr_plain id -> print_ident fmt id
| Cr_plain id -> Global_printer.print_ident fmt id
| Cr_input w -> Format.fprintf fmt "%a (input)" print_extvalue w
let debug_tenv fmt tenv =
@ -151,19 +149,19 @@ struct
let rec clock_compare ck1 ck2 = match ck1, ck2 with
| Cvar { contents = Clink ck1; }, _ -> clock_compare ck1 ck2
| _, Cvar { contents = Clink ck2; } -> clock_compare ck1 ck2
| Cbase, Cbase -> 0
| Clocks.Cbase, Clocks.Cbase -> 0
| Cvar lr1, Cvar lr2 -> link_compare_modulo !lr1 !lr2
| Con (ck1, cn1, vi1), Con (ck2, cn2, vi2) ->
| Clocks.Con (ck1, cn1, vi1), Clocks.Con (ck2, cn2, vi2) ->
let cr1 = compare cn1 cn2 in
if cr1 <> 0 then cr1 else
let cr2 = ident_compare_modulo vi1 vi2 in
if cr2 <> 0 then cr2 else clock_compare ck1 ck2
| Cbase , _ -> 1
| Clocks.Cbase , _ -> 1
| Cvar _, Cbase -> -1
| Cvar _, Clocks.Cbase -> -1
| Cvar _, _ -> 1
| Con _, _ -> -1
| Clocks.Con _, _ -> -1
and link_compare_modulo li1 li2 = match li1, li2 with
| Cindex _, Cindex _ -> 0
@ -312,8 +310,8 @@ and extvalue is_input w class_id_list =
(* Regroup classes from a minimization environment *)
(*******************************************************************)
let rec compute_classes tenv =
let rec add_eq_repr _ repr cenv =
let compute_classes tenv =
let add_eq_repr _ repr cenv =
let repr_list = try IntMap.find repr.er_class cenv with Not_found -> [] in
IntMap.add repr.er_class (repr :: repr_list) cenv in
PatMap.fold add_eq_repr tenv IntMap.empty
@ -375,15 +373,15 @@ let construct_mapping (_, cenv) =
IntMap.fold construct_mapping_eq_repr cenv Env.empty
let rec reconstruct ((tenv, cenv) as env) mapping =
let rec reconstruct ((_tenv, cenv) as _env) mapping =
let reconstruct_class id eq_repr_list eq_list =
let reconstruct_class _id eq_repr_list eq_list =
assert (List.length eq_repr_list > 0);
let repr = List.hd eq_repr_list in
let e =
let children =
let _children =
Misc.take (List.length repr.er_children - repr.er_when_count) repr.er_children in
let ed = reconstruct_exp_desc mapping repr.er_head.e_desc repr.er_children in
@ -433,7 +431,7 @@ and reconstruct_exp_desc mapping headd children =
| Ewhen _ -> assert false (* no Ewhen in exprs *)
| Emerge (x_ref, clause_list) ->
| Emerge (_x_ref, clause_list) ->
let x_ref, children = List.hd children, List.tl children in
Emerge (reconstruct_class_ref mapping x_ref,
reconstruct_clauses clause_list children)
@ -492,7 +490,7 @@ and reconstruct_class_ref mapping cr = match cr with
x
and reconstruct_clock mapping ck = match ck_repr ck with
| Con (ck, c, x) -> Con (reconstruct_clock mapping ck, c, new_name mapping x)
| Clocks.Con (ck, c, x) -> Clocks.Con (reconstruct_clock mapping ck, c, new_name mapping x)
| _ -> ck
and reconstruct_clock_type mapping ct = match ct with
@ -534,7 +532,7 @@ module EqClasses = Map.Make(
(if unsafe e2 then -1 else list_compare compare_children cr_list1 cr_list2))
end)
let rec path_environment tenv =
let path_environment tenv =
let enrich_env pat { er_class = id } env =
let rec enrich pat path env = match pat with
| Evarpat x -> Env.add x (id, path) env
@ -564,7 +562,8 @@ let compute_new_class (tenv : tom_env) =
| Cr_input _ -> None
| Cr_plain x ->
try Some (Env.find x mapping)
with Not_found -> Format.eprintf "Unknown class %a@." print_ident x; assert false
with Not_found -> Format.eprintf "Unknown class %a@."
Global_printer.print_ident x; assert false
in
let children = List.map map_class_ref eqr.er_children in
@ -576,11 +575,11 @@ let compute_new_class (tenv : tom_env) =
in
let classes = PatMap.fold add_eq_repr tenv EqClasses.empty in
let _classes = PatMap.fold add_eq_repr tenv EqClasses.empty in
(get_id (), tenv)
let rec separate_classes tenv =
let separate_classes tenv =
let rec fix (id, tenv) =
let new_id, tenv = compute_new_class tenv in
debug_do (fun () -> Format.printf "New tenv %d:\n%a@." id debug_tenv tenv) ();
@ -639,7 +638,7 @@ let update_node nd =
ignore (Modules.replace_value nd.n_name sign)
let node nd =
debug_do (fun () -> Format.eprintf "Minimizing %a@." print_qualname nd.n_name);
debug_do (fun () -> Format.eprintf "Minimizing %a@." print_qualname nd.n_name) ();
Idents.enter_node nd.n_name;
(* Initial environment *)
@ -649,7 +648,7 @@ let node nd =
| None -> []
| Some c -> c.c_controllables in
let inputs = nd.n_input @ controllables in
let is_input id =
let is_input id =
List.exists (fun vd -> ident_compare vd.v_ident id = 0) inputs in
List.fold_left (add_equation is_input) PatMap.empty nd.n_equs in

4
compiler/myocamlbuild.ml
View file

@ -31,7 +31,6 @@ open Ocamlbuild_plugin.Options
open Myocamlbuild_config
let df = function
| Before_options -> ocamlfind_before_options ()
| After_rules ->
ocamlfind_after_rules ();
@ -50,7 +49,8 @@ let df = function
flag ["ocaml"; "parser" ; "menhir" ; "use_menhir"] (S[A"--explain";
A"--table"]);
flag ["ocaml"; "compile" ] (S[A"-w"; A"Ae"; A"-warn-error"; A"PU"; A"-w"; A"-9"]);
flag ["ocaml"; "compile" ] (S[A"-w"; A"Ae"; A"-warn-error"; A"PU";
A"-w"; A"-9-48"]);
| _ -> ()

101
compiler/myocamlbuild_config.ml
View file

@ -28,85 +28,46 @@
(***********************************************************************)
open Ocamlbuild_plugin
(* these functions are not really officially exported *)
let run_and_read = Ocamlbuild_pack.My_unix.run_and_read
let blank_sep_strings = Ocamlbuild_pack.Lexers.blank_sep_strings
let split s ch =
let x = ref [] in
let rec go s =
let pos = String.index s ch in
x := (String.before s pos)::!x;
go (String.after s (pos + 1))
in
try
go s
with Not_found -> !x
let split_nl s = split s '\n'
let before_space s =
try
String.before s (String.index s ' ')
with Not_found -> s
(* this lists all supported packages *)
let find_packages () =
List.map before_space (split_nl & run_and_read "ocamlfind list")
(* this is supposed to list available syntaxes, but I don't know how to do it. *)
let find_syntaxes () = ["camlp4o"; "camlp4r"]
(* ocamlfind command *)
let ocamlfind x = S[A"ocamlfind"; x]
let ocamlfind_query pkg =
let cmd = Printf.sprintf "ocamlfind query %s" (Filename.quote pkg) in
Ocamlbuild_pack.My_unix.run_and_open cmd (fun ic -> input_line ic)
let ocamlfind_before_options () =
(* by using Before_options one let command line options have an higher priority *)
(* on the contrary using After_options will guarantee to have the higher priority *)
(* override default commands by ocamlfind ones *)
Options.ocamlc := ocamlfind & A"ocamlc";
Options.ocamlopt := ocamlfind & A"ocamlopt";
Options.ocamldep := ocamlfind & A"ocamldep";
Options.ocamldoc := ocamlfind & A"ocamldoc";
Options.ocamlmktop := ocamlfind & A"ocamlmktop"
let ocamlfind_after_rules () =
(* When one link an OCaml library/binary/package, one should use -linkpkg *)
flag ["ocaml"; "link"; "program"] & A"-linkpkg";
(* For each ocamlfind package one inject the -package option when
* compiling, computing dependencies, generating documentation and
* linking. *)
List.iter begin fun pkg ->
flag ["ocaml"; "compile"; "pkg_"^pkg] & S[A"-package"; A pkg];
flag ["ocaml"; "ocamldep"; "pkg_"^pkg] & S[A"-package"; A pkg];
flag ["ocaml"; "doc"; "pkg_"^pkg] & S[A"-package"; A pkg];
flag ["ocaml"; "link"; "pkg_"^pkg] & S[A"-package"; A pkg];
flag ["ocaml"; "infer_interface"; "pkg_"^pkg] & S[A"-package"; A pkg];
end (find_packages ());
(* Like -package but for extensions syntax. Morover -syntax is useless
* when linking. *)
List.iter begin fun syntax ->
flag ["ocaml"; "compile"; "syntax_"^syntax] & S[A"-syntax"; A syntax];
flag ["ocaml"; "ocamldep"; "syntax_"^syntax] & S[A"-syntax"; A syntax];
flag ["ocaml"; "doc"; "syntax_"^syntax] & S[A"-syntax"; A syntax];
flag ["ocaml"; "infer_interface"; "syntax_"^syntax] & S[A"-syntax"; A syntax];
end (find_syntaxes ());
(* Like -package but for extensions syntax. Morover -syntax is useless
* when linking. *)
List.iter begin fun syntax ->
flag ["ocaml"; "compile"; "syntax_"^syntax] & S[A"-syntax"; A syntax];
flag ["ocaml"; "ocamldep"; "syntax_"^syntax] & S[A"-syntax"; A syntax];
flag ["ocaml"; "doc"; "syntax_"^syntax] & S[A"-syntax"; A syntax];
flag ["ocaml"; "infer_interface"; "syntax_"^syntax] & S[A"-syntax"; A syntax];
end (find_syntaxes ());
flag ["ocaml"; "doc"; "thread"] & S[A"-I"; A"+threads"];
(* The default "thread" tag is not compatible with ocamlfind.
Indeed, the default rules add the "threads.cma" or "threads.cmxa"
options when using this tag. When using the "-linkpkg" option with
ocamlfind, this module will then be added twice on the command line.
(* Use both ml and mli files to build documentation: *)
rule "ocaml: ml & mli -> odoc"
~insert:`top
~tags:["ocaml"; "doc"; "doc_use_interf_n_implem"]
~prod:"%.odoc"
(* "%.cmo" so that cmis of ml dependencies are already built: *)
~deps:["%.ml"; "%.mli"; "%.cmo"]
begin fun env build ->
let mli = env "%.mli" and ml = env "%.ml" and odoc = env "%.odoc" in
let tags =
(Tags.union (tags_of_pathname mli) (tags_of_pathname ml))
++"doc_use_interf_n_implem"++"ocaml"++"doc" in
let include_dirs = Pathname.include_dirs_of (Pathname.dirname ml) in
let include_flags =
List.fold_right (fun p acc -> A"-I" :: A p :: acc) include_dirs [] in
Cmd (S [!Options.ocamldoc; A"-dump"; Px odoc;
T (tags++"doc"++"pp"); S (include_flags);
A"-intf"; P mli; A"-impl"; P ml])
end;
To solve this, one approach is to add the "-thread" option when using
the "threads" package using the previous plugin.
*)
flag ["ocaml"; "pkg_threads"; "compile"] (S[A "-thread"]);
flag ["ocaml"; "pkg_threads"; "link"] (S[A "-thread"]);
flag ["ocaml"; "pkg_threads"; "infer_interface"] (S[A "-thread"])
(* Specifying merge options. *)
pflag ["ocaml"; "doc"; "doc_use_interf_n_implem"] "merge"
(fun s -> S[A"-m"; A s]);

14
compiler/obc/c/c.ml
View file

@ -29,7 +29,6 @@
open Format
open List
open Modules
open Names
let print_list ff print sep l = Pp_tools.print_list_r print "" sep "" ff l
@ -38,7 +37,7 @@ let print_list ff print sep l = Pp_tools.print_list_r print "" sep "" ff l
Copied verbatim from the old C backend. *)
let cname_of_name name =
let buf = Buffer.create (String.length name) in
let rec convert c =
let convert c =
match c with
| 'A'..'Z' | 'a'..'z' | '0'..'9' | '_' ->
Buffer.add_char buf c
@ -91,7 +90,7 @@ and cexpr =
| Cbop of string * cexpr * cexpr (** Binary operator. *)
| Cfun_call of string * cexpr list (** Function call with its parameters. *)
| Caddrof of cexpr (** Take the address of an expression. *)
| Cstructlit of string * cexpr list (** Structure literal "{ f1, f2, ... }".*)
| Cstructlit of string * cexpr list (** Structure literal [{ f1, f2, ... }].*)
| Carraylit of cexpr list (** Array literal [\[e1, e2, ...\]]. *)
| Cconst of cconst (** Constants. *)
| Cvar of string (** A local variable. *)
@ -382,3 +381,12 @@ let rec array_base_ctype ty idx_list =
| Cty_arr (_, ty), _::idx_list -> array_base_ctype ty idx_list
| _ ->
assert false
(** Convert C expression to left-hand side *)
let rec clhs_of_cexpr cexpr =
match cexpr with
| Cvar v -> CLvar v
| Cderef e -> CLderef (clhs_of_cexpr e)
| Cfield (e,qn) -> CLfield (clhs_of_cexpr e, qn)
| Carray (e1,e2) -> CLarray (clhs_of_cexpr e1, e2)
| _ -> failwith("C expression not translatable to LHS")

25
compiler/obc/c/cgen.ml
View file

@ -233,7 +233,7 @@ and create_affect_stm dest src ty =
| Cty_id ln ->
(match src with
| Cstructlit (_, ce_list) ->
let create_affect { f_name = f_name;
let create_affect { Signature.f_name = f_name;
Signature.f_type = f_type; } e stm_list =
let cty = ctype_of_otype f_type in
create_affect_stm (CLfield (dest, f_name)) e cty @ stm_list in
@ -263,7 +263,8 @@ let rec cexpr_of_static_exp se =
(cexpr_of_static_exp c) n_list)
| Svar ln ->
if !Compiler_options.unroll_loops && se.se_ty = Initial.tint
then cexpr_of_static_exp (Static.simplify QualEnv.empty (find_const ln).c_value)
then cexpr_of_static_exp
(Static.simplify QualEnv.empty (find_const ln).Signature.c_value)
else Cvar (cname_of_qn ln)
| Sop _ ->
let se' = Static.simplify QualEnv.empty se in
@ -497,7 +498,7 @@ let generate_function_call out_env var_env obj_env outvl objn args =
let rec create_affect_const var_env (dest : clhs) c =
match c.se_desc with
| Svar ln ->
let se = Static.simplify QualEnv.empty (find_const ln).c_value in
let se = Static.simplify QualEnv.empty (find_const ln).Signature.c_value in
create_affect_const var_env dest se
| Sarray_power(c, n_list) ->
let rec make_loop power_list replace = match power_list with
@ -635,7 +636,7 @@ let global_name = ref "";;
(** {2 step() and reset() functions generation *)
(** {2 step() and reset() functions generation} *)
let qn_append q suffix =
{ qual = q.qual; name = q.name ^ suffix }
@ -684,7 +685,7 @@ let fun_def_of_step_fun n obj_env mem objs md =
let body = cstm_of_act_list out_env var_env obj_env md.m_body in
Cfundef {
f_name = fun_name;
C.f_name = fun_name;
f_retty = Cty_void;
f_args = args;
f_body = {
@ -741,7 +742,7 @@ let reset_fun_def_of_class_def cd =
[]
in
Cfundef {
f_name = (cname_of_qn cd.cd_name) ^ "_reset";
C.f_name = (cname_of_qn cd.cd_name) ^ "_reset";
f_retty = Cty_void;
f_args = [("self", Cty_ptr (Cty_id (qn_append cd.cd_name "_mem")))];
f_body = {
@ -787,32 +788,32 @@ let cdefs_and_cdecls_of_type_decl otd =
[], [Cdecl_typedef (ctype_of_otype ty, name)]
| Type_enum nl ->
let of_string_fun = Cfundef
{ f_name = name ^ "_of_string";
{ C.f_name = name ^ "_of_string";
f_retty = Cty_id otd.t_name;
f_args = [("s", Cty_ptr Cty_char)];
f_body =
{ var_decls = [];
block_body =
let gen_if t =
let t = cname_of_qn t in
let t = cname_of_qn t and t' = t.name in
let funcall = Cfun_call ("strcmp", [Cvar "s";
Cconst (Cstrlit t)]) in
Cconst (Cstrlit t')]) in
let cond = Cbop ("==", funcall, Cconst (Ccint 0)) in
Cif (cond, [Creturn (Cconst (Ctag t))], []) in
map gen_if nl; }
}
and to_string_fun = Cfundef
{ f_name = "string_of_" ^ name;
{ C.f_name = "string_of_" ^ name;
f_retty = Cty_ptr Cty_char;
f_args = [("x", Cty_id otd.t_name); ("buf", Cty_ptr Cty_char)];
f_body =
{ var_decls = [];
block_body =
let gen_clause t =
let t = cname_of_qn t in
let t = cname_of_qn t and t' = t.name in
let fun_call =
Cfun_call ("strcpy", [Cvar "buf";
Cconst (Cstrlit t)]) in
Cconst (Cstrlit t')]) in
(t, [Csexpr fun_call]) in
[Cswitch (Cvar "x", map gen_clause nl);
Creturn (Cvar "buf")]; }

33
compiler/obc/c/cmain.ml
View file

@ -27,20 +27,15 @@
(* *)
(***********************************************************************)
open Format
open List
open Misc
open Names
open Idents
open Obc
open Obc_utils
open Types
open Modules
open Signature
open C
open Cgen
open Location
open Format
open Compiler_utils
(** {1 Main C function generation} *)
@ -102,7 +97,7 @@ let assert_node_res cd =
Cif (Cuop ("!", Cfield (Cvar (fst out), local_qn outn)),
[Csexpr (Cfun_call ("fprintf",
[Cvar "stderr";
Cconst (Cstrlit ("Node \""
Cconst (Cstrlit ("Node \""
^ (Names.fullname cd.cd_name)
^ "\" failed at step" ^
" %d.\n"));
@ -132,7 +127,7 @@ let main_def_of_class_def cd =
| Types.Tid id when id = Initial.pfloat -> None
| Types.Tid id when id = Initial.pint -> None
| Types.Tid id when id = Initial.pbool -> None
| Tid { name = n } -> Some n
| Tid tn -> Some (cname_of_qn tn)
in
let cprint_string s = Csexpr (Cfun_call ("printf", [Cconst (Cstrlit s)])) in
@ -167,12 +162,10 @@ let main_def_of_class_def cd =
(vn ^ "." ^ (shortname fn), args)
| _ -> assert false in
let (prompt, args_format_s) = mk_prompt lhs in
let scan_exp =
let scan_exp e =
let printf_s = Format.sprintf "%s ? " prompt in
let format_s = format_for_type ty in
let exp_scanf = Cfun_call ("scanf",
[Cconst (Cstrlit format_s);
Caddrof lhs]) in
let exp_scanf = Cfun_call ("scanf", [Cconst (Cstrlit format_s); e]) in
let body =
if !Compiler_options.hepts_simulation
then (* hepts: systematically test and quit when EOF *)
@ -191,12 +184,14 @@ let main_def_of_class_def cd =
Csblock { var_decls = [];
block_body = body; } in
match need_buf_for_ty ty with
| None -> ([scan_exp], [])
| None -> ([scan_exp (Caddrof lhs)], [])
| Some tyn ->
let varn = fresh "buf" in
([scan_exp;
Csexpr (Cfun_call (tyn ^ "_of_string",
[Cvar varn]))],
let lhs = clhs_of_cexpr lhs in
([scan_exp (Cvar varn);
Caffect (lhs,
(Cfun_call (tyn ^ "_of_string",
[Cvar varn])))],
[(varn, Cty_arr (20, Cty_char))])
end
| Tprod _ | Tinvalid -> failwith("read_lhs_of_ty: untranslatable type")
@ -248,17 +243,17 @@ let main_def_of_class_def cd =
:: ep))],
match nbuf_opt with
| None -> []
| Some _ -> [(varn, Cty_arr (20, Cty_char))])
| Some _ -> [(varn, Cty_arr (20, Cty_char))])
end
| Tprod _ | Tinvalid -> failwith("write_lhs_of_ty: untranslatable type")
in
let stepm = find_step_method cd in
let (scanf_calls, scanf_decls) =
let read_lhs_of_ty_for_vd vd =
read_lhs_of_ty (Cvar (Idents.name vd.v_ident)) vd.v_type in
split (map read_lhs_of_ty_for_vd stepm.m_inputs) in
let (printf_calls, printf_decls) =
let write_lhs_of_ty_for_vd vd =
let (stm, vars) =
@ -318,7 +313,7 @@ let main_def_of_class_def cd =
variable list [var_list], prologue [prologue] and loop body [body]. *)
let main_skel var_list prologue body =
Cfundef {
f_name = "main";
C.f_name = "main";
f_retty = Cty_int;
f_args = [("argc", Cty_int); ("argv", Cty_ptr (Cty_ptr Cty_char))];
f_body = {

8
compiler/obc/c/cunroll.ml
View file

@ -29,13 +29,9 @@
(* Unroll loops *)
open Format
open List
open Modules
open Names
open C
let rec unroll id start stop body =
let unroll id start stop body =
let rec aux i l =
let rec exp e = match e with
| Cuop (s, e) -> Cuop (s, exp e)
@ -77,7 +73,7 @@ let rec unroll id start stop body =
aux start []
let rec static_eval e = match e with
let static_eval e = match e with
| Cconst (Ccint i) -> Some i
| _ -> None

13
compiler/obc/control.ml
View file

@ -31,18 +31,15 @@
(* TODO could optimize for loops ? *)
open Idents
open Misc
open Obc
open Obc_utils
open Clocks
open Signature
open Obc_mapfold
let appears_in_exp, appears_in_lhs =
let lhsdesc _ (x, acc) ld = match ld with
| Lvar y -> ld, (x, acc or (x=y))
| Lmem y -> ld, (x, acc or (x=y))
| Lvar y -> ld, (x, acc || (x=y))
| Lmem y -> ld, (x, acc || (x=y))
| _ -> raise Errors.Fallback
in
let funs = { Obc_mapfold.defaults with lhsdesc = lhsdesc } in
@ -58,7 +55,7 @@ let appears_in_exp, appears_in_lhs =
let used_vars e =
let add x acc = if List.mem x acc then acc else x::acc in
let lhsdesc funs acc ld = match ld with
let lhsdesc _funs acc ld = match ld with
| Lvar y -> ld, add y acc
| Lmem y -> ld, add y acc
| _ -> raise Errors.Fallback
@ -78,14 +75,14 @@ let rec is_modified_by_call x args e_list = match args, e_list with
let is_modified_handlers j x handlers =
let act _ acc a = match a with
| Aassgn(l, _) -> a, acc or (appears_in_lhs x l)
| Aassgn(l, _) -> a, acc || (appears_in_lhs x l)
| Acall (name_list, o, Mstep, e_list) ->
(* first, check if e is one of the output of the function*)
if List.exists (appears_in_lhs x) name_list then
a, true
else (
let sig_info = find_obj (obj_ref_name o) j in
a, acc or (is_modified_by_call x sig_info.node_inputs e_list)
a, acc || (is_modified_by_call x sig_info.node_inputs e_list)
)
| _ -> raise Errors.Fallback
in

4
compiler/obc/java/java.ml
View file

@ -130,7 +130,7 @@ type program = classe list
(** [jname_of_name name] translates the string [name] to a valid Java identifier. *)
let jname_of_name name =
let buf = Buffer.create (String.length name) in
let rec convert c =
let convert c =
match c with
| 'A'..'Z' | 'a'..'z' | '0'..'9' | '_' ->
Buffer.add_char buf c
@ -142,7 +142,7 @@ let jname_of_name name =
Buffer.contents buf
let rec default_value ty = match ty with
let default_value ty = match ty with
| Tclass _ -> Snull
| Tgeneric _ -> Snull
| Tbool -> Sbool true

17
compiler/obc/java/java14_main.ml
View file

@ -1,4 +1,3 @@
open Misc
open Names
open Modules
open Signature
@ -37,7 +36,7 @@ let program p =
Idents.enter_node class_name;
let field_step_dnb, id_step_dnb =
let id = Idents.gen_var "java_main" "default_step_nb" in
mk_field ~static:true ~final:true ~value:(Some (Sint 30000)) Tint id, id
Java.mk_field ~static:true ~final:true ~value:(Some (Sint 30000)) Tint id, id
in
let main_methode =
@ -56,14 +55,14 @@ let program p =
let exp_current_arg = Earray_elem(exp_args, exp_argnb) in
*)
let body =
let vd_main, e_main, q_main, ty_main =
let vd_main, e_main, q_main, _ty_main =
let q_main = Obc2java14.qualname_to_package_classe q_main in (*java qual*)
let id = Idents.gen_var "java_main" "main" in
mk_var_dec id false (Tclass q_main), Evar id, q_main, ty_main
in
let acts =
let out = Eclass(Names.qualname_of_string "java.lang.System.out") in
let jarrays = Eclass(Names.qualname_of_string "java.util.Arrays") in
let _jarrays = Eclass(Names.qualname_of_string "java.util.Arrays") in
let jint = Eclass(Names.qualname_of_string "Integer") in
let jfloat = Eclass(Names.qualname_of_string "Float") in
let jbool = Eclass(Names.qualname_of_string "Boolean") in
@ -98,15 +97,7 @@ let program p =
mk_block [Aassgn(pat_step, Evar id_step_dnb)]);
in
let ret = Emethod_call(e_main, "step", []) in
let print_ret = match ty_main with
| Types.Tarray (Types.Tarray _, _) -> Emethod_call(jarrays, "deepToString", [ret])
| Types.Tarray _ -> Emethod_call(jarrays, "toString", [ret])
| t when t = Initial.tint -> Emethod_call(jint, "toString", [ret])
| t when t = Initial.tfloat -> Emethod_call(jfloat, "toString", [ret])
| t when t = Initial.tbool -> Emethod_call(jbool, "toString", [ret])
| _ -> Emethod_call(ret, "toString", [])
in
let main_for_loop i =
let main_for_loop _ =
(* [Aexp (Emethod_call(out, "printf", *)
(* [Sstring "%d => %s\\n"; Evar i; print_ret]))] *)
[Aexp ret]

7
compiler/obc/java/java_main.ml
View file

@ -26,7 +26,6 @@
(* along with Heptagon. If not, see <http://www.gnu.org/licenses/> *)
(* *)
(***********************************************************************)
open Misc
open Names
open Modules
open Signature
@ -67,7 +66,7 @@ let program p =
Idents.enter_node class_name;
let field_step_dnb, id_step_dnb =
let id = Idents.gen_var "java_main" "default_step_nb" in
mk_field ~static:true ~final:true ~value:(Some (Sint 30000)) Tint id, id
Java.mk_field ~static:true ~final:true ~value:(Some (Sint 30000)) Tint id, id
in
let main_methode =
@ -100,7 +99,7 @@ let program p =
let jminus = pervasives_qn "-" in
(* num args to give to the main *)
let rec num_args = List.length ty_main_args in
let num_args = List.length ty_main_args in
(* parse arguments to give to the main *)
let rec parse_args t_l i = match t_l with
@ -140,7 +139,7 @@ let program p =
else [Aexp (Emethod_call(out, "printf", [Sstring "%d => \n"; Evar i]))]
| _ ->
if !Compiler_options.hepts_simulation
then
then
[Aexp (Emethod_call(out, "printf",
[Sstring "%s\n";
Emethod_call(java_pervasives,

4
compiler/obc/java/java_printer.ml
View file

@ -32,7 +32,6 @@
open Java
open Pp_tools
open Format
open Misc
let print_ident ff id = Format.fprintf ff "%s" (jname_of_name (Idents.name id))
@ -96,7 +95,7 @@ and new_init_ty ff t = _ty true true ff t
and ty ff t = _ty false false ff t
and var_dec init ff vd =
if init & not vd.vd_alias then
if init && not vd.vd_alias then
fprintf ff "%a %a = %a" ty vd.vd_type var_ident vd.vd_ident exp (Java.default_value vd.vd_type)
else
fprintf ff "%a %a" ty vd.vd_type var_ident vd.vd_ident
@ -295,4 +294,3 @@ let output_classe base_dir c =
let output_program dir (p:Java.program) =
List.iter (output_classe dir) p

90
compiler/obc/java/obc2java.ml
View file

@ -39,9 +39,7 @@
[p = e] when [e] is an array is understand as a copy of the reference, not a copy of the array.*)
open Format
open Misc
open Names
open Modules
open Signature
open Obc
open Obc_utils
@ -59,8 +57,8 @@ let add_classe, get_classes =
with [body] a function from [var_ident] (the iterator) to [act] list *)
let fresh_for size body =
let i = Idents.gen_var "obc2java" "i" in
let id = mk_var_dec i false Tint in
Afor (id, Sint 0, size, mk_block (body i))
let id = Java.mk_var_dec i false Tint in
Java.Afor (id, Sint 0, size, Java.mk_block (body i))
(** fresh nested Afor from 0 to [size]
with [body] a function from [var_ident] list (the iterator list) to [act] list :
@ -74,19 +72,19 @@ let fresh_nfor s_l body =
let rec aux s_l i_l = match s_l with
| [s] ->
let i = Idents.gen_var "obc2java" "i" in
let id = (mk_var_dec i false Tint) in
Afor (id, Sint 0, s, mk_block (body (List.rev (i::i_l))))
let id = (Java.mk_var_dec i false Tint) in
Java.Afor (id, Sint 0, s, Java.mk_block (body (List.rev (i::i_l))))
| s::s_l ->
let i = Idents.gen_var "obc2java" "i" in
let id = mk_var_dec i false Tint in
Afor (id, Sint 0, s, mk_block ([aux s_l (i::i_l)]))
let id = Java.mk_var_dec i false Tint in
Java.Afor (id, Sint 0, s, Java.mk_block ([aux s_l (i::i_l)]))
| [] -> Misc.internal_error "Fresh nfor called with empty size list"
in
aux s_l []
(* current module is not translated to keep track,
there is no issue since printed without the qualifier *)
let rec translate_modul m = m (*match m with
let translate_modul m = m (*match m with
| Pervasives
| LocalModule -> m
| _ when m = g_env.current_mod -> m
@ -189,7 +187,7 @@ let rec static_exp param_env se = match se.Types.se_desc with
| Types.Sarray se_l ->
Enew_array (ty param_env se.Types.se_ty, List.map (static_exp param_env) se_l)
| Types.Srecord f_e_l ->
let ty_name =
let ty_name =
match se.Types.se_ty with
| Types.Tid ty_name -> qualname_to_package_classe ty_name
| _ -> Misc.internal_error "Obc2java"
@ -220,7 +218,7 @@ and boxed_ty param_env t = match Modules.unalias_type t with
Tarray (t, s_l)
| Types.Tinvalid -> Misc.internal_error "obc2java invalid type"
and tuple_ty param_env ty_l =
and tuple_ty _param_env ty_l =
let ln = ty_l |> List.length |> Pervasives.string_of_int in
Tclass (java_pervasive_class ("Tuple"^ln))
@ -319,7 +317,7 @@ let obj_ref param_env o = match o with
let jop_of_op param_env op_name e_l =
match op_name with
| { qual = Module "Iostream"; name = "printf" } ->
Emethod_call (Eclass(Names.qualname_of_string "java.lang.System.out"),
Emethod_call (Eclass(Names.qualname_of_string "java.lang.System.out"),
"printf",
(exp_list param_env e_l))
| _ ->
@ -328,19 +326,19 @@ let jop_of_op param_env op_name e_l =
let rec act_list param_env act_l acts =
let _act act acts = match act with
| Obc.Aassgn (p,e) -> (Aassgn (pattern param_env p, exp param_env e))::acts
| Obc.Aassgn (p,e) -> (Java.Aassgn (pattern param_env p, exp param_env e))::acts
| Obc.Aop (op,e_l) -> Aexp (jop_of_op param_env op e_l) :: acts
| Obc.Acall ([], obj, Mstep, e_l) ->
let acall = Emethod_call (obj_ref param_env obj, "step", exp_list param_env e_l) in
Aexp acall::acts
| Obc.Acall ([p], obj, Mstep, e_l) ->
let ecall = Emethod_call (obj_ref param_env obj, "step", exp_list param_env e_l) in
let assgn = Aassgn (pattern param_env p, ecall) in
let assgn = Java.Aassgn (pattern param_env p, ecall) in
assgn::acts
| Obc.Acall (p_l, obj, Mstep, e_l) ->
let return_ty = p_l |> pattern_list_to_type |> (ty param_env) in
let return_id = Idents.gen_var "obc2java" "out" in
let return_vd = mk_var_dec return_id false return_ty in
let return_vd = Java.mk_var_dec return_id false return_ty in
let ecall = Emethod_call (obj_ref param_env obj, "step", exp_list param_env e_l) in
let assgn = Anewvar (return_vd, ecall) in
let copy_return_to_var i p =
@ -352,7 +350,7 @@ let rec act_list param_env act_l acts =
| _ -> Ecast(t, e)
in
let p = pattern param_env p in
Aassgn (p, cast t (Efield (Evar return_id, "c"^(string_of_int i))))
Java.Aassgn (p, cast t (Efield (Evar return_id, "c"^(string_of_int i))))
in
let copies = Misc.mapi copy_return_to_var p_l in
assgn::(copies@acts)
@ -365,23 +363,26 @@ let rec act_list param_env act_l acts =
| [(c,b)] when c = Initial.ptrue ->
(Aif (exp param_env e, block param_env b)):: acts
| [(c,b)] when c = Initial.pfalse ->
(Aifelse (exp param_env e, {b_locals = []; b_body = []}, block param_env b)) :: acts
(Aifelse (exp param_env e, {Java.b_locals = [];
Java.b_body = []},
block param_env b)) :: acts
| _ ->
let _, _then = List.find (fun (c,_) -> c = Initial.ptrue) c_b_l in
let _, _else = List.find (fun (c,_) -> c = Initial.pfalse) c_b_l in
(Aifelse (exp param_env e, block param_env _then, block param_env _else)) :: acts)
| Obc.Acase (e, c_b_l) ->
let _c_b (c,b) =
let _c_b (c,b) =
Senum (translate_constructor_name c),
block param_env b in
let acase = Aswitch (exp param_env e, List.map _c_b c_b_l) in
acase::acts
| Obc.Afor (v, se, se', b) ->
let afor = Afor (var_dec param_env v,
exp param_env se, exp param_env se', block param_env b) in
let afor = Java.Afor (var_dec param_env v,
exp param_env se, exp param_env se',
block param_env b) in
afor::acts
| Obc.Ablock b ->
let ablock = Ablock (block param_env b) in
let ablock = Java.Ablock (block param_env b) in
ablock::acts
in
List.fold_right _act act_l acts
@ -390,7 +391,7 @@ and block param_env ?(locals=[]) ?(end_acts=[]) ob =
let blocals = var_dec_list param_env ob.Obc.b_locals in
let locals = locals @ blocals in
let acts = act_list param_env ob.Obc.b_body end_acts in
{ b_locals = locals; b_body = acts }
{ Java.b_locals = locals; Java.b_body = acts }
@ -401,7 +402,7 @@ and block param_env ?(locals=[]) ?(end_acts=[]) ob =
let sig_params_to_vds p_l =
let param_to_arg param_env p =
let p_ident = Idents.gen_var "obc2java" (String.uppercase p.Signature.p_name) in
let p_vd = mk_var_dec p_ident false (ty param_env p.Signature.p_type) in
let p_vd = Java.mk_var_dec p_ident false (ty param_env p.Signature.p_type) in
let param_env = NamesEnv.add p.Signature.p_name p_ident param_env in
p_vd, param_env
in Misc.mapfold param_to_arg NamesEnv.empty p_l
@ -411,12 +412,12 @@ let sig_args_to_vds param_env a_l =
let arg_to_vd { a_name = n; a_type = t } =
let n = match n with None -> "v" | Some s -> s in
let id = Idents.gen_var "obc2java" n in
mk_var_dec id false (ty param_env t)
Java.mk_var_dec id false (ty param_env t)
in List.map arg_to_vd a_l
(** [copy_to_this vd_l] creates [this.x = x] for all [x] in [vd_l] *)
let copy_to_this vd_l =
let _vd vd = Aassgn (Pthis vd.vd_ident, Evar vd.vd_ident) in
let _vd vd = Java.Aassgn (Pthis vd.vd_ident, Evar vd.vd_ident) in
List.map _vd vd_l
@ -426,7 +427,7 @@ let class_def_list classes cd_l =
let class_name = qualname_to_package_classe cd.cd_name in
(* [param_env] is an env mapping local param name to ident *)
(* [params] : fields to stock the static parameters, arguments of the constructors *)
let fields_params, vds_params, exps_params, param_env =
let fields_params, vds_params, _exps_params, param_env =
let v, env = sig_params_to_vds cd.cd_params in
let f = vds_to_fields ~protection:Pprotected v in
let e = vds_to_exps v in
@ -443,7 +444,7 @@ let class_def_list classes cd_l =
let reset_mems = block param_env (remove_resets oreset.Obc.m_body) in
mk_methode body "reset", reset_mems
with Not_found -> (* stub reset method *)
mk_methode (mk_block []) "reset", mk_block []
mk_methode (Java.mk_block []) "reset", Java.mk_block []
in
(* [obj_env] gives the type of an [obj_ident],
needed in async because we change the classe for async obj *)
@ -461,14 +462,14 @@ let class_def_list classes cd_l =
match od.o_size with
| None ->
let t = Idents.Env.find od.o_ident obj_env in
(Aassgn (Pthis od.o_ident, Enew (t, params)))::acts
(Java.Aassgn (Pthis od.o_ident, Enew (t, params)))::acts
| Some size_l ->
let size_l = List.rev (List.map (static_exp param_env) size_l) in
let t = Idents.Env.find od.o_ident obj_env in
let assgn_elem i_l =
[ Aassgn (Parray_elem (Pthis od.o_ident, List.map mk_var i_l), Enew (t, params)) ]
[ Java.Aassgn (Parray_elem (Pthis od.o_ident, List.map mk_var i_l), Enew (t, params)) ]
in
(Aassgn (Pthis od.o_ident, Enew_array (Tarray (t,size_l), [])))
(Java.Aassgn (Pthis od.o_ident, Enew_array (Tarray (t,size_l), [])))
:: (fresh_nfor size_l assgn_elem)
:: acts
in
@ -476,24 +477,24 @@ let class_def_list classes cd_l =
let allocate acts vd = match Modules.unalias_type vd.v_type with
| Types.Tarray _ ->
let t = ty param_env vd.v_type in
( Aassgn (Pthis vd.v_ident, Enew_array (t,[])) ):: acts
( Java.Aassgn (Pthis vd.v_ident, Enew_array (t,[])) ):: acts
| _ -> acts
in
(* init actions [acts] in reverse order : *)
(* init member variables *)
let acts = [Ablock reset_mems] in
let acts = [Java.Ablock reset_mems] in
(* allocate member arrays *)
let acts = List.fold_left allocate acts cd.cd_mems in
(* init member objects *)
let acts = List.fold_left obj_init_act acts cd.cd_objs in
(* init static params *)
let acts = (copy_to_this vds_params)@acts in
{ b_locals = []; b_body = acts }
{ Java.b_locals = []; Java.b_body = acts }
in mk_methode ~args:vds_params body (shortname class_name), obj_env
in
let fields =
let mem_to_field fields vd =
(mk_field ~protection:Pprotected (ty param_env vd.v_type) vd.v_ident) :: fields
(Java.mk_field ~protection:Pprotected (ty param_env vd.v_type) vd.v_ident) :: fields
in
let obj_to_field fields od =
let jty = match od.o_size with
@ -501,7 +502,7 @@ let class_def_list classes cd_l =
| Some size_l -> Tarray (Idents.Env.find od.o_ident obj_env,
List.map (static_exp param_env) size_l)
in
(mk_field ~protection:Pprotected jty od.o_ident) :: fields
(Java.mk_field ~protection:Pprotected jty od.o_ident) :: fields
in
let fields = fields_params in
let fields = List.fold_left mem_to_field fields cd.cd_mems in
@ -547,23 +548,23 @@ let type_dec_list classes td_l =
(* [translate_field_name] will give the right result anywhere it is used,
since the [ident_of_name] will keep it as it is unique in the class,
see [Idents.enter_node classe_name] *)
mk_field jty field
Java.mk_field jty field
in
let f_l =
List.sort
List.sort
(fun f1 f2 ->
compare (f1.Signature.f_name.name) (f2.Signature.f_name.name))
f_l in
let fields = List.map mk_field_jfield f_l in
let cons_params = List.map (fun f -> mk_var_dec f.f_ident false f.f_type) fields in
let cons_body =
let cons_params = List.map (fun f -> Java.mk_var_dec f.f_ident false f.Java.f_type) fields in
let cons_body =
List.map
(fun f -> Aassgn ((Pthis f.f_ident),(Evar f.f_ident)))
(fun f -> Java.Aassgn ((Pthis f.f_ident),(Evar f.f_ident)))
fields in
let cons =
mk_methode
mk_methode
~args:cons_params
(mk_block cons_body)
(Java.mk_block cons_body)
classe_name.name in
(mk_classe ~fields:fields ~constrs:[cons] classe_name) :: classes
in
@ -583,7 +584,7 @@ let const_dec_list cd_l = match cd_l with
(* thus [translate_const_name] will gives the right result anywhere it is used. *)
let value = Some (static_exp param_env ovalue) in
let t = ty param_env otype in
mk_field ~static: true ~final: true ~value: value t name
Java.mk_field ~static: true ~final: true ~value: value t name
in
let fields = List.map mk_const_field cd_l in
[mk_classe ~fields: fields classe_name]
@ -602,6 +603,3 @@ let program p =
let classes = type_dec_list classes ts in
let p = class_def_list classes ns in
get_classes()@p

98
compiler/obc/java/obc2java14.ml
View file

@ -39,7 +39,6 @@
[p = e] when [e] is an array is understand as a copy of the reference, not a copy of the array.*)
open Format
open Misc
open Names
open Modules
open Signature
@ -59,8 +58,8 @@ let add_classe, get_classes =
with [body] a function from [var_ident] (the iterator) to [act] list *)
let fresh_for size body =
let i = Idents.gen_var "obc2java" "i" in
let id = mk_var_dec i false Tint in
Afor (id, Sint 0, size, mk_block (body i))
let id = Java.mk_var_dec i false Tint in
Java.Afor (id, Sint 0, size, Java.mk_block (body i))
(** fresh nested Afor from 0 to [size]
with [body] a function from [var_ident] list (the iterator list) to [act] list :
@ -74,19 +73,19 @@ let fresh_nfor s_l body =
let rec aux s_l i_l = match s_l with
| [s] ->
let i = Idents.gen_var "obc2java" "i" in
let id = (mk_var_dec i false Tint) in
Afor (id, Sint 0, s, mk_block (body (List.rev (i::i_l))))
let id = (Java.mk_var_dec i false Tint) in
Java.Afor (id, Sint 0, s, Java.mk_block (body (List.rev (i::i_l))))
| s::s_l ->
let i = Idents.gen_var "obc2java" "i" in
let id = mk_var_dec i false Tint in
Afor (id, Sint 0, s, mk_block ([aux s_l (i::i_l)]))
let id = Java.mk_var_dec i false Tint in
Java.Afor (id, Sint 0, s, Java.mk_block ([aux s_l (i::i_l)]))
| [] -> Misc.internal_error "Fresh nfor called with empty size list"
in
aux s_l []
(* current module is not translated to keep track,
there is no issue since printed without the qualifier *)
let rec translate_modul m = m (*match m with
let translate_modul m = m (*match m with
| Pervasives
| LocalModule -> m
| _ when m = g_env.current_mod -> m
@ -189,7 +188,7 @@ let rec static_exp param_env se = match se.Types.se_desc with
| Types.Sarray se_l ->
Enew_array (ty param_env se.Types.se_ty, List.map (static_exp param_env) se_l)
| Types.Srecord f_e_l ->
let ty_name =
let ty_name =
match se.Types.se_ty with
| Types.Tid ty_name -> qualname_to_package_classe ty_name
| _ -> Misc.internal_error "Obc2java14"
@ -208,7 +207,7 @@ and boxed_ty param_env t = match Modules.unalias_type t with
| Types.Tid t when t = Initial.pbool -> Tclass (Names.local_qn "Boolean")
| Types.Tid t when t = Initial.pint -> Tclass (Names.local_qn "Integer")
| Types.Tid t when t = Initial.pfloat -> Tclass (Names.local_qn "Float")
| Types.Tid t ->
| Types.Tid t ->
begin try
let ty = find_type t in
begin match ty with
@ -228,7 +227,7 @@ and boxed_ty param_env t = match Modules.unalias_type t with
Tarray (t, s_l)
| Types.Tinvalid -> Misc.internal_error "obc2java invalid type"
and tuple_ty param_env ty_l =
and tuple_ty _param_env ty_l =
let ln = ty_l |> List.length |> Pervasives.string_of_int in
Tclass (java_pervasive_class ("Tuple"^ln))
@ -335,7 +334,7 @@ let obj_ref param_env o = match o with
let jop_of_op param_env op_name e_l =
match op_name with
| { qual = Module "Iostream"; name = "printf" } ->
Emethod_call (Eclass(Names.qualname_of_string "java.lang.System.out"),
Emethod_call (Eclass(Names.qualname_of_string "java.lang.System.out"),
"print",
(exp_list param_env e_l))
| _ ->
@ -344,7 +343,7 @@ let jop_of_op param_env op_name e_l =
let rec act_list param_env act_l acts =
let _act act acts = match act with
| Obc.Aassgn (p,e) -> (Aassgn (pattern param_env p, exp param_env e))::acts
| Obc.Aassgn (p,e) -> (Java.Aassgn (pattern param_env p, exp param_env e))::acts
| Obc.Aop (op,e_l) -> Aexp (jop_of_op param_env op e_l) :: acts
| Obc.Acall (p_l, obj, Mstep, e_l) ->
let o_ref = obj_ref param_env obj in
@ -352,7 +351,7 @@ let rec act_list param_env act_l acts =
let assgn = Aexp ecall in
let copy_return_to_var i p =
let p = pattern param_env p in
Aassgn (p, Emethod_call (o_ref, "getOutput" ^ (string_of_int i), []))
Java.Aassgn (p, Emethod_call (o_ref, "getOutput" ^ (string_of_int i), []))
in
let copies = Misc.mapi copy_return_to_var p_l in
assgn::(copies@acts)
@ -365,14 +364,15 @@ let rec act_list param_env act_l acts =
| [(c,b)] when c = Initial.ptrue ->
(Aif (exp param_env e, block param_env b)):: acts
| [(c,b)] when c = Initial.pfalse ->
(Aifelse (exp param_env e, {b_locals = []; b_body = []}, block param_env b)) :: acts
(Aifelse (exp param_env e, {Java.b_locals = [];
Java.b_body = []}, block param_env b)) :: acts
| _ ->
let _, _then = List.find (fun (c,_) -> c = Initial.ptrue) c_b_l in
let _, _else = List.find (fun (c,_) -> c = Initial.pfalse) c_b_l in
(Aifelse (exp param_env e, block param_env _then, block param_env _else)) :: acts)
| Obc.Acase (e, c_b_l) ->
let _c_b (c,b) =
let type_name =
let _c_b (c,b) =
let type_name =
match e.e_ty with
Types.Tid n -> qualname_to_package_classe n
| _ -> failwith("act_list: translating case") in
@ -382,11 +382,11 @@ let rec act_list param_env act_l acts =
let acase = Aswitch (exp param_env e, List.map _c_b c_b_l) in
acase::acts
| Obc.Afor (v, se, se', b) ->
let afor = Afor (var_dec param_env v,
let afor = Java.Afor (var_dec param_env v,
exp param_env se, exp param_env se', block param_env b) in
afor::acts
| Obc.Ablock b ->
let ablock = Ablock (block param_env b) in
let ablock = Java.Ablock (block param_env b) in
ablock::acts
in
List.fold_right _act act_l acts
@ -395,7 +395,7 @@ and block param_env ?(locals=[]) ?(end_acts=[]) ob =
let blocals = var_dec_list param_env ob.Obc.b_locals in
let locals = locals @ blocals in
let acts = act_list param_env ob.Obc.b_body end_acts in
{ b_locals = locals; b_body = acts }
{ Java.b_locals = locals; Java.b_body = acts }
@ -406,7 +406,7 @@ and block param_env ?(locals=[]) ?(end_acts=[]) ob =
let sig_params_to_vds p_l =
let param_to_arg param_env p =
let p_ident = Idents.gen_var "obc2java" (String.uppercase p.Signature.p_name) in
let p_vd = mk_var_dec p_ident false (ty param_env p.Signature.p_type) in
let p_vd = Java.mk_var_dec p_ident false (ty param_env p.Signature.p_type) in
let param_env = NamesEnv.add p.Signature.p_name p_ident param_env in
p_vd, param_env
in Misc.mapfold param_to_arg NamesEnv.empty p_l
@ -416,12 +416,12 @@ let sig_args_to_vds param_env a_l =
let arg_to_vd { a_name = n; a_type = t } =
let n = match n with None -> "v" | Some s -> s in
let id = Idents.gen_var "obc2java" n in
mk_var_dec id false (ty param_env t)
Java.mk_var_dec id false (ty param_env t)
in List.map arg_to_vd a_l
(** [copy_to_this vd_l] creates [this.x = x] for all [x] in [vd_l] *)
let copy_to_this vd_l =
let _vd vd = Aassgn (Pthis vd.vd_ident, Evar vd.vd_ident) in
let _vd vd = Java.Aassgn (Pthis vd.vd_ident, Evar vd.vd_ident) in
List.map _vd vd_l
@ -431,7 +431,7 @@ let class_def_list classes cd_l =
let class_name = qualname_to_package_classe cd.cd_name in
(* [param_env] is an env mapping local param name to ident *)
(* [params] : fields to stock the static parameters, arguments of the constructors *)
let fields_params, vds_params, exps_params, param_env =
let fields_params, vds_params, _exps_params, param_env =
let v, env = sig_params_to_vds cd.cd_params in
let f = vds_to_fields ~protection:Pprotected v in
let e = vds_to_exps v in
@ -448,7 +448,7 @@ let class_def_list classes cd_l =
let reset_mems = block param_env (remove_resets oreset.Obc.m_body) in
mk_methode body "reset", reset_mems
with Not_found -> (* stub reset method *)
mk_methode (mk_block []) "reset", mk_block []
mk_methode (Java.mk_block []) "reset", Java.mk_block []
in
(* [obj_env] gives the type of an [obj_ident],
needed in async because we change the classe for async obj *)
@ -466,14 +466,14 @@ let class_def_list classes cd_l =
match od.o_size with
| None ->
let t = Idents.Env.find od.o_ident obj_env in
(Aassgn (Pthis od.o_ident, Enew (t, params)))::acts
(Java.Aassgn (Pthis od.o_ident, Enew (t, params)))::acts
| Some size_l ->
let size_l = List.rev (List.map (static_exp param_env) size_l) in
let t = Idents.Env.find od.o_ident obj_env in
let assgn_elem i_l =
[ Aassgn (Parray_elem (Pthis od.o_ident, List.map mk_var i_l), Enew (t, params)) ]
[ Java.Aassgn (Parray_elem (Pthis od.o_ident, List.map mk_var i_l), Enew (t, params)) ]
in
(Aassgn (Pthis od.o_ident, Enew_array (Tarray (t,size_l), [])))
(Java.Aassgn (Pthis od.o_ident, Enew_array (Tarray (t,size_l), [])))
:: (fresh_nfor size_l assgn_elem)
:: acts
in
@ -481,24 +481,24 @@ let class_def_list classes cd_l =
let allocate acts vd = match Modules.unalias_type vd.v_type with
| Types.Tarray _ ->
let t = ty param_env vd.v_type in
( Aassgn (Pthis vd.v_ident, Enew_array (t,[])) ):: acts
( Java.Aassgn (Pthis vd.v_ident, Enew_array (t,[])) ):: acts
| _ -> acts
in
(* init actions [acts] in reverse order : *)
(* init member variables *)
let acts = [Ablock reset_mems] in
let acts = [Java.Ablock reset_mems] in
(* allocate member arrays *)
let acts = List.fold_left allocate acts cd.cd_mems in
(* init member objects *)
let acts = List.fold_left obj_init_act acts cd.cd_objs in
(* init static params *)
let acts = (copy_to_this vds_params)@acts in
{ b_locals = []; b_body = acts }
{ Java.b_locals = []; Java.b_body = acts }
in mk_methode ~args:vds_params body (shortname class_name), obj_env
in
let fields =
let mem_to_field fields vd =
(mk_field ~protection:Pprotected (ty param_env vd.v_type) vd.v_ident) :: fields
(Java.mk_field ~protection:Pprotected (ty param_env vd.v_type) vd.v_ident) :: fields
in
let obj_to_field fields od =
let jty = match od.o_size with
@ -506,7 +506,7 @@ let class_def_list classes cd_l =
| Some size_l -> Tarray (Idents.Env.find od.o_ident obj_env,
List.map (static_exp param_env) size_l)
in
(mk_field ~protection:Pprotected jty od.o_ident) :: fields
(Java.mk_field ~protection:Pprotected jty od.o_ident) :: fields
in
let fields = fields_params in
let fields = List.fold_left mem_to_field fields cd.cd_mems in
@ -514,12 +514,12 @@ let class_def_list classes cd_l =
in
let ostep = find_step_method cd in
let vd_output = var_dec_list param_env ostep.m_outputs in
let output_fields =
List.map (fun vd -> mk_field vd.vd_type vd.vd_ident) vd_output in
let output_fields =
List.map (fun vd -> Java.mk_field vd.vd_type vd.vd_ident) vd_output in
let fields = fields @ output_fields in
let build_output_methods i f =
mk_methode ~returns:f.f_type
(mk_block [Areturn (Evar f.f_ident)])
mk_methode ~returns:f.Java.f_type
(Java.mk_block [Areturn (Evar f.f_ident)])
("getOutput" ^ (string_of_int i))
in
let output_methods = Misc.mapi build_output_methods output_fields in
@ -550,8 +550,8 @@ let type_dec_list classes td_l =
let mk_constr_field (acc_fields,i) c =
let init_value = Sint i in
let c = translate_constructor_name_2 c classe_name in
let field =
mk_field ~static:true ~final:true ~value:(Some init_value)
let field =
Java.mk_field ~static:true ~final:true ~value:(Some init_value)
Tint (Idents.ident_of_name c.name) in
(field::acc_fields),(i+1) in
let fields,_ = List.fold_left mk_constr_field ([],1) c_l in
@ -563,23 +563,24 @@ let type_dec_list classes td_l =
(* [translate_field_name] will give the right result anywhere it is used,
since the [ident_of_name] will keep it as it is unique in the class,
see [Idents.enter_node classe_name] *)
mk_field jty field
Java.mk_field jty field
in
let f_l =
List.sort
List.sort
(fun f1 f2 ->
compare (f1.Signature.f_name.name) (f2.Signature.f_name.name))
f_l in
let fields = List.map mk_field_jfield f_l in
let cons_params = List.map (fun f -> mk_var_dec f.f_ident false f.f_type) fields in
let cons_body =
let cons_params = List.map
(fun f -> Java.mk_var_dec f.f_ident false f.Java.f_type) fields in
let cons_body =
List.map
(fun f -> Aassgn ((Pthis f.f_ident),(Evar f.f_ident)))
(fun f -> Java.Aassgn ((Pthis f.f_ident),(Evar f.f_ident)))
fields in
let cons =
mk_methode
mk_methode
~args:cons_params
(mk_block cons_body)
(Java.mk_block cons_body)
classe_name.name in
(mk_classe ~fields:fields ~constrs:[cons] classe_name) :: classes
in
@ -599,7 +600,7 @@ let const_dec_list cd_l = match cd_l with
(* thus [translate_const_name] will gives the right result anywhere it is used. *)
let value = Some (static_exp param_env ovalue) in
let t = ty param_env otype in
mk_field ~static: true ~final: true ~value: value t name
Java.mk_field ~static: true ~final: true ~value: value t name
in
let fields = List.map mk_const_field cd_l in
[mk_classe ~fields: fields classe_name]
@ -618,6 +619,3 @@ let program p =
let classes = type_dec_list classes ts in
let p = class_def_list classes ns in
get_classes()@p

6
compiler/obc/main/obc_compiler.ml
View file

@ -26,8 +26,6 @@
(* along with Heptagon. If not, see <http://www.gnu.org/licenses/> *)
(* *)
(***********************************************************************)
open Misc
open Location
open Compiler_utils
open Compiler_options
@ -37,7 +35,7 @@ let compile_program p =
(* Memory allocation application *)
let p = pass "Application of Memory Allocation"
(!do_mem_alloc or !do_linear_typing) Memalloc_apply.program p pp in
(!do_mem_alloc || !do_linear_typing) Memalloc_apply.program p pp in
(*Scalarize for wanting backends*)
let p = pass "Scalarize" (!do_scalarize) Scalarize.program p pp in
@ -47,7 +45,7 @@ let compile_program p =
(*Dead code removal*)
let p = pass "Dead code removal"
(!do_mem_alloc or !do_linear_typing) Deadcode.program p pp in
(!do_mem_alloc || !do_linear_typing) Deadcode.program p pp in
(*Control optimization*)
let p = pass "Control optimization" true Control.program p pp in

1
compiler/obc/obc.ml
View file

@ -31,7 +31,6 @@
(** See the manual for the semantics of the language *)
open Misc
open Names
open Idents
open Types

3
compiler/obc/obc_printer.ml
View file

@ -29,8 +29,6 @@
open Obc
open Format
open Pp_tools
open Types
open Idents
open Names
open Global_printer
@ -235,4 +233,3 @@ let print oc p =
let ff = formatter_of_out_channel oc in
fprintf ff "@[-- Code generated by the MiniLucid Compiler@.";
fprintf ff "@[<v>"; print_prog ff p; fprintf ff "@]@]@."

9
compiler/obc/obc_utils.ml
View file

@ -30,7 +30,6 @@
open Names
open Idents
open Location
open Misc
open Types
open Linearity
open Obc
@ -101,7 +100,7 @@ let mk_if cond true_act =
let rec var_name x =
match x.pat_desc with
| Lvar x -> x
| Obc.Lvar x -> x
| Lmem x -> x
| Lfield(x,_) -> var_name x
| Larray(l, _) -> var_name l
@ -110,7 +109,7 @@ let rec var_name x =
a list of var_dec. *)
let rec vd_mem n = function
| [] -> false
| vd::l -> vd.v_ident = n or (vd_mem n l)
| vd::l -> vd.v_ident = n || (vd_mem n l)
(** Returns the var_dec object corresponding to the name n
in a list of var_dec. *)
@ -287,12 +286,12 @@ let interface_types i =
let rec ext_value_of_pattern patt =
let desc = match patt.pat_desc with
| Lvar id -> Wvar id
| Obc.Lvar id -> Wvar id
| Lmem id -> Wmem id
| Lfield (p, fn) -> Wfield (ext_value_of_pattern p, fn)
| Larray (p, e) -> Warray (ext_value_of_pattern p, e) in
mk_ext_value ~loc:patt.pat_loc patt.pat_ty desc
let rec exp_of_pattern patt =
let exp_of_pattern patt =
let w = ext_value_of_pattern patt in
mk_exp w.w_ty (Eextvalue w)

15
compiler/obc/transformations/memalloc_apply.ml
View file

@ -42,7 +42,7 @@ module LinListEnv =
end)
let rec ivar_of_pat l = match l.pat_desc with
| Lvar x -> Ivar x
| Obc.Lvar x -> Ivar x
| Lfield(l, f) -> Ifield (ivar_of_pat l, f)
| _ -> assert false
@ -57,7 +57,7 @@ let rec repr_from_ivar env iv =
(try
let lhs = Env.find x env in lhs.pat_desc
with
Not_found -> Lvar x)
Not_found -> Obc.Lvar x)
| Ifield(iv, f) ->
let ty = Tid (Modules.find_field f) in
let lhs = mk_pattern ty (repr_from_ivar env iv) in
@ -82,9 +82,9 @@ let choose_representative m inputs outputs mems ty vars =
let desc = match inputs, outputs, mems with
| [], [], [] -> choose_record_field m vars
| [], [], (Ivar m)::_ -> Lmem m
| [Ivar vin], [], [] -> Lvar vin
| [], [Ivar vout], [] -> Lvar vout
| [Ivar vin], [Ivar _], [] -> Lvar vin
| [Ivar vin], [], [] -> Obc.Lvar vin
| [], [Ivar vout], [] -> Obc.Lvar vout
| [Ivar vin], [Ivar _], [] -> Obc.Lvar vin
| _, _, _ ->
Interference.print_debug "@.Something is wrong with the coloring : %a@." print_ivar_list vars;
Interference.print_debug "\tInputs : %a@." print_ivar_list inputs;
@ -115,7 +115,7 @@ let memalloc_subst_map inputs outputs mems subst_lists =
let rec lhs funs (env, mut, j) l = match l.pat_desc with
| Lmem _ -> l, (env, mut, j)
| Larray _ | Lfield _ -> Obc_mapfold.lhs funs (env, mut, j) l
| Lvar _ ->
| Obc.Lvar _ ->
(* replace with representative *)
let iv = ivar_of_pat l in
let lhs_desc = repr_from_ivar env iv in
@ -135,7 +135,8 @@ let extvalue funs (env, mut, j) w = match w.w_desc with
| Warray _ | Wfield _ -> Obc_mapfold.extvalue funs (env, mut, j) w
| Wvar x ->
(* replace with representative *)
let lhs, _ = lhs funs (env, mut, j) (mk_pattern Types.invalid_type (Lvar x)) in
let lhs, _ = lhs funs (env, mut, j)
(mk_pattern Types.invalid_type (Obc.Lvar x)) in
let neww = ext_value_of_pattern lhs in
{ w with w_desc = neww.w_desc }, (env, mut, j)

3
compiler/obc/transformations/scalarize.ml
View file

@ -47,7 +47,6 @@
*)
open Misc
open Obc
open Obc_utils
open Obc_mapfold
@ -95,5 +94,3 @@ let act funs () a = match a with
let program p =
let p, _ = program_it { defaults with act = act } () p in
p

Some files were not shown because too many files have changed in this diff Show more