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

blop

Browse source
This commit is contained in:
Léonard Gérard 2011-03-21 14:30:19 +01:00
parent 6428ff81f0
commit b8b16a7355
43 changed files with 443 additions and 301 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
.gitignore vendored
View file

@ -27,3 +27,5 @@ _build
*.dot
test/*.ml
test/_check_builds
lib/java/.classpath
test/async/build/*

1
compiler/global/clocks.ml
View file

@ -95,6 +95,7 @@ let rec skeleton ck = function
assert false;
| _ -> Cprod (List.map (skeleton ck) ty_list))
| Tarray (t, _) -> skeleton ck t
| Tmutable t -> skeleton ck t
| Tid _ | Tunit -> Ck ck
(* TODO here it implicitely says that the base clock is Cbase

2
compiler/global/global_compare.ml
View file

@ -107,4 +107,6 @@ and type_compare ty1 ty2 = match ty1, ty2 with
| Tid _, _ -> 1
| Tarray _, (Tprod _ | Tid _) -> -1
| Tarray _, _ -> 1
| Tmutable _, (Tprod _ | Tid _ | Tarray _) -> -1
| Tmutable _, _ -> 1
| Tunit, _ -> -1

27
compiler/global/global_mapfold.ml
View file

@ -5,19 +5,17 @@ open Types
open Signature
type 'a global_it_funs = {
static_exp :
'a global_it_funs -> 'a -> static_exp -> static_exp * 'a;
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;
link : 'a global_it_funs -> 'a -> link -> link * 'a; *)
param: 'a global_it_funs -> 'a -> param -> param * 'a;
arg: 'a global_it_funs -> 'a -> arg -> arg * 'a;
node : 'a global_it_funs -> 'a -> node -> node * 'a;
structure: 'a global_it_funs -> 'a -> structure -> structure * 'a;
field: 'a global_it_funs -> 'a -> field -> field * 'a; }
static_exp : 'a global_it_funs -> 'a -> static_exp -> static_exp * 'a;
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;
link : 'a global_it_funs -> 'a -> link -> link * 'a; *)
param : 'a global_it_funs -> 'a -> param -> param * 'a;
arg : 'a global_it_funs -> 'a -> arg -> arg * 'a;
node : 'a global_it_funs -> 'a -> node -> node * 'a;
structure : 'a global_it_funs -> 'a -> structure -> structure * 'a;
field : 'a global_it_funs -> 'a -> field -> field * 'a; }
let rec static_exp_it funs acc se = funs.static_exp funs acc se
and static_exp funs acc se =
@ -59,6 +57,9 @@ and ty funs acc t = match t with
let t, acc = ty_it funs acc t in
let se, acc = static_exp_it funs acc se in
Tarray (t, se), acc
| Tmutable t ->
let t, acc = ty_it funs acc t in
Tmutable t, acc
| Tunit -> t, acc
(*
and ct_it funs acc c = try funs.ct funs acc c with Fallback -> ct funs acc t

2
compiler/global/global_printer.ml
View file

@ -70,6 +70,8 @@ and print_type ff = function
| Tid id -> print_qualname ff id
| Tarray (ty, n) ->
fprintf ff "@[<hov2>%a^%a@]" print_type ty print_static_exp n
| Tmutable ty ->
fprintf ff "@[<hov2>mutable %a@]" print_type ty
| Tunit -> fprintf ff "unit"
let print_field ff field =

1
compiler/global/modules.ml
View file

@ -291,6 +291,7 @@ let rec unalias_type t = match t with
with Not_found -> raise (Undefined_type ty_name))
| Tarray (ty, n) -> Tarray(unalias_type ty, n)
| Tprod ty_list -> Tprod (List.map unalias_type ty_list)
| Tmutable t -> Tmutable (unalias_type t)
| Tunit -> Tunit

6
compiler/global/signature.ml
View file

@ -30,7 +30,7 @@ type size_constraint =
type node = {
node_inputs : arg list;
node_outputs : arg list;
node_statefull : bool;
node_stateful : bool;
node_params : param list;
node_params_constraints : size_constraint list }
@ -58,10 +58,10 @@ let mk_field n ty = { f_name = n; f_type = ty }
let mk_const_def ty value =
{ c_type = ty; c_value = value }
let mk_node ?(constraints = []) ins outs statefull params =
let mk_node ?(constraints = []) ins outs stateful params =
{ node_inputs = ins;
node_outputs = outs;
node_statefull = statefull;
node_stateful = stateful;
node_params = params;
node_params_constraints = constraints }

10
compiler/global/static.ml
View file

@ -96,8 +96,14 @@ let rec eval_core partial env se = match se.se_desc with
let cd = find_const ln in
eval_core partial env cd.c_value
with Not_found -> (* then try to find in local env *)
(try eval_core partial env (QualEnv.find ln env)
with Not_found ->
(try
let se = QualEnv.find ln env in
(match se.se_desc with
| Svar ln' when ln'=ln -> (* prevent basic infinite loop *)
if partial then se else raise Not_found
| _ -> eval_core partial env se
)
with Not_found -> (* Could not evaluate the var *)
if partial then se
else raise (Partial_evaluation (Unknown_param ln, se.se_loc))
)

3
compiler/global/types.ml
View file

@ -30,7 +30,8 @@ and static_exp_desc =
and ty =
| Tprod of ty list (** Product type used for tuples *)
| Tid of type_name (** Usable type_name are alias or pervasives {bool,int,float} (see [Initial]) *)
| Tarray of ty * static_exp (** [base_type] * [size] *)
| Tarray of ty * static_exp (** [base_type] * [size] *) (* TODO obc : array of prod ?? nonono *)
| Tmutable of ty (* TODO obc : do not hack it here *)
| Tunit
let invalid_type = Tprod [] (** Invalid type given to untyped expression etc. *)

67
compiler/heptagon/analysis/statefull.ml
View file

@ -6,7 +6,7 @@
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
(* *)
(**************************************************************************)
(* Checks that a node declared stateless is stateless *)
(* Checks that a node declared stateless is stateless, and set possible nodes as stateless. *)
open Names
open Location
open Signature
@ -21,7 +21,7 @@ type error =
let message loc kind =
begin match kind with
| Eshould_be_a_node ->
Format.eprintf "%aThis node is statefull \
Format.eprintf "%aThis node is stateful \
but was declared stateless.@."
print_location loc
| Eexp_should_be_stateless ->
@ -30,54 +30,73 @@ let message loc kind =
end;
raise Errors.Error
(** @returns whether the exp is statefull. Replaces node calls with
let last _ stateful l = match l with
| Var -> l, stateful
| Last _ -> l, true
(** @returns whether the exp is stateful. Replaces node calls with
the correct Efun or Enode depending on the node signature. *)
let edesc funs statefull ed =
(* do the recursion on function args *)
let ed, statefull = Hept_mapfold.edesc funs statefull ed in
let edesc funs stateful ed =
let ed, stateful = Hept_mapfold.edesc funs stateful ed in
match ed with
| Efby _ | Epre _ -> ed, true
| Eapp({ a_op = Earrow }, _, _) -> ed, true
| 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_statefull then Enode f else Efun f in
Eapp({ app with a_op = op }, e_list, r),
ty_desc.node_statefull or statefull
| _ -> ed, statefull
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
| _ -> ed, stateful
let eqdesc funs acc eqd =
let eqd, _ = Hept_mapfold.eqdesc funs acc eqd in
match eqd with
| Eautomaton st_h_l ->
let st_h_l, _ = Misc.mapfold (state_handler_it funs) acc st_h_l in
Eautomaton st_h_l, true
| _ -> raise Errors.Fallback
let eq funs acc eq =
let eq, statefull = Hept_mapfold.eq funs acc eq in
{ eq with eq_statefull = statefull }, statefull
let eq, stateful = Hept_mapfold.eq funs acc eq in
{ eq with eq_stateful = stateful }, stateful
let block funs acc b =
let b, statefull = Hept_mapfold.block funs false b in
{ b with b_statefull = statefull }, acc or statefull
let b, stateful = Hept_mapfold.block funs false b in
{ b with b_stateful = stateful }, acc or stateful
(** Strong preemption should be decided with stateless expressions *)
let escape_unless funs acc esc =
let esc, statefull = Hept_mapfold.escape funs false esc in
if statefull then
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 statefull
esc, acc or stateful
(** Present conditions should be stateless *)
let present_handler funs acc ph =
let p_cond, statefull = Hept_mapfold.exp_it funs false ph.p_cond in
if statefull then
let p_cond, stateful = Hept_mapfold.exp_it funs false ph.p_cond in
if stateful then
message ph.p_cond.e_loc Eexp_should_be_stateless;
let p_block, acc = Hept_mapfold.block_it funs acc ph.p_block in
{ ph with p_cond = p_cond; p_block = p_block }, acc
(** Funs with states are rejected, nodes without state are set as funs *)
let node_dec funs _ n =
Idents.enter_node n.n_name;
let n, statefull = Hept_mapfold.node_dec funs false n in
if statefull & not (n.n_statefull) then
message n.n_loc Eshould_be_a_node;
n, false
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 *)
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 *)
let program p =
let funs =
{ Hept_mapfold.defaults with edesc = edesc;
{ Hept_mapfold.defaults with
edesc = edesc;
escape_unless = escape_unless;
present_handler = present_handler;
eqdesc = eqdesc;
last = last;
eq = eq; block = block; node_dec = node_dec } in
let p, _ = Hept_mapfold.program_it funs false p in
p

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

@ -223,7 +223,7 @@ let unify t1 t2 =
let kind f ty_desc =
let ty_of_arg v = v.a_type in
let op = if ty_desc.node_statefull then Enode f else Efun f in
let op = if ty_desc.node_stateful then Enode f else Efun f in
op, List.map ty_of_arg ty_desc.node_inputs,
List.map ty_of_arg ty_desc.node_outputs
@ -250,6 +250,7 @@ let build_subst names values =
let rec subst_type_vars m = function
| Tarray(ty, e) -> Tarray(subst_type_vars m ty, simplify m e)
| Tprod l -> Tprod (List.map (subst_type_vars m) l)
| Tmutable t -> Tmutable (subst_type_vars m t)
| t -> t
let add_distinct_env id ty env =
@ -384,6 +385,8 @@ let rec check_type const_env = function
| Tid ty_name -> Tid ty_name (* TODO bug ? should check that ty_name exists ? *)
| Tprod l ->
Tprod (List.map (check_type const_env) l)
| Tmutable t ->
Tmutable (check_type const_env t)
| Tunit -> Tunit
and typing_static_exp const_env se =

63
compiler/heptagon/hept_mapfold.ml
View file

@ -54,46 +54,25 @@ open Global_mapfold
open Heptagon
type 'a hept_it_funs = {
app:
'a hept_it_funs -> 'a -> Heptagon.app -> Heptagon.app * 'a;
block:
'a hept_it_funs -> 'a -> Heptagon.block -> Heptagon.block * 'a;
edesc:
'a hept_it_funs -> 'a -> Heptagon.desc -> Heptagon.desc * 'a;
eq:
'a hept_it_funs -> 'a -> Heptagon.eq -> Heptagon.eq * 'a;
eqdesc:
'a hept_it_funs -> 'a -> Heptagon.eqdesc -> Heptagon.eqdesc * 'a;
escape_unless :
'a hept_it_funs -> 'a -> Heptagon.escape -> Heptagon.escape * 'a;
escape_until:
'a hept_it_funs -> 'a -> Heptagon.escape -> Heptagon.escape * 'a;
exp:
'a hept_it_funs -> 'a -> Heptagon.exp -> Heptagon.exp * 'a;
pat:
'a hept_it_funs -> 'a -> pat -> Heptagon.pat * 'a;
present_handler:
'a hept_it_funs -> 'a -> Heptagon.present_handler
-> Heptagon.present_handler * 'a;
state_handler:
'a hept_it_funs -> 'a -> Heptagon.state_handler
-> Heptagon.state_handler * 'a;
switch_handler:
'a hept_it_funs -> 'a -> Heptagon.switch_handler
-> Heptagon.switch_handler * 'a;
var_dec:
'a hept_it_funs -> 'a -> Heptagon.var_dec -> Heptagon.var_dec * 'a;
last:
'a hept_it_funs -> 'a -> Heptagon.last -> Heptagon.last * 'a;
contract:
'a hept_it_funs -> 'a -> Heptagon.contract -> Heptagon.contract * 'a;
node_dec:
'a hept_it_funs -> 'a -> Heptagon.node_dec -> Heptagon.node_dec * 'a;
const_dec:
'a hept_it_funs -> 'a -> Heptagon.const_dec -> Heptagon.const_dec * 'a;
program:
'a hept_it_funs -> 'a -> Heptagon.program -> Heptagon.program * 'a;
global_funs: 'a Global_mapfold.global_it_funs }
app : 'a hept_it_funs -> 'a -> app -> app * 'a;
block : 'a hept_it_funs -> 'a -> block -> block * 'a;
edesc : 'a hept_it_funs -> 'a -> desc -> desc * 'a;
eq : 'a hept_it_funs -> 'a -> eq -> eq * 'a;
eqdesc : 'a hept_it_funs -> 'a -> eqdesc -> eqdesc * 'a;
escape_unless : 'a hept_it_funs -> 'a -> escape -> escape * 'a;
escape_until : 'a hept_it_funs -> 'a -> escape -> escape * 'a;
exp : 'a hept_it_funs -> 'a -> exp -> exp * 'a;
pat : 'a hept_it_funs -> 'a -> pat -> pat * 'a;
present_handler: 'a hept_it_funs -> 'a -> present_handler -> present_handler * 'a;
state_handler : 'a hept_it_funs -> 'a -> state_handler -> state_handler * 'a;
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;
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;
program : 'a hept_it_funs -> 'a -> program -> program * 'a;
global_funs : 'a Global_mapfold.global_it_funs }
let rec exp_it funs acc e = funs.exp funs acc e
@ -200,7 +179,7 @@ and eqdesc funs acc eqd = match eqd with
and block_it funs acc b = funs.block funs acc b
and block funs acc b =
(* defnames ty ?? *)
(* TODO defnames ty ?? *)
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
{ b with b_local = b_local; b_equs = b_equs }, acc
@ -238,7 +217,7 @@ and present_handler funs acc ph =
and var_dec_it funs acc vd = funs.var_dec funs acc vd
and var_dec funs acc vd =
(* v_type ??? *)
(* TODO v_type ??? *)
let v_last, acc = last_it funs acc vd.v_last in
{ vd with v_last = v_last }, acc

26
compiler/heptagon/heptagon.ml
View file

@ -76,7 +76,7 @@ and pat =
type eq = {
eq_desc : eqdesc;
eq_statefull : bool;
eq_stateful : bool;
eq_loc : location; }
and eqdesc =
@ -91,7 +91,7 @@ and block = {
b_local : var_dec list;
b_equs : eq list;
b_defnames : ty Env.t;
b_statefull : bool;
b_stateful : bool;
b_loc : location; }
and state_handler = {
@ -141,7 +141,7 @@ type contract = {
type node_dec = {
n_name : qualname;
n_statefull : bool;
n_stateful : bool;
n_input : var_dec list;
n_output : var_dec list;
n_contract : contract option;
@ -166,7 +166,7 @@ type program = {
type signature = {
sig_name : qualname;
sig_inputs : arg list;
sig_statefull : bool;
sig_stateful : bool;
sig_outputs : arg list;
sig_params : param list;
sig_loc : location }
@ -197,16 +197,16 @@ let mk_op_app ?(params=[]) ?(unsafe=false) ?(reset=None) op args =
let mk_type_dec name desc =
{ t_name = name; t_desc = desc; t_loc = no_location; }
let mk_equation ?(statefull = true) desc =
{ eq_desc = desc; eq_statefull = statefull; eq_loc = no_location; }
let mk_equation ?(stateful = true) desc =
{ eq_desc = desc; eq_stateful = stateful; eq_loc = no_location; }
let mk_var_dec ?(last = Var) ?(ck = fresh_clock()) name ty =
{ v_ident = name; v_type = ty; v_clock = ck;
v_last = last; v_loc = no_location }
let mk_block ?(statefull = true) ?(defnames = Env.empty) ?(locals = []) eqs =
let mk_block ?(stateful = true) ?(defnames = Env.empty) ?(locals = []) eqs =
{ b_local = locals; b_equs = eqs; b_defnames = defnames;
b_statefull = statefull; b_loc = no_location; }
b_stateful = stateful; b_loc = no_location; }
let dfalse =
mk_exp (Econst (mk_static_bool false)) (Tid Initial.pbool)
@ -217,15 +217,15 @@ let mk_ifthenelse e1 e2 e3 =
{ e3 with e_desc = mk_op_app Eifthenelse [e1; e2; e3] }
let mk_simple_equation pat e =
mk_equation ~statefull:false (Eeq(pat, e))
mk_equation ~stateful:false (Eeq(pat, e))
let mk_switch_equation ?(statefull = true) e l =
mk_equation ~statefull:statefull (Eswitch (e, l))
let mk_switch_equation ?(stateful = true) e l =
mk_equation ~stateful:stateful (Eswitch (e, l))
let mk_signature name ins outs statefull params loc =
let mk_signature name ins outs stateful params loc =
{ sig_name = name;
sig_inputs = ins;
sig_statefull = statefull;
sig_stateful = stateful;
sig_outputs = outs;
sig_params = params;
sig_loc = loc }

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

@ -47,7 +47,6 @@ open Hept_parsetree
%token AROBASE
%token DOUBLE_LESS DOUBLE_GREATER
%token MAP FOLD FOLDI MAPFOLD
%token ASYNC BANG
%token <string> PREFIX
%token <string> INFIX0
%token <string> INFIX1
@ -59,7 +58,6 @@ open Hept_parsetree
%right AROBASE
%nonassoc prec_ident
%nonassoc DEFAULT
%left ELSE
%right ARROW
@ -77,8 +75,7 @@ open Hept_parsetree
%right PRE
%left POWER
%right PREFIX
%left DOT
%left BANG
%start program
@ -190,7 +187,7 @@ node_dec:
RETURNS LPAREN out_params RPAREN
contract b=block(LET) TEL
{{ n_name = $2;
n_statefull = $1;
n_stateful = $1;
n_input = $5;
n_output = $9;
n_contract = $11;
@ -547,7 +544,7 @@ modul:
| m=modul DOT c=Constructor { Names.QualModule { Names.qual = m; Names.name = c} }
constructor:
| Constructor { ToQ $1 } %prec prec_ident
| Constructor { ToQ $1 }
| q=qualified(Constructor) { q }
;
@ -626,7 +623,7 @@ _interface_decl:
RETURNS LPAREN params_signature RPAREN
{ Isignature({ sig_name = $3;
sig_inputs = $6;
sig_statefull = $2;
sig_stateful = $2;
sig_outputs = $10;
sig_params = $4;
sig_loc = (Loc($startpos,$endpos)) }) }

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

@ -162,7 +162,7 @@ type contract =
type node_dec =
{ n_name : dec_name;
n_statefull : bool;
n_stateful : bool;
n_input : var_dec list;
n_output : var_dec list;
n_contract : contract option;
@ -191,7 +191,7 @@ type arg =
type signature =
{ sig_name : dec_name;
sig_inputs : arg list;
sig_statefull : bool;
sig_stateful : bool;
sig_outputs : arg list;
sig_params : var_dec list;
sig_loc : location }

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

@ -296,7 +296,7 @@ and translate_pat loc env = function
let rec translate_eq env eq =
{ Heptagon.eq_desc = translate_eq_desc eq.eq_loc env eq.eq_desc ;
Heptagon.eq_statefull = false;
Heptagon.eq_stateful = false;
Heptagon.eq_loc = eq.eq_loc; }
and translate_eq_desc loc env = function
@ -326,7 +326,7 @@ and translate_block env b =
{ Heptagon.b_local = translate_vd_list env b.b_local;
Heptagon.b_equs = List.map (translate_eq env) b.b_equs;
Heptagon.b_defnames = Env.empty;
Heptagon.b_statefull = false;
Heptagon.b_stateful = false;
Heptagon.b_loc = b.b_loc; }, env
and translate_state_handler env sh =
@ -402,9 +402,9 @@ let translate_node node =
let i = args_of_var_decs node.n_input in
let o = args_of_var_decs node.n_output in
let p = params_of_var_decs node.n_params in
add_value n (Signature.mk_node i o node.n_statefull p);
add_value n (Signature.mk_node i o node.n_stateful p);
{ Heptagon.n_name = n;
Heptagon.n_statefull = node.n_statefull;
Heptagon.n_stateful = node.n_stateful;
Heptagon.n_input = inputs;
Heptagon.n_output = outputs;
Heptagon.n_contract = contract;
@ -469,8 +469,8 @@ let translate_signature s =
let i = List.map translate_arg s.sig_inputs in
let o = List.map translate_arg s.sig_outputs in
let p = params_of_var_decs s.sig_params in
add_value n (Signature.mk_node i o s.sig_statefull p);
Heptagon.mk_signature n i o s.sig_statefull p s.sig_loc
add_value n (Signature.mk_node i o s.sig_stateful p);
Heptagon.mk_signature n i o s.sig_stateful p s.sig_loc
let translate_interface_desc = function

4
compiler/heptagon/transformations/inline.ml
View file

@ -56,7 +56,7 @@ let exp funs (env, newvars, newequs) exp = match exp.e_desc with
| Eapp ({ a_op = Enode nn; } as op, argl, rso) when to_be_inlined nn ->
let add_reset eq = match rso with
| None -> eq
| Some x -> mk_equation ~statefull:false
| Some x -> mk_equation ~stateful:false
(Ereset (mk_block [eq], x)) in
let ni = mk_unique_node (env nn) in
@ -80,7 +80,7 @@ let exp funs (env, newvars, newequs) exp = match exp.e_desc with
fst (Hept_mapfold.node_dec funs () ni) in
let mk_input_equ vd e =
mk_equation ~statefull:false (Eeq (Evarpat vd.v_ident, e)) in
mk_equation ~stateful:false (Eeq (Evarpat vd.v_ident, e)) in
let mk_output_exp vd = mk_exp (Evar vd.v_ident) vd.v_type in
let newvars = ni.n_input @ ni.n_block.b_local @ ni.n_output @ newvars

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

@ -13,10 +13,10 @@ open Hept_mapfold
let translate_present_handlers handlers cont =
let translate_present_handler { p_cond = e; p_block = b } cont =
let statefull = b.b_statefull or cont.b_statefull in
mk_block ~statefull:statefull ~defnames:b.b_defnames
let stateful = b.b_stateful or cont.b_stateful in
mk_block ~stateful:stateful ~defnames:b.b_defnames
[mk_switch_equation
~statefull:statefull e
~stateful:stateful e
[{ w_name = Initial.ptrue; w_block = b };
{ w_name = Initial.pfalse; w_block = cont }]] in
let b = List.fold_right translate_present_handler handlers cont in

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

@ -8,7 +8,7 @@
(**************************************************************************)
(* removing reset statements *)
(* REQUIRES automaton switch statefull present *)
(* REQUIRES automaton switch stateful present *)
open Misc
open Idents
@ -74,7 +74,7 @@ let edesc funs (res,s) ed =
let eq funs (res,_) eq = Hept_mapfold.eq funs (res,eq.eq_statefull) eq
let eq funs (res,_) eq = Hept_mapfold.eq funs (res,eq.eq_stateful) eq
(* Transform reset blocks in blocks with reseted exps, create a var to store the reset condition evaluation. *)
let eqdesc funs (res,stateful) = function
@ -85,7 +85,7 @@ let eqdesc funs (res,stateful) = function
let e, vd, eq = bool_var_from_exp e in
let r = merge_resets res (Some e) in
let b, _ = Hept_mapfold.block_it funs (r,true) b in
let b = { b with b_equs = eq::b.b_equs; b_local = vd::b.b_local; b_statefull = true } in
let b = { b with b_equs = eq::b.b_equs; b_local = vd::b.b_local; b_stateful = true } in
Eblock(b), (res,true))
else (
let b, _ = Hept_mapfold.block_it funs (res,false) b in

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

@ -155,11 +155,11 @@ let exp funs (env,h) e =
| Evar _ -> Env.sample_var e env, (env,h)
| _ -> Hept_mapfold.exp funs (env,h) e
(* update statefull and loc *)
(* update stateful and loc *)
let eq funs (env,h) eq =
let eqd = match eq.eq_desc with
| Eblock b -> (* probably created by eqdesc, so update statefull and loc *)
Eblock { b with b_statefull = eq.eq_statefull; b_loc = eq.eq_loc }
| Eblock b -> (* probably created by eqdesc, so update stateful and loc *)
Eblock { b with b_stateful = eq.eq_stateful; b_loc = eq.eq_loc }
| _ -> eq.eq_desc in
Hept_mapfold.eq funs (env,h) {eq with eq_desc = eqd}

5
compiler/main/hept2mls.ml
View file

@ -377,7 +377,7 @@ let translate_contract env contract =
let node
{ Heptagon.n_name = n; Heptagon.n_input = i; Heptagon.n_output = o;
Heptagon.n_contract = contract;
Heptagon.n_contract = contract; Heptagon.n_stateful = stateful;
Heptagon.n_block = { Heptagon.b_local = v; Heptagon.b_equs = eq_list };
Heptagon.n_loc = loc;
Heptagon.n_params = params;
@ -390,10 +390,11 @@ let node
translate_eqs env IdentSet.empty (locals, [], []) eq_list in
let l_eqs, _ = add_locals IdentSet.empty l_eqs [] s_eqs in
{ n_name = n;
n_stateful = stateful;
n_input = List.map translate_var i;
n_output = List.map translate_var o;
n_contract = contract;
n_controller_call = ([],[]);
(* n_controller_call = ([],[]); *)
n_local = locals;
n_equs = l_eqs;
n_loc = loc ;

82
compiler/main/mls2obc.ml
View file

@ -31,7 +31,7 @@ let op_from_string op = { qual = Pervasives; name = op; }
let rec pattern_of_idx_list p l =
let rec aux ty l = match ty, l with
| _, [] -> p
| Tarray (ty',_), idx :: l -> mk_pattern ty (Larray (aux ty' l, idx))
| Tarray (ty',_), idx :: l -> mk_pattern ty' (Larray (aux ty' l, idx))
| _ -> internal_error "mls2obc" 1
in
aux p.pat_ty l
@ -140,12 +140,12 @@ and translate_act map pat
let e2 = translate map e2 in
let a1 =
Afor (cpt1d, mk_static_int 0, n1,
mk_block [Aassgn (mk_pattern t (Larray (x, mk_evar_int cpt1)),
mk_block [Aassgn (mk_pattern t1 (Larray (x, mk_evar_int cpt1)),
mk_pattern_exp t1 (Larray (pattern_of_exp e1, mk_evar_int cpt1)))] ) in
let idx = mk_exp_int (Eop (op_from_string "+", [ mk_exp_int (Econst n1); mk_evar_int cpt2])) in
let a2 =
Afor (cpt2d, mk_static_int 0, n2,
mk_block [Aassgn (mk_pattern t (Larray (x, idx)),
mk_block [Aassgn (mk_pattern t2 (Larray (x, idx)),
mk_pattern_exp t2 (Larray (pattern_of_exp e2, mk_evar_int cpt2)))] )
in
[a1; a2]
@ -154,18 +154,26 @@ and translate_act map pat
let cpt, cptd = fresh_it () in
let e = translate map e in
let x = Control.var_from_name map x in
[ Afor (cptd, mk_static_int 0, n, mk_block [Aassgn (mk_pattern x.pat_ty (Larray (x, mk_evar_int cpt)), e) ]) ]
let t = match x.pat_ty with
| Tarray (t,_) -> t
| _ -> Misc.internal_error "mls2obc select slice type" 5
in
[ Afor (cptd, mk_static_int 0, n, mk_block [Aassgn (mk_pattern t (Larray (x, mk_evar_int cpt)), e) ]) ]
| Minils.Evarpat x, Minils.Eapp ({ Minils.a_op = Minils.Eselect_slice; Minils.a_params = [idx1; idx2] }, [e], _) ->
let cpt, cptd = fresh_it () in
let e = translate map e in
let x = Control.var_from_name map x in
let t = match x.pat_ty with
| Tarray (t,_) -> t
| _ -> Misc.internal_error "mls2obc select slice type" 5
in
let idx = mk_exp_int (Eop (op_from_string "+", [mk_evar_int cpt; mk_exp_int (Econst idx1) ])) in
(* bound = (idx2 - idx1) + 1*)
let bound = mk_static_int_op (op_from_string "+")
[ mk_static_int 1; mk_static_int_op (op_from_string "-") [idx2;idx1] ] in
[ Afor (cptd, mk_static_int 0, bound,
mk_block [Aassgn (mk_pattern x.pat_ty (Larray (x, mk_evar_int cpt)),
mk_pattern_exp e.e_ty (Larray (pattern_of_exp e, idx)))] ) ]
mk_block [Aassgn (mk_pattern t (Larray (x, mk_evar_int cpt)),
mk_pattern_exp t (Larray (pattern_of_exp e, idx)))] ) ]
| Minils.Evarpat x, Minils.Eapp ({ Minils.a_op = Minils.Eselect_dyn }, e1::e2::idx, _) ->
let x = Control.var_from_name map x in
let bounds = Mls_utils.bounds_list e1.Minils.e_ty in
@ -191,7 +199,7 @@ and translate_act map pat
Minils.Eapp ({ Minils.a_op = Minils.Efield_update; Minils.a_params = [{ se_desc = Sfield f }] }, [e1; e2], _) ->
let x = Control.var_from_name map x in
let copy = Aassgn (x, translate map e1) in
let action = Aassgn (mk_pattern x.pat_ty (Lfield (x, f)), translate map e2) in
let action = Aassgn (mk_pattern x.pat_ty (Lfield (x, f)), translate map e2) in (* TODO wrong type *)
[copy; action]
| Minils.Evarpat n, _ ->
@ -449,15 +457,9 @@ let subst_map inputs outputs locals mem_tys =
List.fold_left (fun map (x, x_ty) -> Env.add x (mk_pattern x_ty (Lmem x)) map) map mem_tys
let translate_node
({
Minils.n_name = f;
Minils.n_input = i_list;
Minils.n_output = o_list;
Minils.n_local = d_list;
Minils.n_equs = eq_list;
Minils.n_contract = contract;
Minils.n_params = params;
Minils.n_loc = loc;
({ Minils.n_name = f; Minils.n_input = i_list; Minils.n_output = o_list;
Minils.n_local = d_list; Minils.n_equs = eq_list; Minils.n_stateful = stateful;
Minils.n_contract = contract; Minils.n_params = params; Minils.n_loc = loc;
} as n) =
Idents.enter_node f;
let mem_var_tys = Mls_utils.node_memory_vars n in
@ -467,20 +469,21 @@ let translate_node
let i_list = translate_var_dec i_list in
let o_list = translate_var_dec o_list in
let d_list = translate_var_dec (v @ d_list) in
let m, d_list = List.partition
(fun vd -> List.exists (fun (i,_) -> i = vd.v_ident) mem_var_tys) d_list in
let m, d_list = List.partition (fun vd -> List.exists (fun (i,_) -> i = vd.v_ident) mem_var_tys) d_list in
let s = Control.joinlist (s_list @ s_list') in
let j = j' @ j in
let si = Control.joinlist (si @ si') in
let stepm = {
m_name = Mstep; m_inputs = i_list; m_outputs = o_list;
m_body = mk_block ~locals:(d_list' @ d_list) s } in
let resetm = {
m_name = Mreset; m_inputs = []; m_outputs = [];
m_body = mk_block si } in
{ cd_name = f; cd_mems = m; cd_params = params;
cd_objs = j; cd_methods = [stepm; resetm];
cd_loc = loc }
let stepm = { m_name = Mstep; m_inputs = i_list; m_outputs = o_list;
m_body = mk_block ~locals:(d_list' @ d_list) s }
in
let resetm = { m_name = Mreset; m_inputs = []; m_outputs = []; m_body = mk_block si } in
if stateful
then { cd_name = f; cd_stateful = true; cd_mems = m; cd_params = params;
cd_objs = j; cd_methods = [stepm; resetm]; cd_loc = loc; }
else ( (* Functions won't have [Mreset] or memories, they still have [params] and instances (of functions) *)
{ cd_name = f; cd_stateful = false; cd_mems = []; cd_params = params;
cd_objs = j; cd_methods = [stepm]; cd_loc = loc; }
)
let translate_ty_def { Minils.t_name = name; Minils.t_desc = tdesc;
Minils.t_loc = loc } =
@ -488,8 +491,8 @@ let translate_ty_def { Minils.t_name = name; Minils.t_desc = tdesc;
| Minils.Type_abs -> Type_abs
| Minils.Type_alias ln -> Type_alias ln
| Minils.Type_enum tag_name_list -> Type_enum tag_name_list
| Minils.Type_struct field_ty_list ->
Type_struct field_ty_list in
| Minils.Type_struct field_ty_list -> Type_struct field_ty_list
in
{ t_name = name; t_desc = tdesc; t_loc = loc }
let translate_const_def { Minils.c_name = name; Minils.c_value = se;
@ -499,19 +502,12 @@ let translate_const_def { Minils.c_name = name; Minils.c_value = se;
c_type = ty;
c_loc = loc }
let program {
Minils.p_modname = p_modname;
Minils.p_opened = p_module_list;
Minils.p_types = p_type_list;
Minils.p_nodes = p_node_list;
Minils.p_consts = p_const_list
} =
{
p_modname = p_modname;
p_opened = p_module_list;
p_types = List.map translate_ty_def p_type_list;
p_consts = List.map translate_const_def p_const_list;
p_defs = List.map translate_node p_node_list;
}
let program { Minils.p_modname = p_modname; Minils.p_opened = p_module_list; Minils.p_types = p_type_list;
Minils.p_nodes = p_node_list; Minils.p_consts = p_const_list } =
{ p_modname = p_modname;
p_opened = p_module_list;
p_types = List.map translate_ty_def p_type_list;
p_consts = List.map translate_const_def p_const_list;
p_classes = List.map translate_node p_node_list; }

7
compiler/minils/main/mls2seq.ml
View file

@ -19,6 +19,7 @@ open Misc
type target =
| Obc of (Obc.program -> unit)
| Obc_no_params of (Obc.program -> unit)
| Obc_scalar of (Obc.program ->unit)
| Minils of (Minils.program -> unit)
| Minils_no_params of (Minils.program -> unit)
@ -38,8 +39,9 @@ let write_obc_file p =
close_out obc;
comment "Generation of Obc code"
let targets = [ "c", Obc_no_params Cmain.program;
"java", Obc Java_main.program;
"java", Obc_scalar Java_main.program;
"obc", Obc write_obc_file;
"obc_np", Obc_no_params write_obc_file;
"epo", Minils write_object_file ]
@ -69,6 +71,9 @@ let generate_target p s =
if !verbose then
List.iter (Obc_printer.print stdout) o_list;
List.iter convert_fun o_list
| Obc_scalar convert_fun ->
let p = p |> Mls2obc.program |> Scalarize.program in
convert_fun p
(** Translation into dataflow and sequential languages, defaults to obc. *)

11
compiler/minils/minils.ml
View file

@ -106,11 +106,12 @@ type contract = {
type node_dec = {
n_name : qualname;
n_stateful : bool;
n_input : var_dec list;
n_output : var_dec list;
n_contract : contract option;
(* GD: inglorious hack for controller call *)
mutable n_controller_call : var_ident list * var_ident list;
(* GD: inglorious hack for controller call
mutable n_controller_call : var_ident list * var_ident list; *)
n_local : var_dec list;
n_equs : eq list;
n_loc : location;
@ -146,13 +147,14 @@ let mk_equation ?(loc = no_location) pat exp =
let mk_node
?(input = []) ?(output = []) ?(contract = None) ?(local = []) ?(eq = [])
?(loc = no_location) ?(param = []) ?(constraints = [])
?(stateful = true) ?(loc = no_location) ?(param = []) ?(constraints = [])
?(pinst = ([],[])) name =
{ n_name = name;
n_stateful = stateful;
n_input = input;
n_output = output;
n_contract = contract;
n_controller_call = pinst;
(* n_controller_call = pinst;*)
n_local = local;
n_equs = eq;
n_loc = loc;
@ -174,4 +176,3 @@ let mk_program o n t c =
p_opened = o; p_nodes = n; p_types = t; p_consts = c }
let void = mk_exp ~ty:Types.Tunit (Eapp (mk_app Etuple, [], None))

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

@ -14,7 +14,7 @@ module Error =
struct
type error =
| Enode_unbound of qualname
| Epartial_evaluation of static_exp
| Epartial_evaluation of static_exp list
let message loc kind =
begin match kind with
@ -22,10 +22,10 @@ struct
Format.eprintf "%aUnknown node '%s'@."
print_location loc
(fullname ln)
| Epartial_evaluation se ->
Format.eprintf "%aUnable to fully instanciate the static exp '%a'@."
print_location se.se_loc
print_static_exp se
| Epartial_evaluation se_l ->
Format.eprintf "%aUnable to fully instanciate the static exps '%a'@."
print_location loc
print_static_exp_tuple se_l
end;
raise Errors.Error
end
@ -77,10 +77,10 @@ struct
let nodes_instances = ref QualEnv.empty
(** create a params instance *)
let instantiate m se =
try List.map (eval m) se
with Errors.Error se ->
Error.message no_location (Error.Epartial_evaluation se)
let instantiate m se_l =
try List.map (eval m) se_l
with Errors.Error ->
Error.message no_location (Error.Epartial_evaluation se_l)
(** @return the name of the node corresponding to the instance of
[ln] with the static parameters [params]. *)

2
compiler/minils/transformations/checkpass.ml
View file

@ -46,7 +46,7 @@ let add_check prefix pass nd nd_list =
Modules.add_value nd_check.n_name
{ node_inputs = [];
node_outputs = [{ a_name = None; a_type = Tid Initial.pbool; }];
node_statefull = true;
node_stateful = true;
node_params = [];
node_params_constraints = [] };

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

@ -405,7 +405,7 @@ let rec reconstruct input_type (env : PatEnv.t) =
| Etuplepat pat_list, Tprod ty_list ->
List.fold_right2 mk_var_decs pat_list ty_list var_list
| Etuplepat [], Tunit -> var_list
| Etuplepat _, (Tarray _ | Tid _ | Tunit ) -> assert false (* ill-typed *) in
| Etuplepat _, (Tarray _ | Tid _ | Tunit | Tmutable _) -> assert false (* ill-typed *) in
let add_to_lists pat (_, head, children) (eq_list, var_list) =
(* Remember the encoding of resets given above. *)

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

@ -73,10 +73,10 @@ let output_names_list sig_info =
in
List.map remove_option sig_info.node_outputs
let is_statefull n =
let is_stateful n =
try
let sig_info = find_value n in
sig_info.node_statefull
sig_info.node_stateful
with
Not_found -> Error.message no_location (Error.Enode (fullname n))
@ -100,8 +100,8 @@ let rec ctype_of_otype oty =
| Types.Tid id when id = Initial.pfloat -> Cty_float
| Types.Tid id when id = Initial.pbool -> Cty_int
| Tid id -> Cty_id id
| Tarray(ty, n) -> Cty_arr(int_of_static_exp n,
ctype_of_otype ty)
| Tarray(ty, n) -> Cty_arr(int_of_static_exp n, ctype_of_otype ty)
| Tmutable t -> ctype_of_otype t
| Tprod _ -> assert false
| Tunit -> assert false
@ -362,7 +362,7 @@ let out_var_name_of_objn o =
of the called node, [mem] represents the node context and [args] the
argument list.*)
let step_fun_call var_env sig_info objn out args =
if sig_info.node_statefull then (
if sig_info.node_stateful then (
let mem =
(match objn with
| Oobj o -> Cfield (Cderef (Cvar "self"), local_qn (name o))
@ -471,7 +471,7 @@ let rec cstm_of_act var_env obj_env act =
(** For composition of statements, just recursively apply our
translation function on sub-statements. *)
| Afor ({ v_ident = x; _ }, i1, i2, act) ->
| Afor ({ v_ident = x }, i1, i2, act) ->
[Cfor(name x, int_of_static_exp i1,
int_of_static_exp i2, cstm_of_act_list var_env obj_env act)]
@ -541,7 +541,7 @@ let step_fun_args n md =
let args = cvarlist_of_ovarlist md.m_inputs in
let out_arg = [("out", Cty_ptr (Cty_id (qn_append n "_out")))] in
let context_arg =
if is_statefull n then
if is_stateful n then
[("self", Cty_ptr (Cty_id (qn_append n "_mem")))]
else
[]
@ -594,7 +594,7 @@ let mem_decl_of_class_def cd =
(** This one just translates the class name to a struct name following the
convention we described above. *)
let struct_field_of_obj_dec l od =
if is_statefull od.o_class then
if is_stateful od.o_class then
let ty = Cty_id (qn_append od.o_class "_mem") in
let ty = match od.o_size with
| Some se -> Cty_arr (int_of_static_exp se, ty)
@ -603,7 +603,7 @@ let mem_decl_of_class_def cd =
else
l
in
if is_statefull cd.cd_name then (
if is_stateful cd.cd_name then (
(** Fields corresponding to normal memory variables. *)
let mem_fields = List.map cvar_of_vd cd.cd_mems in
(** Fields corresponding to object variables. *)
@ -622,9 +622,13 @@ let out_decl_of_class_def cd =
(** [reset_fun_def_of_class_def cd] returns the defintion of the C function
tasked to reset the class [cd]. *)
let reset_fun_def_of_class_def cd =
let var_env = List.map cvar_of_vd cd.cd_mems in
let reset = find_reset_method cd in
let body = cstm_of_act_list var_env cd.cd_objs reset.m_body in
let body =
try
let var_env = List.map cvar_of_vd cd.cd_mems in
let reset = find_reset_method cd in
cstm_of_act_list var_env cd.cd_objs reset.m_body
with Not_found -> [] (* TODO C : nicely deal with stateless objects *)
in
Cfundef {
f_name = (cname_of_qn cd.cd_name) ^ "_reset";
f_retty = Cty_void;
@ -635,6 +639,7 @@ let reset_fun_def_of_class_def cd =
}
}
(** [cdecl_and_cfun_of_class_def cd] translates the class definition [cd] to
a C program. *)
let cdefs_and_cdecls_of_class_def cd =
@ -651,7 +656,7 @@ let cdefs_and_cdecls_of_class_def cd =
let res_fun_decl = cdecl_of_cfundef reset_fun_def in
let step_fun_decl = cdecl_of_cfundef step_fun_def in
let (decls, defs) =
if is_statefull cd.cd_name then
if is_stateful cd.cd_name then
([res_fun_decl; step_fun_decl], [reset_fun_def; step_fun_def])
else
([step_fun_decl], [step_fun_def]) in
@ -748,7 +753,7 @@ let global_file_header name prog =
let dependencies = List.map modul_to_string dependencies in
let (decls, defs) =
List.split (List.map cdefs_and_cdecls_of_class_def prog.p_defs) in
List.split (List.map cdefs_and_cdecls_of_class_def prog.p_classes) in
let decls = List.concat decls
and defs = List.concat defs in

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

@ -88,7 +88,7 @@ let assert_node_res cd =
statements) needed for a main() function calling [cd]. *)
let main_def_of_class_def cd =
let format_for_type ty = match ty with
| Tarray _ | Tprod _ | Tunit -> assert false
| Tarray _ | Tprod _ | Tmutable _ | Tunit -> assert false
| Types.Tid id when id = Initial.pfloat -> "%f"
| Types.Tid id when id = Initial.pint -> "%d"
| Types.Tid id when id = Initial.pbool -> "%d"
@ -98,7 +98,7 @@ let main_def_of_class_def cd =
(** Does reading type [ty] need a buffer? When it is the case,
[need_buf_for_ty] also returns the type's name. *)
let need_buf_for_ty ty = match ty with
| Tarray _ | Tprod _ | Tunit -> assert false
| Tarray _ | Tprod _ | Tmutable _ | Tunit -> assert false
| Types.Tid id when id = Initial.pfloat -> None
| Types.Tid id when id = Initial.pint -> None
| Types.Tid id when id = Initial.pbool -> None
@ -262,7 +262,7 @@ let mk_main name p =
if !Compiler_options.simulation then (
let n_names = !Compiler_options.assert_nodes in
let find_class n =
try List.find (fun cd -> cd.cd_name.name = n) p.p_defs
try List.find (fun cd -> cd.cd_name.name = n) p.p_classes
with Not_found ->
Format.eprintf "Unknown node %s.@." n;
exit 1 in

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

@ -23,6 +23,7 @@ type ty = Tclass of class_name
| Tint
| Tfloat
| Tarray of ty * exp
| Tref of ty
| Tunit
and classe = { c_protection : protection;
@ -81,6 +82,7 @@ and exp = Eval of pattern
| Enew of ty * exp list
| Enew_array of ty * exp list (** [ty] is the array base type *)
| Evoid (*printed as nothing*)
| Ecast of ty * exp
| Svar of const_name
| Sint of int
| Sfloat of float
@ -99,13 +101,14 @@ and pattern = Pfield of pattern * field_name
type program = classe list
let default_value ty = match ty with
let rec default_value ty = match ty with
| Tclass _ -> Snull
| Tgeneric _ -> Snull
| Tbool -> Sbool true
| Tint -> Sint 0
| Tfloat -> Sfloat 0.0
| Tunit -> Evoid
| Tref t -> default_value t
| Tarray _ -> Enew_array (ty,[])

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

@ -42,6 +42,7 @@ let rec _ty size ff t = match t with
| Tclass n -> class_name ff n
| Tgeneric (n, ty_l) -> fprintf ff "%a<@[%a@]>" class_name n (print_list_r ty """,""") ty_l
| Tarray (t,s) -> if size then fprintf ff "%a[%a]" full_ty t exp s else fprintf ff "%a[]" ty t
| Tref t -> ty ff t
| Tunit -> pp_print_string ff "void"
and full_ty ff t = _ty true ff t
@ -78,6 +79,7 @@ and exp ff = function
| [] -> fprintf ff "new %a" full_ty t
| _ -> fprintf ff "new %a@[<2>%a@]" ty t (print_list_r exp "{"",""}") e_l )
| Evoid -> ()
| Ecast (t,e) -> fprintf ff "(%a)(%a)" ty t exp e
| Svar c -> const_name ff c
| Sint i -> pp_print_int ff i
| Sfloat f -> pp_print_float ff f

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

@ -52,6 +52,10 @@ let rec translate_modul m = match m with
let translate_const_name { qual = m; name = n } =
{ qual = QualModule { qual = translate_modul m; name = "CONSTANTES"}; name = String.uppercase n }
(** a [Module.fun] becomes a [module.FUNS.fun] *)
let translate_fun_name { qual = m; name = n } =
{ qual = QualModule { qual = translate_modul m; name = "FUNS"}; name = n }
(** a [Module.name] becomes a [module.Name]
used for type_names, class_names, fun_names *)
let qualname_to_class_name q =
@ -94,7 +98,17 @@ let rec static_exp param_env se = match se.Types.se_desc with
| Types.Sconstructor c -> let c = translate_constructor_name c in Sconstructor c
| Types.Sfield f -> eprintf "ojSfield @."; assert false;
| Types.Stuple se_l -> tuple param_env se_l
| Types.Sarray_power _ -> eprintf "ojSarray_power@."; assert false; (* TODO java array *)
| Types.Sarray_power (see,pow) ->
let pow = (try Static.int_of_static_exp Names.QualEnv.empty pow
with Errors.Error ->
eprintf "%aStatic power of array should have integer power. \
Please use callgraph or non-static exp in %a.@."
Location.print_location se.Types.se_loc
Global_printer.print_static_exp se;
raise Errors.Error)
in
let se_l = Misc.repeat_list (static_exp param_env see) pow in
Enew_array (ty param_env se.Types.se_ty, se_l)
| Types.Sarray se_l -> Enew_array (ty param_env se.Types.se_ty, List.map (static_exp param_env) se_l)
| Types.Srecord _ -> eprintf "ojSrecord@."; assert false; (* TODO java *)
| Types.Sop (f, se_l) -> Efun (qualname_to_class_name f, List.map (static_exp param_env) se_l)
@ -106,11 +120,12 @@ and boxed_ty param_env t = match t with
| Types.Tid t when t = Initial.pfloat -> Tclass (Names.local_qn "Float")
| Types.Tid t -> Tclass (qualname_to_class_name t)
| Types.Tarray (t,size) -> Tarray (boxed_ty param_env t, static_exp param_env size)
| Types.Tmutable t -> Tref (boxed_ty param_env t)
| Types.Tunit -> Tunit
and tuple_ty param_env ty_l =
let ln = ty_l |> List.length |> Pervasives.string_of_int in
Tgeneric (java_pervasive_class ("Tuple"^ln), List.map (boxed_ty param_env) ty_l)
Tclass (java_pervasive_class ("Tuple"^ln))
and ty param_env t :Java.ty = match t with
| Types.Tprod ty_l -> tuple_ty param_env ty_l
@ -119,6 +134,7 @@ and ty param_env t :Java.ty = match t with
| Types.Tid t when t = Initial.pfloat -> Tfloat
| Types.Tid t -> Tclass (qualname_to_class_name t)
| Types.Tarray (t,size) -> Tarray (ty param_env t, static_exp param_env size)
| Types.Tmutable t -> Tref (ty param_env t)
| Types.Tunit -> Tunit
and var_dec param_env vd = { vd_type = ty param_env vd.v_type; vd_ident = vd.v_ident }
@ -166,7 +182,15 @@ let rec act_list param_env act_l acts =
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 =
Aassgn (pattern param_env p, Eval (Pfield (Pvar return_id, "c"^(string_of_int i))))
let t = ty param_env p.pat_ty in
let cast t e = match t with
| Tbool -> Ecast(Tbool, Ecast(boxed_ty param_env p.pat_ty, e))
| Tint -> Ecast(Tint, Ecast(boxed_ty param_env p.pat_ty, e))
| Tfloat -> Ecast(Tfloat, Ecast(boxed_ty param_env p.pat_ty, e))
| _ -> Ecast(t, e)
in
let p = pattern param_env p in
Aassgn (p, cast t (Eval (Pfield (Pvar return_id, "c"^(string_of_int i)))))
in
let copies = Misc.mapi copy_return_to_var p_l in
assgn::(copies@acts)
@ -231,8 +255,6 @@ let copy_to_this vd_l =
List.map _vd vd_l
let class_def_list classes cd_l =
let class_def classes cd =
Idents.enter_node cd.cd_name;
@ -249,23 +271,24 @@ let class_def_list classes cd_l =
[reset_mems] is the block to reset the members of the class
without call to the reset method of inner instances, it retains [this.x = 0] but not [this.I.reset()] *)
let reset, reset_mems =
let oreset = find_reset_method cd in
let body = block param_env oreset.Obc.m_body in
let reset_mems = block param_env (remove_resets oreset.Obc.m_body) in
mk_methode body "reset", reset_mems
try (* When there exist a reset method *)
let oreset = find_reset_method cd in
let body = block param_env oreset.Obc.m_body in
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 []
in
(* [obj_env] gives the type of an [obj_ident], needed in async because we change the classe for async obj *)
let constructeur, obj_env =
let obj_env = (* In async we change the type of the async objects *)
let obj_env = (* Mapping between Obc class and Java class, useful at least with asyncs *)
let aux obj_env od =
let t = Tclass (qualname_to_class_name od.o_class)
in Idents.Env.add od.o_ident t obj_env
in List.fold_left aux Idents.Env.empty cd.cd_objs
in
let body =
(* TODO java array : also initialize arrays with [ new int[3] ] *)
(* Initialize the objects *)
(* Function to initialize the objects *)
let obj_init_act acts od =
let params = List.map (static_exp param_env) od.o_params in
match od.o_size with
@ -280,13 +303,23 @@ let class_def_list classes cd_l =
:: (fresh_for size assgn_elem)
:: acts
in
(* function to allocate the arrays *)
let allocate acts vd = match vd.v_type with
| Types.Tarray (t, size) ->
let t = ty param_env vd.v_type in
( 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
(* init member objects *)
let acts = List.fold_left obj_init_act acts cd.cd_objs in
(* allocate member arrays *)
let acts = List.fold_left allocate acts cd.cd_mems in
(* init static params *)
let acts = (copy_to_this vds_params)@acts in
{ b_locals = []; b_body = acts }
{ b_locals = []; b_body = List.rev acts }
in mk_methode ~args:vds_params body (shortname class_name), obj_env
in
let fields =
@ -367,7 +400,7 @@ let const_dec_list cd_l = match cd_l with
let program p =
let classes = const_dec_list p.p_consts in
let classes = type_dec_list classes p.p_types in
let p = class_def_list classes p.p_defs in
let p = class_def_list classes p.p_classes in
get_classes()@p

5
compiler/obc/obc.ml
View file

@ -108,16 +108,19 @@ type method_def =
type class_def =
{ cd_name : class_name;
cd_stateful : bool; (** when false, the class is a function with static parameters
calling other functions with parameters *)
cd_mems : var_dec list;
cd_objs : obj_dec list;
cd_params : param list;
cd_methods: method_def list;
cd_loc : location }
type program =
{ p_modname : modul;
p_opened : modul list;
p_types : type_dec list;
p_consts : const_dec list;
p_defs : class_def list }
p_classes : class_def list; }

8
compiler/obc/obc_mapfold.ml
View file

@ -147,7 +147,9 @@ and method_def funs acc md =
, acc
and class_def_it funs acc cd = funs.class_def funs acc cd
and class_def_it funs acc cd =
Idents.enter_node cd.cd_name;
funs.class_def funs acc cd
and class_def funs acc cd =
let cd_mems, acc = var_decs_it funs acc cd.cd_mems in
let cd_objs, acc = obj_decs_it funs acc cd.cd_objs in
@ -186,8 +188,8 @@ and program_it funs acc p = funs.program funs acc p
and program funs acc p =
let td_list, acc = mapfold (type_dec_it funs) acc p.p_types in
let cd_list, acc = mapfold (const_dec_it funs) acc p.p_consts in
let nd_list, acc = mapfold (class_def_it funs) acc p.p_defs in
{ p with p_types = td_list; p_consts = cd_list; p_defs = nd_list }, acc
let nd_list, acc = mapfold (class_def_it funs) acc p.p_classes in
{ p with p_types = td_list; p_consts = cd_list; p_classes = nd_list }, acc
let defaults = {

5
compiler/obc/obc_printer.ml
View file

@ -152,6 +152,7 @@ let print_class_def ff
print_list_r print_method "" "\n" "" ff m_list;
fprintf ff "@]"
let print_type_def ff { t_name = name; t_desc = tdesc } =
match tdesc with
| Type_abs -> fprintf ff "@[type %a@\n@]" print_qualname name
@ -179,12 +180,12 @@ let print_const_dec ff c =
print_static_exp c.c_value
let print_prog ff { p_opened = modules; p_types = types;
p_consts = consts; p_defs = defs } =
p_consts = consts; p_classes = classes; } =
List.iter (print_open_module ff) modules;
List.iter (print_type_def ff) types;
List.iter (print_const_dec ff) consts;
fprintf ff "@\n";
List.iter (fun def -> (print_class_def ff def; fprintf ff "@\n@\n")) defs
List.iter (fun cdef -> (print_class_def ff cdef; fprintf ff "@\n@\n")) classes
let print oc p =
let ff = formatter_of_out_channel oc in

61
compiler/obc/transformations/scalarize.ml Normal file
View file

@ -0,0 +1,61 @@
(**************************************************************************)
(* *)
(* Heptagon *)
(* *)
(* Author : Marc Pouzet *)
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
(* *)
(**************************************************************************)
(** Remove implicit array's deep copy. If ever some p = e with p of type array still exist,
they are only used as reference to the array, no copy is implied :
array assignation after [scalarize] is pointer wise assignation *)
open Misc
open Obc
open Obc_utils
open Obc_mapfold
(** fresh Afor from 0 to [size] with [body] a function from [var_ident] (the iterator) to [act] list *)
let fresh_for size body =
let i = Idents.gen_var "scalarize" "i" in
let id = mk_var_dec i Initial.tint in
let ei = mk_evar_int i in
Afor (id, Initial.mk_static_int 0, size, mk_block (body ei))
let act funs () a = match a with
| Aassgn (p,e) ->
(match e.e_ty with
| Types.Tarray (t, size) ->
(* a reference (alias) to the array, since we could have a full expression *)
let array_ref = Idents.gen_var "scalarize" "a_ref" in
let vd_array_ref = mk_var_dec array_ref (Types.Tmutable p.pat_ty) in
(* reference initialization *)
let pat_array_ref = mk_pattern ~loc:e.e_loc p.pat_ty (Lvar array_ref) in
let init_array_ref = Aassgn (pat_array_ref, e) in
(* the copy loop *)
let array_ref_i i = mk_pattern_exp t (Larray (pat_array_ref, i)) in
let p_i i = mk_pattern t (Larray (p, i)) in
let copy_i i =
(* recursive call to deal with multidimensional arrays (go deeper) *)
let a = Aassgn (p_i i, array_ref_i i) in
let a, _ = act_it funs () a in
[a]
in
let copy_array = fresh_for size copy_i in
(* resulting block *)
let block = mk_block ~locals:[vd_array_ref] [init_array_ref; copy_array] in
Ablock block, ()
| _ -> raise Errors.Fallback
)
| _ -> raise Errors.Fallback
let program p =
let p, _ = program_it { defaults with act = act } () p in
p

14
heptc
View file

@ -9,17 +9,25 @@ SCRIPT_DIR=$RUN_DIR/`dirname $0`
COMPILER_DIR=$SCRIPT_DIR/compiler
COMPILER=heptc.byte
COMPILER_DEBUG=heptc.d.byte
LIB_DIR=$SCRIPT_DIR/lib
#the symlink
HEPTC=$COMPILER_DIR/$COMPILER
HEPTC_DEBUG=$COMPILER_DIR/$COMPILER_DEBUG
#compile the compiler
if [ ! -x $HEPTC ]
then
cd $COMPILER_DIR
ocamlbuild -j 0 $COMPILER
cd -
if [ -x $HEPTC_DEBUG ]
then
#use the debug
HEPTC=$HEPTC_DEBUG
else
cd $COMPILER_DIR
ocamlbuild -j 0 $COMPILER
cd -
fi
fi
#compile the stdlib

89
lib/java/jeptagon/Pervasives.java
View file

@ -25,48 +25,39 @@ public class Pervasives {
public V get(long timeout, TimeUnit unit) { return v; }
}
public static class Tuple1<T> {
public final T c0;
public Tuple1(T v) {
public static class Tuple1 {
public final Object c0;
public Tuple1(Object v) {
c0 = v;
}
}
public static class Tuple22 {
public static class Tuple2 {
public final Object c0;
public final Object c1;
public Tuple22(Object v0, Object v1) {
public Tuple2(Object v0, Object v1) {
c0 = v0;
c1 = v1;
}
}
public static class Tuple2 <T0,T1> {
public final T0 c0;
public final T1 c1;
public Tuple2(T0 v0, T1 v1) {
c0 = v0;
c1 = v1;
}
}
public static class Tuple3 <T0,T1,T2> {
public final T0 c0;
public final T1 c1;
public final T2 c2;
public Tuple3(T0 v0, T1 v1, T2 v2) {
public static class Tuple3 {
public final Object c0;
public final Object c1;
public final Object c2;
public Tuple3(Object v0, Object v1, Object v2) {
c0 = v0;
c1 = v1;
c2 = v2;
}
}
public static class Tuple4 <T0,T1,T2,T3> {
public final T0 c0;
public final T1 c1;
public final T2 c2;
public final T3 c3;
public Tuple4(T0 v0, T1 v1, T2 v2, T3 v3) {
public static class Tuple4 {
public final Object c0;
public final Object c1;
public final Object c2;
public final Object c3;
public Tuple4(Object v0, Object v1, Object v2, Object v3) {
c0 = v0;
c1 = v1;
c2 = v2;
@ -74,13 +65,13 @@ public class Pervasives {
}
}
public static class Tuple5 <T0,T1,T2,T3,T4> {
public final T0 c0;
public final T1 c1;
public final T2 c2;
public final T3 c3;
public final T4 c4;
public Tuple5(T0 v0, T1 v1, T2 v2, T3 v3, T4 v4) {
public static class Tuple5 {
public final Object c0;
public final Object c1;
public final Object c2;
public final Object c3;
public final Object c4;
public Tuple5(Object v0, Object v1, Object v2, Object v3, Object v4) {
c0 = v0;
c1 = v1;
c2 = v2;
@ -89,14 +80,14 @@ public class Pervasives {
}
}
public static class Tuple6 <T0,T1,T2,T3,T4,T5> {
public final T0 c0;
public final T1 c1;
public final T2 c2;
public final T3 c3;
public final T4 c4;
public final T5 c5;
public Tuple6(T0 v0, T1 v1, T2 v2, T3 v3, T4 v4, T5 v5) {
public static class Tuple6 {
public final Object c0;
public final Object c1;
public final Object c2;
public final Object c3;
public final Object c4;
public final Object c5;
public Tuple6(Object v0, Object v1, Object v2, Object v3, Object v4, Object v5) {
c0 = v0;
c1 = v1;
c2 = v2;
@ -106,15 +97,15 @@ public class Pervasives {
}
}
public static class Tuple7 <T0,T1,T2,T3,T4,T5,T6> {
public final T0 c0;
public final T1 c1;
public final T2 c2;
public final T3 c3;
public final T4 c4;
public final T5 c5;
public final T6 c6;
public Tuple7(T0 v0, T1 v1, T2 v2, T3 v3, T4 v4, T5 v5, T6 v6) {
public static class Tuple7 {
public final Object c0;
public final Object c1;
public final Object c2;
public final Object c3;
public final Object c4;
public final Object c5;
public final Object c6;
public Tuple7(Object v0, Object v1, Object v2, Object v3, Object v4, Object v5, Object v6) {
c0 = v0;
c1 = v1;
c2 = v2;

2
test/async/pipline.ept
View file

@ -12,7 +12,7 @@ tel
fun mean<<n: int>> (i: int^n) returns (m: int)
let
m = fold sum <<n>> (i,0)
m = (fold (+) <<n>> (i,0)) /n
tel

7
test/async/scalarize.ept Normal file
View file

@ -0,0 +1,7 @@
node f() returns ()
var t1,t2 : int^4;
let
t1 = [3, 5, 6, 7];
t2 = map (+) <<4>> (4^4,t1);
tel

5
test/good/array_fill.ept
View file

@ -1,9 +1,10 @@
const n : int = 33
node stopbb(shiftenable : bool) returns (dataout : bool^n)
var last dataint : bool^n = false^n;
var last dataint : bool^n; f : bool;
let
dataout = (false^n) fby dataint;
f = false;
dataout = (f^n) fby dataint;
switch shiftenable
| true do dataint = [true] @ dataout[0 .. n - 2];
| false do

2
todo.txt
View file

@ -3,7 +3,7 @@ Plus ou moins ordonné du plus urgent au moins urgent.
*- Bugs related to matching types without unaliasing it. In lots of parts. Use Modules.unalias_type.
*- Functions in Obc should not be objetcs.
*- Les types des patterns dans les boucles crées par concatenate ( entre autres ) sont faux.
*- Collision entre les noms de params et les idents dans les noeuds.

46
tools/debugger_script
View file

@ -1,29 +1,31 @@
load_printer "_build/global/names.d.cmo"
load_printer "_build/global/location.d.cmo"
load_printer "/sw/lib/ocaml/menhirLib/menhirLib.cmo"
load_printer "/sw/lib/ocaml/str.cma"
load_printer "_build/menhirLib.cmo"
load_printer "_build/utilities/misc.d.cmo"
load_printer "_build/global/types.d.cmo"
load_printer "_build/global/signature.d.cmo"
load_printer "_build/global/names.d.cmo"
load_printer "_build/utilities/global/compiler_options.d.cmo"
load_printer "_build/global/idents.d.cmo"
load_printer "_build/global/location.d.cmo"
load_printer "_build/global/types.d.cmo"
load_printer "_build/global/clocks.d.cmo"
load_printer "_build/global/signature.d.cmo"
load_printer "_build/utilities/global/errors.d.cmo"
load_printer "_build/utilities/global/compiler_utils.d.cmo"
load_printer "_build/global/modules.d.cmo"
load_printer "_build/global/initial.d.cmo"
load_printer "_build/global/idents.d.cmo"
load_printer "_build/global/clocks.d.cmo"
load_printer "_build/utilities/pp_tools.d.cmo"
load_printer "_build/global/global_printer.d.cmo"
load_printer "_build/global/initial.d.cmo"
load_printer "_build/global/static.d.cmo"
load_printer "_build/heptagon/heptagon.d.cmo"
load_printer "_build/utilities/graph.d.cmo"
load_printer "_build/heptagon/analysis/causal.d.cmo"
load_printer "_build/heptagon/analysis/causality.d.cmo"
load_printer "_build/heptagon/analysis/initialization.d.cmo"
load_printer "_build/global/global_mapfold.d.cmo"
load_printer "_build/heptagon/hept_mapfold.d.cmo"
load_printer "_build/heptagon/analysis/statefull.d.cmo"
load_printer "_build/heptagon/analysis/typing.d.cmo"
load_printer "_build/heptagon/hept_printer.d.cmo"
load_printer "_build/heptagon/parsing/hept_parsetree.d.cmo"
load_printer "_build/heptagon/parsing/hept_parser.d.cmo"
load_printer "_build/heptagon/parsing/hept_lexer.d.cmo"
load_printer "_build/heptagon/parsing/hept_scoping.d.cmo"
load_printer "_build/heptagon/transformations/automata.d.cmo"
load_printer "_build/heptagon/transformations/block.d.cmo"
load_printer "_build/heptagon/transformations/completion.d.cmo"
@ -31,28 +33,34 @@ load_printer "_build/heptagon/transformations/reset.d.cmo"
load_printer "_build/heptagon/transformations/every.d.cmo"
load_printer "_build/heptagon/transformations/last.d.cmo"
load_printer "_build/heptagon/transformations/present.d.cmo"
load_printer "_build/heptagon/transformations/switch.d.cmo"
load_printer "_build/heptagon/main/hept_compiler.d.cmo"
load_printer "_build/heptagon/parsing/hept_parsetree.d.cmo"
load_printer "_build/heptagon/parsing/hept_parser.d.cmo"
load_printer "_build/heptagon/parsing/hept_lexer.d.cmo"
load_printer "_build/heptagon/parsing/hept_scoping.d.cmo"
load_printer "_build/heptagon/parsing/hept_parsetree_mapfold.d.cmo"
load_printer "_build/heptagon/parsing/hept_static_scoping.d.cmo"
load_printer "_build/heptagon/main/hept_parser_scoper.d.cmo"
load_printer "_build/minils/minils.d.cmo"
load_printer "_build/minils/mls_mapfold.d.cmo"
load_printer "_build/minils/mls_printer.d.cmo"
load_printer "_build/utilities/graph.d.cmo"
load_printer "_build/utilities/global/dep.d.cmo"
load_printer "_build/minils/mls_utils.d.cmo"
load_printer "_build/main/hept2mls.d.cmo"
load_printer "_build/minils/transformations/itfusion.d.cmo"
load_printer "_build/obc/obc.d.cmo"
load_printer "_build/obc/control.d.cmo"
load_printer "_build/obc/obc_mapfold.d.cmo"
load_printer "_build/obc/obc_utils.d.cmo"
load_printer "_build/obc/control.d.cmo"
load_printer "_build/main/mls2obc.d.cmo"
load_printer "_build/minils/transformations/callgraph.d.cmo"
load_printer "_build/obc/c/c.d.cmo"
load_printer "_build/obc/c/csubst.d.cmo"
load_printer "_build/obc/obc_utils.d.cmo"
load_printer "_build/obc/c/cgen.d.cmo"
load_printer "_build/obc/c/cmain.d.cmo"
load_printer "_build/obc/java/java.d.cmo"
load_printer "_build/obc/java/java_printer.d.cmo"
load_printer "_build/obc/java/obc2java.d.cmo"
load_printer "_build/obc/java/java_main.d.cmo"
load_printer "_build/obc/obc_printer.d.cmo"
load_printer "_build/obc/transformations/scalarize.d.cmo"
load_printer "_build/minils/main/mls2seq.d.cmo"
load_printer "_build/minils/analysis/clocking.d.cmo"
load_printer "_build/minils/transformations/normalize.d.cmo"
@ -64,5 +72,5 @@ load_printer "_build/minils/transformations/introvars.d.cmo"
load_printer "_build/minils/transformations/singletonvars.d.cmo"
load_printer "_build/minils/transformations/tomato.d.cmo"
load_printer "_build/minils/main/mls_compiler.d.cmo"
load_printer "_build/main/heptc.d.cmo"
load_printer "_build/main/heptc.d.cmo