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

Compare commits

base: jeltz:async
Branches Tags
jeltz:master
jeltz:async
..
compare: jeltz:master
Branches Tags
jeltz:async
jeltz:master

No commits in common. "async" and "master" have entirely different histories.
async ... master

36 changed files with 165 additions and 902 deletions
Show stats Expand all files Collapse all files

2
.gitignore vendored
View file

@ -37,5 +37,3 @@ config.status
*.bbl
auto
autom4te.cache
!/lib/c/*.h
!/lib/c/*.c

4
compiler/global/names.ml
View file

@ -32,7 +32,6 @@
type name = string
type module_name = name
type ack_name = name
type modul =
| Pervasives
@ -100,9 +99,6 @@ let qualname_of_string s =
| [] -> (* Misc.internal_error "Names" *)raise Exit
| n::q_l -> { qual = modul_of_string_list q_l; name = n }
let qn_append q suffix =
{ qual = q.qual; name = q.name ^ suffix }
let modul_of_string s =
let q_l = Misc.split_string s "." in
modul_of_string_list (List.rev q_l)

57
compiler/heptagon/analysis/async_check.ml
View file

@ -1,57 +0,0 @@
open Names
open Location
open Heptagon
open Hept_mapfold
type error =
| Etoo_much_async
let message loc kind =
begin match kind with
| Etoo_much_async ->
Format.eprintf "%aInvalid async nesting.@."
print_location loc
end;
raise Errors.Error
(* Compute the set of nodes that use at least one async call. *)
let exp_callers funs (callers, current) e =
let e, (callers, current) = Hept_mapfold.exp funs (callers, current) e in
match e.e_desc with
| Eapp({ a_op = Easync _ }, _, _) ->
e, (QualSet.add (Option.get current) callers, current)
(* TODO(Arduino): Eiterator *)
| _ -> e, (callers, current)
let node_dec_callers funs (callers, _) n =
Hept_mapfold.node_dec funs (callers, Some n.n_name) n
let funs_callers =
{ Hept_mapfold.defaults with
node_dec = node_dec_callers;
exp = exp_callers }
(* Ensure that no node using an async call is called more than once. *)
let exp_async funs (callers, calls) e =
let e, (callers, calls) = Hept_mapfold.exp funs (callers, calls) e in
match e.e_desc with
| Eapp({ a_op = Easync (name, _) }, _, _) ->
let caller = QualSet.mem name callers in
let exists = QualSet.mem name calls in
if caller && exists then
message e.e_loc Etoo_much_async
else
e, (callers, QualSet.add name calls)
(* TODO(Arduino): Eiterator *)
| _ -> e, (callers, calls)
let funs_async =
{ Hept_mapfold.defaults with
exp = exp_async }
let program p =
let _, (callers, _) =
Hept_mapfold.program_it funs_callers (QualSet.empty, None) p
in
let _ = Hept_mapfold.program_it funs_async (callers, QualSet.empty) p in
p

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

@ -167,7 +167,7 @@ and apply op e_list =
let i2 = typing e2 in
let i3 = typing e3 in
ctuplelist [t1; i2; i3]
| ( Efun _ | Easync _ | Enode _ | Econcat | Eselect_slice
| ( Efun _| Enode _ | Econcat | Eselect_slice
| Eselect_dyn | Eselect_trunc | Eselect | Earray_fill | Ereinit) ->
ctuplelist (List.map typing e_list)
| (Earray | Etuple) ->

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

@ -198,8 +198,7 @@ and typing_app h base pat op e_list = match op with
| Efun { qual = Module "Iostream"; name = "fprintf" } ->
List.iter (expect h pat (Ck base)) e_list;
Cprod []
(* FIXME(Arduino): voir si c'est correct *)
| (Efun f | Enode f | Easync (f, _)) ->
| (Efun f | Enode f) ->
let node = Modules.find_value f in
let pat_id_list = ident_list_of_pat pat in
let rec build_env a_l v_l env = match a_l, v_l with

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

@ -287,7 +287,6 @@ and apply h app e_list =
let ty1 = typing h e1 in
let _ = typing h e2 in
itype ty1
(* FIXME(Arduino): voir si ajout nécessaire *)
| Enode _ ->
begin
(* for nodes, force all inputs to be initialized *)

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

@ -525,8 +525,7 @@ and collect_app env op e_list = match op with
| Efun { qual = Module "Iostream"; name = "fprintf" | "printf" } ->
VarsCollection.prod []
(* FIXME(Arduino): voir si c'est correct *)
| Efun f | Enode f | Easync (f, _) ->
| Efun f | Enode f ->
let ty_desc = Modules.find_value f in
let inputs_lins = linearities_of_arg_list ty_desc.node_inputs in
let outputs_lins = linearities_of_arg_list ty_desc.node_outputs in
@ -591,7 +590,7 @@ and typing_app env op e_list = match op with
let e = assert_1 e_list in
let env = safe_expect env Ltop e in
Ltop, env
| Eifthenelse | Efun _ | Enode _ | Easync _ | Etuple
| Eifthenelse | Efun _ | Enode _ | Etuple
| Eupdate | Efield_update | Ereinit -> assert false (*already done in expect_app*)
(** Check that the application of op to e_list can have the linearity
@ -601,8 +600,7 @@ and expect_app env expected_lin op e_list = match op with
let env = List.fold_left (fun env -> safe_expect env Ltop) env e_list in
Ltuple [], env
(* FIXME(Arduino): voir si c'est correct *)
| Efun f | Enode f | Easync (f, _) ->
| Efun f | Enode f ->
let ty_desc = Modules.find_value f in
let inputs_lins = linearities_of_arg_list ty_desc.node_inputs in
let outputs_lins = linearities_of_arg_list ty_desc.node_outputs in

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

@ -266,17 +266,13 @@ let flatten_ty_list l =
List.fold_right
(fun arg args -> match arg with Tprod l -> l@args | a -> a::args ) l []
let kind f ty_desc ack =
let kind f ty_desc =
let ty_of_arg v =
if Linearity.is_linear v.a_linearity && not !Compiler_options.do_linear_typing then
error Eenable_memalloc;
v.a_type
in
let op = match ack with
| Some ack -> Easync (f, ack)
| _ when ty_desc.node_stateful -> Enode f
| _ -> 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
@ -637,8 +633,7 @@ let rec typing cenv h e =
a_params = params } as app),
n_list, pe_list, e_list, reset) ->
let ty_desc = find_value f in
(* TODO(Arduino): iterator + async *)
let op, expected_ty_list, result_ty_list = kind f ty_desc None in
let op, expected_ty_list, result_ty_list = kind f ty_desc in
let node_params =
List.map (fun { p_name = n } -> local_qn n) ty_desc.node_params in
let m = build_subst node_params params in
@ -774,14 +769,9 @@ and typing_app cenv h app e_list =
let typed_format_args = typing_format_args cenv h typed_e1 format_args in
Tprod [], app, typed_e1::typed_e2::typed_format_args
(* FIXME(Arduino): voir si c'est correct *)
| (Efun f | Enode f | Easync (f, _)) ->
| (Efun f | Enode f) ->
let ty_desc = find_value f in
let ack = match app.a_op with
| Easync (_, ack) -> Some ack
| _ -> None
in
let op, expected_ty_list, result_ty_list = kind f ty_desc ack in
let op, expected_ty_list, result_ty_list = kind f ty_desc in
let node_params = List.map (fun { p_name = n } -> local_qn n) ty_desc.node_params in
let m = build_subst node_params app.a_params in
let expected_ty_list = List.map (simplify_type m) expected_ty_list in

11
compiler/heptagon/hept_printer.ml
View file

@ -100,9 +100,6 @@ and print_node_params ff l =
and print_exp_tuple ff l =
fprintf ff "@[<2>(%a)@]" (print_list_r print_exp """,""") l
and print_static_exp_tuple ff l =
fprintf ff "@[<2>(%a)@]" (print_list_r print_static_exp """,""") l
and print_vd_tuple ff l =
match l with
| [] -> fprintf ff "()"
@ -206,14 +203,6 @@ and print_app ff (app, args) =
print_stateful ff true;
fprintf ff "@[%a@,%a@,%a@]"
print_qualname f print_params app.a_params print_exp_tuple args
| Easync (f, ack) ->
print_stateful ff true;
fprintf ff "@[async %a@,%a@,%a on %s@,%a@]"
print_qualname f
print_params app.a_params
print_exp_tuple args
ack.ack_name
print_static_exp_tuple ack.ack_params
| Eifthenelse ->
let e1, e2, e3 = assert_3 args in
fprintf ff "@[<hv>if %a@ then %a@ else %a@]"

3
compiler/heptagon/heptagon.ml
View file

@ -79,7 +79,6 @@ and op =
| Etuple
| Efun of fun_name
| Enode of fun_name
| Easync of fun_name * ack
| Eifthenelse
| Earrow
| Efield
@ -94,8 +93,6 @@ and op =
| Econcat
| Ereinit
and ack = { ack_name : ack_name; ack_params : static_exp list }
and pat =
| Etuplepat of pat list
| Evarpat of var_ident

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

@ -37,7 +37,6 @@ let compile_program p log_c =
(* Typing *)
let p = silent_pass "Statefulness check" true Stateful.program p in
let p = silent_pass "Unsafe check" true Unsafe.program p in
let p = silent_pass "Async check" true Async_check.program p in
let p = pass "Typing" true Typing.program p pp in
let p = pass "Linear Typing" !do_linear_typing Linear_typing.program p pp in

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

@ -42,7 +42,6 @@ let keyword_table = ((Hashtbl.create 149) : (string, token) Hashtbl.t);;
List.iter (fun (str,tok) -> Hashtbl.add keyword_table str tok) [
"node", NODE;
"async", ASYNC;
"fun", FUN;
"returns", RETURNS;
"var", VAR;

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

@ -68,7 +68,6 @@ open Hept_parsetree
%token ENFORCE
%token REACHABLE
%token ATTRACTIVE
%token ASYNC
%token WITH
%token WHEN WHENOT MERGE ON ONOT
%token INLINED
@ -526,14 +525,6 @@ node_name:
| q=qualname c=call_params { mk_app (Enode q) c false }
| INLINED q=qualname c=call_params { mk_app (Enode q) c true }
async_clock_args:
| const opt_comma {[$1]}
| const COMMA async_clock_args {$1 :: $3}
async_clock:
| n=IDENT LPAREN args=async_clock_args RPAREN
{ mk_ack n args }
merge_handlers:
| hs=nonempty_list(merge_handler) { hs }
| e1=simple_exp e2=simple_exp { [(Q Initial.ptrue, e1);(Q Initial.pfalse, e2)] }
@ -551,9 +542,6 @@ _exp:
/* node call*/
| n=node_name LPAREN args=exps RPAREN
{ Eapp(n, args) }
/* async node call */
| ASYNC q=qualname c=call_params LPAREN args=exps RPAREN ON ack=async_clock
{ Eapp(mk_app (Easync (q, ack)) c false, args) }
| SPLIT n=ident LPAREN e=exp RPAREN
{ Esplit(n, e) }
| REINIT LPAREN e1=exp COMMA e2=exp RPAREN

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

@ -41,7 +41,6 @@ type module_name = Names.modul
(** state_names, [automata] translate them in constructors with a fresh type. *)
type state_name = Names.name
type ack_name = Names.ack_name
type qualname =
| Q of Names.qualname (* already qualified name *)
@ -114,7 +113,6 @@ and app = { a_op: op; a_params: exp list; a_inlined: bool }
and op =
| Etuple
| Enode of qualname
| Easync of qualname * ack
| Efun of qualname
| Eifthenelse
| Earrow
@ -130,8 +128,6 @@ and op =
| Econcat
| Ereinit
and ack = { ack_name : ack_name; ack_params : static_exp list }
and pat =
| Etuplepat of pat list
| Evarpat of var_name
@ -275,9 +271,6 @@ let mk_exp desc ?(ct_annot = None) loc =
let mk_app op params inlined =
{ a_op = op; a_params = params; a_inlined = inlined }
let mk_ack name params =
{ ack_name = name; ack_params = params }
let mk_call ?(params=[]) ?(inlined=false) op exps =
Eapp (mk_app op params inlined, exps)

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

@ -350,11 +350,6 @@ and translate_desc loc env = function
let e1 = translate_exp env e1 in
Heptagon.Esplit(x, e1)
and translate_ack { ack_name = name; ack_params = params } =
let tr_params = List.map translate_static_exp params in
{ Heptagon.ack_name = name;
Heptagon.ack_params = tr_params }
and translate_op = function
| Earrow -> Heptagon.Earrow
| Eifthenelse -> Heptagon.Eifthenelse
@ -371,8 +366,6 @@ and translate_op = function
| Eselect_trunc -> Heptagon.Eselect_trunc
| Efun ln -> Heptagon.Efun (qualify_value ln)
| Enode ln -> Heptagon.Enode (qualify_value ln)
| Easync (ln, ack) ->
Heptagon.Easync (qualify_value ln, translate_ack ack)
| Ereinit -> Heptagon.Ereinit
and translate_pat loc env = function

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

@ -68,7 +68,6 @@ let qualify_pervasive q =
op<a1,a2> (a3) == op <a1> (a2,a3) == op (a1,a2,a3) *)
let static_app_from_app app args =
match app.a_op with
(* TODO(Arduino): static? *)
| Efun q
| Enode q ->
let q = qualify_pervasive q in

4
compiler/main/hept2mls.ml
View file

@ -81,14 +81,10 @@ let translate_iterator_type = function
| Heptagon.Ifoldi -> Ifoldi
| Heptagon.Imapfold -> Imapfold
let translate_ack { Heptagon.ack_name = name; Heptagon.ack_params = params } =
{ ack_name = name; ack_params = params }
let translate_op = function
| Heptagon.Eifthenelse -> Eifthenelse
| Heptagon.Efun f -> Efun f
| Heptagon.Enode f -> Enode f
| Heptagon.Easync (f, ack) -> Easync (f, translate_ack ack)
| Heptagon.Efield -> assert false
| Heptagon.Efield_update -> Efield_update
| Heptagon.Earray_fill -> Earray_fill

21
compiler/main/mls2obc.ml
View file

@ -280,8 +280,7 @@ let rec translate map e =
e.e_desc
(* Already treated cases when translating the [eq] *)
| Minils.Eiterator _ | Minils.Emerge _ | Minils.Efby _
| Minils.Eapp ({Minils.a_op=(Minils.Enode _|Minils.Efun _|Minils.Easync _
|Minils.Econcat
| Minils.Eapp ({Minils.a_op=(Minils.Enode _|Minils.Efun _|Minils.Econcat
|Minils.Eupdate|Minils.Eselect_dyn
|Minils.Eselect_trunc|Minils.Eselect_slice
|Minils.Earray_fill|Minils.Efield_update
@ -489,16 +488,12 @@ let rec translate_eq map call_context
let action = Aop (q, List.map (translate_extvalue_to_exp map) args) in
v, si, j, (control map ck action) :: s
| pat, Minils.Eapp
({ Minils.a_op =
Minils.Efun _ | Minils.Enode _ | Minils.Easync _ } as app,
e_list, r) ->
| pat, Minils.Eapp ({ Minils.a_op = Minils.Efun _ | Minils.Enode _ } as app, e_list, r) ->
let name_list = translate_pat map e.Minils.e_ty pat in
let c_list = List.map (translate_extvalue_to_exp map) e_list in
let v', si', j', action = mk_node_call map call_context
app loc name_list c_list e.Minils.e_ty in
let action = List.map (control map ck) action in
(* TODO(Arduino): add Easync? *)
let s = (match r, app.Minils.a_op with
| Some r, Minils.Enode _ ->
let ck = Clocks.Con (ck, Initial.ptrue, r) in
@ -537,9 +532,6 @@ and translate_eq_list map call_context act_list =
let rev_act = List.rev act_list in
List.fold_left (translate_eq map call_context) ([], [], [], []) rev_act
and translate_ack { Minils.ack_name = name; Minils.ack_params = params } =
{ ack_name = name; ack_params = params }
and mk_node_call map call_context app loc (name_list : Obc.pattern list) args ty =
match app.Minils.a_op with
| Minils.Efun f when Mls_utils.is_op f ->
@ -579,26 +571,19 @@ and mk_node_call map call_context app loc (name_list : Obc.pattern list) args ty
let env = List.fold_left2 build Env.empty nd.Minils.n_input args in
v @ nd.Minils.n_local, si, j, subst_act_list env s
| Minils.Enode f | Minils.Efun f | Minils.Easync (f, _) ->
| Minils.Enode f | Minils.Efun f ->
let id = match app.Minils.a_id with
| None -> gen_obj_ident f
| Some id -> id
in
let o = mk_obj_call_from_context call_context id in
let ack = match app.Minils.a_op with
| Minils.Easync (_, ack) -> Some (translate_ack ack)
| _ -> None
in
let obj =
{ o_ident = obj_ref_name o; o_class = f;
o_params = app.Minils.a_params;
o_ack = ack;
o_size = size_from_call_context call_context; o_loc = loc } in
let si = match app.Minils.a_op with
| Minils.Efun _ -> []
| Minils.Enode _ -> [reinit o]
(* TODO(Arduino): is it correct? *)
| Minils.Easync _ -> []
| _ -> assert false
in
let s = [Acall (name_list, o, Mstep, args)] in

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

@ -129,8 +129,7 @@ let typing_app h base pat op w_list = match op with
| Efun { qual = Module "Iostream"; name = "fprintf" } ->
List.iter (expect_extvalue h base) w_list;
Cprod []
(* FIXME(Arduino): voir si c'est correct *)
| (Efun f | Enode f | Easync (f, _)) ->
| ( Efun f | Enode f) ->
let node = Modules.find_value f in
let pat_id_list = Mls_utils.ident_list_of_pat pat in
let rec build_env a_l v_l env = match a_l, v_l with

3
compiler/minils/minils.ml
View file

@ -108,7 +108,6 @@ 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] *)
| Easync of fun_name * ack
| Eifthenelse (** [if arg1 then arg2 else arg3] *)
| Efield_update (** [{ arg1 with a_param1 = arg2 }] *)
| Earray (** [[ args ]] *)
@ -120,8 +119,6 @@ and op =
| Eupdate (** [[ arg1 with arg3..arg_n = arg2 ]] *)
| Econcat (** [arg1\@\@arg2] *)
and ack = { ack_name : ack_name; ack_params : static_exp list }
type pat =
| Etuplepat of pat list
| Evarpat of var_ident

2
compiler/minils/mls_compare.ml
View file

@ -149,7 +149,7 @@ struct
let cr = match app1.a_op, app2.a_op with
| Efun ln1, Efun ln2 -> compare ln1 ln2
| x, y when x = y -> 0 (* all constructors can be compared with P.compare *)
| (Eequal | Efun _ | Enode _ | Easync _ | Eifthenelse
| (Eequal | Efun _ | Enode _ | Eifthenelse
| Efield_update), _ -> -1
| (Earray | Earray_fill | Eselect | Eselect_slice | Eselect_dyn
| Eselect_trunc | Eupdate | Econcat ), _ -> 1

7
compiler/minils/mls_printer.ml
View file

@ -163,13 +163,6 @@ and print_app ff (app, args) =
| Efun f | Enode f ->
fprintf ff "@[%a@,%a@,%a@]"
print_qualname f print_params app.a_params print_w_tuple args
| Easync (f, ack) ->
fprintf ff "@[async %a@,%a@,%a on %s@,%a@]"
print_qualname f
print_params app.a_params
print_w_tuple args
ack.ack_name
print_static_exp_tuple ack.ack_params
| Eifthenelse ->
let e1, e2, e3 = assert_3 args in
fprintf ff "@[<hv>if %a@ then %a@ else %a@]"

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

@ -188,12 +188,6 @@ struct
| Eapp ({ a_op = Enode ln; a_params = params } as app, e_list, r) ->
let op = Enode (node_for_params_call ln (instantiate m params)) in
Eapp ({ app with a_op = op; a_params = [] }, e_list, r)
| Eapp ({ a_op = Easync (ln, ack);
a_params = params } as app, e_list, r) ->
let op =
Easync (node_for_params_call ln (instantiate m params), ack)
in
Eapp ({ app with a_op = op; a_params = [] }, e_list, r)
| Eiterator(it, ({ a_op = Efun ln; a_params = params } as app),
n, pe_list, e_list, r) ->
let op = Efun (node_for_params_call ln (instantiate m params)) in
@ -204,7 +198,6 @@ struct
let op = Enode (node_for_params_call ln (instantiate m params)) in
Eiterator(it,{app with a_op = op; a_params = [] },
n, pe_list, e_list, r)
(* TODO(Arduino): iterator *)
| _ -> ed
in ed, m
@ -320,11 +313,10 @@ let collect_node_calls ln =
else (ln, params)::acc
in
let edesc _ acc ed = match ed with
| Eapp ({ a_op = (Enode ln | Efun ln | Easync (ln, _));
a_params = params }, _, _) ->
| Eapp ({ a_op = (Enode ln | Efun ln); a_params = params }, _, _) ->
ed, add_called_node ln params acc
| Eiterator(_, { a_op = (Enode ln | Efun ln | Easync (ln, _));
a_params = params }, _, _, _, _) ->
| Eiterator(_, { a_op = (Enode ln | Efun ln); a_params = params },
_, _, _, _) ->
ed, add_called_node ln params acc
| _ -> raise Errors.Fallback
in

50
compiler/obc/c/async.ml
View file

@ -1,50 +0,0 @@
open Obc
open C
open Modules
open Idents
open Names
open Signature
let async_global_var_name od = "g_async__" ^ (name od.o_ident)
let filter_async_objs cd =
List.filter
(fun od ->
match od.o_ack with
| Some _ -> true
| None -> false)
cd.cd_objs
let async_global_objs_vars cd =
List.map
(fun od ->
let name = async_global_var_name od in
let ty = Cty_id (qn_append od.o_class "_async") in
name, ty)
(filter_async_objs cd)
let async_global_objs_defs cd =
List.map
(fun (name, ty) -> Cvardef (name, ty))
(async_global_objs_vars cd)
let async_global_objs_decls cd =
List.map
(fun (name, ty) -> Cdecl_extern (name, ty))
(async_global_objs_vars cd)
let od_is_stateful od =
let sig_info = find_value od.o_class in
sig_info.node_stateful
let async_reset cd =
let async_objs = filter_async_objs cd in
let stateful = List.filter od_is_stateful async_objs in
List.map
(fun od ->
let global = Cvar (async_global_var_name od) in
let field = Cfield (global, local_qn "self") in
let reset = cname_of_qn od.o_class ^ "_reset" in
Csexpr (Cfun_call (reset, [Caddrof field])))
stateful

125
compiler/obc/c/async_avr.ml
View file

@ -1,125 +0,0 @@
open Names
open Types
open C
open Obc
open Async
open Async_backend
module AvrBackend : AsyncBackend =
struct
type clock =
| Timer_ms of int
(* FIXME(Arduino): don't do a shallow copy *)
let gen_copy_func cd suffix =
let func_name = (cname_of_qn cd.cd_name) ^ "_copy" ^ suffix in
(* TODO(Arduino): add const qualifier *)
let arg_ty = Cty_ptr (Cty_id (qn_append cd.cd_name suffix)) in
let sizeof = Cfun_call ("sizeof", [Cderef (Cvar "src")]) in
let memcpy =
Cfun_call ("atomic_memcpy", [Cvar "dest"; Cvar "src"; sizeof])
in
Cfundef {
C.f_name = func_name;
f_retty = Cty_void;
f_args = [("dest", arg_ty); ("src", arg_ty)];
f_body = {
var_decls = [];
block_body = [Csexpr memcpy] }
}
let gen_copy_func_in cd = gen_copy_func cd "_in"
let gen_copy_func_out cd = gen_copy_func cd "_out"
let includes = ["avr"]
let translate_ack { ack_name = name; ack_params = params } =
match params with
| [{se_desc = Sint ms}] when name = "timer_ms" -> Timer_ms ms
| _ -> assert false
let rec gcd a = function
| 0 -> abs a
| b -> gcd b (a mod b)
let lcm a b = match a, b with
| 0, _ | _, 0 -> 0
| _ -> abs (a * b) / (gcd a b)
let fold_lcm l = List.fold_left lcm (List.hd l) (List.tl l)
let fold_gcd l = List.fold_left gcd (List.hd l) (List.tl l)
let ms_of_ack = function
| Timer_ms ms -> ms
let incr_mod name modulo =
let one_const = Cconst (Ccint 1) in
let modulo_const = Cconst (Ccint modulo) in
let incr = Cbop ("+", Cvar name, one_const) in
Caffect (CLvar name, Cbop ("%", incr, modulo_const))
let call_step_async tick_var base (od, ack) =
let step = (cname_of_qn od.o_class) ^ "_async_step" in
let global = async_global_var_name od in
let call = Csexpr (Cfun_call (step, [Caddrof (Cvar global)])) in
let zero = Cconst (Ccint 0) in
let timer = Cconst (Ccint (ms_of_ack ack / base)) in
let cond = Cbop ("==", Cbop ("%", tick_var, timer), zero) in
Cif (cond, [call], [])
let translate_objs objs =
List.map
(fun od ->
let ack = Option.get od.o_ack in
(od, translate_ack ack))
objs
let decls_and_defs objs =
let trans = translate_objs objs in
let timers = List.map
(fun (_, ack) -> ms_of_ack ack)
trans
in
let body = match timers with
| [] -> []
| _ ->
let gcd_timer = fold_gcd timers in
let lcm_timer = fold_lcm timers in
let steps =
List.map (call_step_async (Cvar "tick") gcd_timer) trans
in
let incr = incr_mod "tick" (lcm_timer / gcd_timer) in
steps @ [incr]
in
(* run_timers is declared in avr.h (because of the ISR macro which
* I don't know how to generate here) *)
let defs = [
Cfundef {
C.f_name = "run_timers";
f_retty = Cty_void;
f_args = [];
f_body = {
var_decls = [
mk_vardecl_val ~static:true "tick" Cty_int (Cconst (Ccint 0))
];
block_body = body
}
}
] in
[], defs
let main_init objs =
let trans = translate_objs objs in
let timers = List.map
(fun (_, ack) -> ms_of_ack ack)
trans
in
match timers with
| [] -> []
| _ ->
let value = fold_gcd timers in
[Csexpr (Cfun_call ("init_timer1", [Cconst (Ccint value)]))]
end

11
compiler/obc/c/async_backend.mli
View file

@ -1,11 +0,0 @@
open C
open Obc
module type AsyncBackend =
sig
val gen_copy_func_in : class_def -> cdef
val gen_copy_func_out : class_def -> cdef
val includes : string list
val decls_and_defs : obj_dec list -> cdecl list * cdef list
val main_init : obj_dec list -> cstm list
end

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

@ -69,18 +69,11 @@ type cty =
| Cty_arr of int * cty (** A static array of the specified size. *)
| Cty_void (** Well, [void] is not really a C type. *)
type cvardecl = {
vd_name : string;
vd_ty : cty;
vd_static : bool;
vd_value : cexpr option
}
(** A C block: declarations and statements. In source code form, it begins with
variable declarations before a list of semicolon-separated statements, the
whole thing being enclosed in curly braces. *)
and cblock = {
var_decls : cvardecl list;
type cblock = {
var_decls : (string * cty) list;
(** Variable declarations, where each declaration consists of a variable
name and the associated C type. *)
block_body : cstm list;
@ -143,7 +136,6 @@ type cdecl =
(** C function declaration. *)
| Cdecl_constant of string * cty * cexpr
(** C constant declaration (alias, name)*)
| Cdecl_extern of string * cty
(** C function definitions *)
type cfundef = {
@ -163,10 +155,6 @@ let cdecl_of_cfundef cfd = match cfd with
| Cfundef cfd -> Cdecl_function (cfd.f_name, cfd.f_retty, cfd.f_args)
| _ -> invalid_arg "cdecl_of_cfundef"
let cdef_name = function
| Cfundef cfd -> cfd.f_name
| Cvardef (name, _) -> name
(** A C file can be a source file, containing definitions, or a header file,
containing declarations. *)
type cfile = string * cfile_desc
@ -177,15 +165,6 @@ and cfile_desc =
(******************************)
let mk_vardecl ?(static = false) ?(value = None) name ty =
{ vd_name = name; vd_ty = ty; vd_static = static; vd_value = value }
let mk_vardecl_val ?(static = false) name ty value =
mk_vardecl ~static:static ~value:(Some value) name ty
let vardecl_of_cvars cvars =
List.map (fun (name, ty) -> mk_vardecl name ty) cvars
(** {3 Pretty-printing of the C ast.} *)
(** [pp_list1 f sep fmt l] pretty-prints into the Format.formatter [fmt]
@ -252,7 +231,7 @@ and pp_param_list fmt l = pp_list1 pp_vardecl "," fmt l
and pp_var_list fmt l = pp_list pp_vardecl ";" fmt l
let rec pp_cblock fmt cb =
let pp_varlist = pp_list pp_cvardecl ";" in
let pp_varlist = pp_list pp_vardecl ";" in
fprintf fmt "%a%a" pp_varlist cb.var_decls pp_cstm_list cb.block_body
and pp_cstm_list fmt stml = pp_list pp_cstm ";" fmt stml
and pp_cstm fmt stm = match stm with
@ -325,16 +304,6 @@ and pp_cconst fmt cconst = match cconst with
| Ctag t -> pp_string fmt t
| Cstrlit t -> fprintf fmt "\"%s\"" (String.escaped t)
and pp_cvardecl fmt vd =
if vd.vd_static then
fprintf fmt "static ";
fprintf fmt "%a" pp_vardecl (vd.vd_name, vd.vd_ty);
match vd.vd_value with
| Some e -> fprintf fmt " = %a" pp_cexpr e
| None -> ()
and pp_cvardecl_list fmt l = pp_list1 pp_vardecl "," fmt l
let pp_cdecl fmt cdecl = match cdecl with
| Cdecl_enum (s, sl) ->
fprintf fmt "@[<v>@[<v 2>typedef enum {@ %a@]@ } %a;@ @]@\n"
@ -354,9 +323,6 @@ let pp_cdecl fmt cdecl = match cdecl with
| Cdecl_constant (n, cty, ce) ->
fprintf fmt "@[<v>static const %a = %a;@ @]@\n"
pp_vardecl (n, cty) pp_cconst_expr ce
| Cdecl_extern (n, cty) ->
fprintf fmt "@[<v>extern %a;@ @]@\n"
pp_vardecl (n, cty)
let pp_cdef fmt cdef = match cdef with
| Cfundef cfd ->

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

@ -34,8 +34,6 @@ open Idents
open Obc
open Obc_utils
open Types
open Async
open Async_avr
open Modules
open Signature
@ -78,40 +76,6 @@ struct
raise Errors.Error
end
type vars_rewriter =
{ vr_vars : IdentSet.t;
vr_rewrite : ident -> cexpr }
let vr_match vr var = IdentSet.mem var vr.vr_vars
let vr_direct vars =
{ vr_vars = vars;
vr_rewrite = fun var -> Cvar (name var) }
let vr_field st_expr vars =
{ vr_vars = vars;
vr_rewrite = fun var -> Cfield (st_expr, local_qn (name var)) }
let vr_rewrite vr var =
if vr_match vr var then
vr.vr_rewrite var
else
Cvar (name var)
let vr_compose a b =
let rewrite var =
let vr = if vr_match a var then a else b in
vr_rewrite vr var
in
{ vr_rewrite = rewrite;
vr_vars = IdentSet.union a.vr_vars b.vr_vars }
let ident_set_of_var_decs vds =
List.fold_left
(fun set vd -> IdentSet.add vd.v_ident set)
IdentSet.empty
vds
let struct_name ty =
match ty with
| Cty_id n -> n
@ -258,10 +222,7 @@ let rec assoc_type_lhs lhs var_env = match lhs with
| Cty_ptr ty -> ty
| _ -> Error.message no_location Error.Ederef_not_pointer)
| CLfield(CLderef (CLvar "self"), { name = x }) -> assoc_type x var_env
(* TODO(Arduino): it's probably not necessary, but we could choose to
use assoc_type depending on the async state of the node *)
| CLfield(CLderef (CLvar "_out"), { name = x }) -> assoc_type x var_env
| CLfield(CLvar "_local_out", { name = x }) -> assoc_type x var_env
| CLfield(x, f) ->
let ty = assoc_type_lhs x var_env in
let n = struct_name ty in
@ -338,18 +299,18 @@ let rec cexpr_of_static_exp se =
| Stuple _ -> Misc.internal_error "cgen: static tuple"
(** [cexpr_of_exp exp] translates the Obj action [exp] to a C expression. *)
and cexpr_of_exp vr var_env exp =
and cexpr_of_exp out_env var_env exp =
match exp.e_desc with
| Eextvalue w -> cexpr_of_ext_value vr var_env w
| Eextvalue w -> cexpr_of_ext_value out_env var_env w
(* Operators *)
| Eop(op, exps) -> cop_of_op vr var_env op exps
| Eop(op, exps) -> cop_of_op out_env var_env op exps
(* Structure literals. *)
| Estruct (tyn, fl) ->
let cexpr = cexpr_of_exp vr var_env in
let cexpr = cexpr_of_exp out_env var_env in
let cexps_assoc = List.rev_map (fun (f, e) -> f, cexpr e) fl in
cexpr_of_struct tyn cexps_assoc
| Earray e_list ->
Carraylit (cexprs_of_exps vr var_env e_list)
Carraylit (cexprs_of_exps out_env var_env e_list)
and cexpr_of_struct tyn cexps_assoc =
let cexps = List.fold_left
@ -358,8 +319,8 @@ and cexpr_of_struct tyn cexps_assoc =
(* Reverse `cexps' here because of the previous use of `List.fold_left'. *)
Cstructlit (cname_of_qn tyn, List.rev cexps)
and cexprs_of_exps vr var_env exps =
List.map (cexpr_of_exp vr var_env) exps
and cexprs_of_exps out_env var_env exps =
List.map (cexpr_of_exp out_env var_env) exps
and cop_of_op_aux op_name cexps = match op_name with
| { qual = Pervasives; name = op } ->
@ -383,15 +344,20 @@ and cop_of_op_aux op_name cexps = match op_name with
Cfun_call("fprintf", file::s::args)
| { name = op } -> Cfun_call(op,cexps)
and cop_of_op vr var_env op_name exps =
let cexps = cexprs_of_exps vr var_env exps in
and cop_of_op out_env var_env op_name exps =
let cexps = cexprs_of_exps out_env var_env exps in
cop_of_op_aux op_name cexps
and clhs_of_pattern vr var_env l = match l.pat_desc with
and clhs_of_pattern out_env var_env l = match l.pat_desc with
(* Each Obc variable corresponds to a real local C variable. *)
| Lvar v ->
let n = name v in
let n_lhs = clhs_of_cexpr (vr_rewrite vr v) in
let n_lhs =
if IdentSet.mem v out_env
then CLfield (CLderef (CLvar "_out"), local_qn n)
else CLvar n
in
if List.mem_assoc n var_env then
let ty = assoc_type n var_env in
(match ty with
@ -403,19 +369,24 @@ and clhs_of_pattern vr var_env l = match l.pat_desc with
(* Dereference our [self] struct holding the node's memory. *)
| Lmem v -> CLfield (CLderef (CLvar "self"), local_qn (name v))
(* Field access. /!\ Indexed Obj expression should be a valid lhs! *)
| Lfield (l, fn) -> CLfield(clhs_of_pattern vr var_env l, fn)
| Lfield (l, fn) -> CLfield(clhs_of_pattern out_env var_env l, fn)
| Larray (l, idx) ->
CLarray(clhs_of_pattern vr var_env l,
cexpr_of_exp vr var_env idx)
CLarray(clhs_of_pattern out_env var_env l,
cexpr_of_exp out_env var_env idx)
and clhs_list_of_pattern_list vr var_env lhss =
List.map (clhs_of_pattern vr var_env) lhss
and clhs_list_of_pattern_list out_env var_env lhss =
List.map (clhs_of_pattern out_env var_env) lhss
and cexpr_of_pattern vr var_env l = match l.pat_desc with
and cexpr_of_pattern out_env var_env l = match l.pat_desc with
(* Each Obc variable corresponds to a real local C variable. *)
| Lvar v ->
let n = name v in
let n_lhs = vr_rewrite vr v in
let n_lhs =
if IdentSet.mem v out_env
then Cfield (Cderef (Cvar "_out"), local_qn n)
else Cvar n
in
if List.mem_assoc n var_env then
let ty = assoc_type n var_env in
(match ty with
@ -427,17 +398,22 @@ and cexpr_of_pattern vr var_env l = match l.pat_desc with
(* Dereference our [self] struct holding the node's memory. *)
| Lmem v -> Cfield (Cderef (Cvar "self"), local_qn (name v))
(* Field access. /!\ Indexed Obj expression should be a valid lhs! *)
| Lfield (l, fn) -> Cfield(cexpr_of_pattern vr var_env l, fn)
| Lfield (l, fn) -> Cfield(cexpr_of_pattern out_env var_env l, fn)
| Larray (l, idx) ->
Carray(cexpr_of_pattern vr var_env l,
cexpr_of_exp vr var_env idx)
Carray(cexpr_of_pattern out_env var_env l,
cexpr_of_exp out_env var_env idx)
and cexpr_of_ext_value vr var_env w = match w.w_desc with
and cexpr_of_ext_value out_env var_env w = match w.w_desc with
| Wconst c -> cexpr_of_static_exp c
(* Each Obc variable corresponds to a plain local C variable. *)
| Wvar v ->
let n = name v in
let n_lhs = vr_rewrite vr v in
let n_lhs =
if IdentSet.mem v out_env
then Cfield (Cderef (Cvar "_out"), local_qn n)
else Cvar n
in
if List.mem_assoc n var_env then
let ty = assoc_type n var_env in
(match ty with
@ -448,10 +424,10 @@ and cexpr_of_ext_value vr var_env w = match w.w_desc with
(* Dereference our [self] struct holding the node's memory. *)
| Wmem v -> Cfield (Cderef (Cvar "self"), local_qn (name v))
(* Field access. /!\ Indexed Obj expression should be a valid lhs! *)
| Wfield (l, fn) -> Cfield(cexpr_of_ext_value vr var_env l, fn)
| Wfield (l, fn) -> Cfield(cexpr_of_ext_value out_env var_env l, fn)
| Warray (l, idx) ->
Carray(cexpr_of_ext_value vr var_env l,
cexpr_of_exp vr var_env idx)
Carray(cexpr_of_ext_value out_env var_env l,
cexpr_of_exp out_env var_env idx)
let rec assoc_obj instance obj_env =
match obj_env with
@ -474,7 +450,7 @@ let out_var_name_of_objn o =
(** Creates the list of arguments to call a node. [targeting] is the targeting
of the called node, [mem] represents the node context and [args] the
argument list.*)
let step_fun_call vr var_env sig_info objn out args async =
let step_fun_call out_env var_env sig_info objn out args =
let rec add_targeting l ads = match l, ads with
| [], [] -> []
| e::l, ad::ads ->
@ -492,50 +468,34 @@ let step_fun_call vr var_env sig_info objn out args async =
let f = Cfield (Cderef (Cvar "self"), local_qn (name o)) in
let rec mk_idx pl = match pl with
| [] -> f
| p::pl ->
Carray (mk_idx pl, cexpr_of_pattern vr var_env p)
| p::pl -> Carray (mk_idx pl, cexpr_of_pattern out_env var_env p)
in
mk_idx l
) in
match async with
| Some async -> args @ [Caddrof out; Caddrof async]
| None -> args @ [Caddrof out; Caddrof mem]
args@[Caddrof out; Caddrof mem]
) else
match async with
| Some async -> args @ [Caddrof out; Caddrof async]
| None -> args @ [Caddrof out]
args@[Caddrof out]
(** Generate the statement to call [objn].
[outvl] is a list of lhs where to put the results.
[args] is the list of expressions to use as arguments.
[mem] is the lhs where is stored the node's context.*)
let generate_function_call vr var_env obj_env outvl objn args =
let generate_function_call out_env var_env obj_env outvl objn args =
(* Class name for the object to step. *)
let classln = assoc_cn objn obj_env in
let classn = cname_of_qn classln in
let sig_info = find_value classln in
let out = Cvar (out_var_name_of_objn classn) in
let od = assoc_obj (obj_ref_name objn) obj_env in
let fun_call =
if is_op classln then
cop_of_op_aux classln args
else
let async = match od.o_ack with
| Some _ -> Some (Cvar (async_global_var_name od))
| None -> None
in
(* The step function takes scalar arguments and its own internal
memory holding structure. *)
let args =
step_fun_call vr var_env sig_info objn out args async
in
(* The step function takes scalar arguments and its own internal memory
holding structure. *)
let args = step_fun_call out_env var_env sig_info objn out args in
(* Our C expression for the function call. *)
let suffix = match od.o_ack with
| Some _ -> "_step_async_stub"
| None -> "_step"
in
Cfun_call (classn ^ suffix, args)
Cfun_call (classn ^ "_step", args)
in
(* Act according to the length of our list. Step functions with
@ -553,7 +513,7 @@ let generate_function_call vr var_env obj_env outvl objn args =
let ty = assoc_type_lhs outv var_env in
create_affect_stm outv (Cfield (out, local_qn out_name)) ty
in
(Csexpr fun_call) :: (List.flatten (map2 create_affect outvl out_sig))
(Csexpr fun_call)::(List.flatten (map2 create_affect outvl out_sig))
(** Create the statement dest = c where c = v^n^m... *)
let rec create_affect_const var_env (dest : clhs) c =
@ -591,23 +551,23 @@ let rec create_affect_const var_env (dest : clhs) c =
(** [cstm_of_act obj_env mods act] translates the Obj action [act] to a list of
C statements, using the association list [obj_env] to map object names to
class names. *)
let rec cstm_of_act vr var_env obj_env act =
let rec cstm_of_act out_env var_env obj_env act =
match act with
(* Cosmetic : cases on boolean values are converted to if statements. *)
| Acase (c, [({name = "true"}, te); ({ name = "false" }, fe)])
| Acase (c, [({name = "false"}, fe); ({ name = "true"}, te)]) ->
let cc = cexpr_of_exp vr var_env c in
let cte = cstm_of_act_list vr var_env obj_env te in
let cfe = cstm_of_act_list vr var_env obj_env fe in
let cc = cexpr_of_exp out_env var_env c in
let cte = cstm_of_act_list out_env var_env obj_env te in
let cfe = cstm_of_act_list out_env var_env obj_env fe in
[Cif (cc, cte, cfe)]
| Acase (c, [({name = "true"}, te)]) ->
let cc = cexpr_of_exp vr var_env c in
let cte = cstm_of_act_list vr var_env obj_env te in
let cc = cexpr_of_exp out_env var_env c in
let cte = cstm_of_act_list out_env var_env obj_env te in
let cfe = [] in
[Cif (cc, cte, cfe)]
| Acase (c, [({name = "false"}, fe)]) ->
let cc = Cuop ("!", (cexpr_of_exp vr var_env c)) in
let cte = cstm_of_act_list vr var_env obj_env fe in
let cc = Cuop ("!", (cexpr_of_exp out_env var_env c)) in
let cte = cstm_of_act_list out_env var_env obj_env fe in
let cfe = [] in
[Cif (cc, cte, cfe)]
@ -621,36 +581,36 @@ let rec cstm_of_act vr var_env obj_env act =
let ccl =
List.map
(fun (c,act) -> cname_of_qn c,
cstm_of_act_list vr var_env obj_env act) cl in
[Cswitch (cexpr_of_exp vr var_env e, ccl)]
cstm_of_act_list out_env var_env obj_env act) cl in
[Cswitch (cexpr_of_exp out_env var_env e, ccl)]
| Ablock b ->
cstm_of_act_list vr var_env obj_env b
cstm_of_act_list out_env var_env obj_env b
(* For composition of statements, just recursively apply our
translation function on sub-statements. *)
| Afor ({ v_ident = x }, i1, i2, act) ->
[Cfor(name x, cexpr_of_exp vr var_env i1,
cexpr_of_exp vr var_env i2,
cstm_of_act_list vr var_env obj_env act)]
[Cfor(name x, cexpr_of_exp out_env var_env i1,
cexpr_of_exp out_env var_env i2,
cstm_of_act_list out_env var_env obj_env act)]
(* Translate constant assignment *)
| Aassgn (vn, { e_desc = Eextvalue { w_desc = Wconst c }; }) ->
let vn = clhs_of_pattern vr var_env vn in
let vn = clhs_of_pattern out_env var_env vn in
create_affect_const var_env vn c
(* Purely syntactic translation from an Obc local variable to a C
local one, with recursive translation of the rhs expression. *)
| Aassgn (vn, e) ->
let vn = clhs_of_pattern vr var_env vn in
let vn = clhs_of_pattern out_env var_env vn in
let ty = assoc_type_lhs vn var_env in
let ce = cexpr_of_exp vr var_env e in
let ce = cexpr_of_exp out_env var_env e in
create_affect_stm vn ce ty
(* Our Aop marks an operator invocation that will perform side effects. Just
translate to a simple C statement. *)
| Aop (op_name, args) ->
[Csexpr (cop_of_op vr var_env op_name args)]
[Csexpr (cop_of_op out_env var_env op_name args)]
(* Reinitialization of an object variable, extracting the reset
function's name from our environment [obj_env]. *)
@ -669,8 +629,7 @@ let rec cstm_of_act vr var_env obj_env act =
| [] ->
[Csexpr (Cfun_call (classn ^ "_reset", [Caddrof field]))]
| p::pl ->
mk_loop pl
(Carray (field, cexpr_of_pattern vr var_env p))
mk_loop pl (Carray(field, cexpr_of_pattern out_env var_env p))
in
mk_loop pl field
)
@ -679,21 +638,19 @@ let rec cstm_of_act vr var_env obj_env act =
local structure to hold the results, before allocating to our
variables. *)
| Acall (outvl, objn, Mstep, el) ->
let args = cexprs_of_exps vr var_env el in
let outvl = clhs_list_of_pattern_list vr var_env outvl in
generate_function_call vr var_env obj_env outvl objn args
let args = cexprs_of_exps out_env var_env el in
let outvl = clhs_list_of_pattern_list out_env var_env outvl in
generate_function_call out_env var_env obj_env outvl objn args
and cstm_of_act_list vr var_env obj_env b =
and cstm_of_act_list out_env var_env obj_env b =
let l = List.map cvar_of_vd b.b_locals in
let var_env = l @ var_env in
let cstm = List.flatten
(List.map (cstm_of_act vr var_env obj_env) b.b_body)
in
let cstm = List.flatten (List.map (cstm_of_act out_env var_env obj_env) b.b_body) in
match l with
| [] -> cstm
| _ -> [Csblock { var_decls = vardecl_of_cvars l;
block_body = cstm }]
| _ ->
[Csblock { var_decls = l; block_body = cstm }]
(* TODO needed only because of renaming phase *)
let global_name = ref "";;
@ -702,18 +659,22 @@ let global_name = ref "";;
(** {2 step() and reset() functions generation} *)
let qn_append q suffix =
{ qual = q.qual; name = q.name ^ suffix }
(** Builds the argument list of step function*)
let step_fun_args n md add_mem =
let step_fun_args n md =
let args = inputlist_of_ovarlist md.m_inputs in
let out_arg = [("_out", Cty_ptr (Cty_id (qn_append n "_out")))] in
let context_arg =
if is_stateful n && add_mem then
if is_stateful n then
[("self", Cty_ptr (Cty_id (qn_append n "_mem")))]
else
[]
in
args @ out_arg @ context_arg
(** [fun_def_of_step_fun name obj_env mods sf] returns a C function definition
[name ^ "_out"] corresponding to the Obc step function [sf]. The object name
<-> class name mapping [obj_env] is needed to translate internal steps and
@ -724,7 +685,7 @@ let fun_def_of_step_fun n obj_env mem objs md =
let fun_name = (cname_of_qn n) ^ "_step" in
(* Its arguments, translating Obc types to C types and adding our internal
memory structure. *)
let args = step_fun_args n md true in
let args = step_fun_args n md in
(* Out vars for function calls *)
let out_vars =
@ -736,122 +697,21 @@ let fun_def_of_step_fun n obj_env mem objs md =
(* The body *)
let mems = List.map cvar_of_vd (mem@md.m_outputs) in
let var_env = args @ mems @ out_vars in
let vr = vr_compose
(vr_field (Cderef (Cvar "_out")) (ident_set_of_var_decs md.m_outputs))
(vr_direct (ident_set_of_var_decs md.m_inputs))
in
let body =
cstm_of_act_list vr var_env obj_env md.m_body
in
Cfundef {
C.f_name = fun_name;
f_retty = Cty_void;
f_args = args;
f_body = {
var_decls = vardecl_of_cvars out_vars;
block_body = body
}
}
let async_ty n =
Cty_ptr (Cty_id (qn_append n "_async"))
let async_field_ptr name =
Caddrof (Cfield (Cderef (Cvar "_async"), local_qn name))
let fun_stub_def_of_step_fun n md copy_in copy_out =
let fun_name = (cname_of_qn n) ^ "_step_async_stub" in
let args = (step_fun_args n md false) @ [("_async", async_ty n)] in
let out_vars = [("_in", Cty_id (qn_append n "_in"))] in
let prologue = List.flatten (List.map
(fun (src_name, ty) ->
let src = Cvar src_name in
let dest = CLfield (CLvar "_in", local_qn src_name) in
create_affect_stm dest src ty)
(inputlist_of_ovarlist md.m_inputs))
in
let body = [
Csexpr (Cfun_call (copy_in, [async_field_ptr "in"; Caddrof (Cvar "_in")]));
Csexpr (Cfun_call (copy_out, [Cvar "_out"; async_field_ptr "out"]))
] in
Cfundef {
C.f_name = fun_name;
f_retty = Cty_void;
f_args = args;
f_body = {
var_decls = vardecl_of_cvars out_vars;
block_body = prologue @ body
}
}
let async_fun_def_of_step_fun n obj_env mem objs md copy_in copy_out =
let fun_name = (cname_of_qn n) ^ "_async_step" in
let args = [("_async", async_ty n)] in
(* Out vars for function calls *)
let out_vars =
unique
(List.map (fun obj -> out_var_name_of_objn (cname_of_qn obj.o_class),
Cty_id (qn_append obj.o_class "_out"))
(List.filter (fun obj -> not (is_op obj.o_class)) objs)) in
let out_vars =
let out_env =
List.fold_left
(fun out_vars s -> ("_local" ^ s, Cty_id (qn_append n s)) :: out_vars)
out_vars
["_in"; "_out"]
(fun out_env vd -> IdentSet.add vd.v_ident out_env)
IdentSet.empty
md.m_outputs
in
(* FIXME(Arduino): it is probably easier to access to self directly from
_async struct pointer, but the string "self" is hardcoded in a large
number of places… *)
let out_vars =
if is_stateful n then
("self", Cty_ptr (Cty_id (qn_append n "_mem"))) :: out_vars
else
out_vars
in
(* The body *)
let mems = List.map cvar_of_vd (mem@md.m_outputs) in
let var_env = args @ mems @ out_vars in
let async_field_ptr name =
Caddrof (Cfield (Cderef (Cvar "_async"), local_qn name))
in
let l_in = Cvar "_local_in" in
let l_out = Cvar "_local_out" in
let vr = vr_compose
(vr_field l_out (ident_set_of_var_decs md.m_outputs))
(vr_field l_in (ident_set_of_var_decs md.m_inputs))
in
let prologue = [
Csexpr (Cfun_call (copy_in, [Caddrof l_in; async_field_ptr "in"]))
] in
let prologue =
if is_stateful n then
(Caffect (CLvar "self", async_field_ptr "self")) :: prologue
else
prologue
in
let body = cstm_of_act_list vr var_env obj_env md.m_body in
let epilogue = [
Csexpr (Cfun_call (copy_out, [async_field_ptr "out"; Caddrof l_out]))
] in
let body = cstm_of_act_list out_env var_env obj_env md.m_body in
Cfundef {
C.f_name = fun_name;
f_retty = Cty_void;
f_args = args;
f_body = {
var_decls = vardecl_of_cvars out_vars;
block_body = prologue @ body @ epilogue
var_decls = out_vars;
block_body = body
}
}
@ -885,42 +745,20 @@ let mem_decl_of_class_def cd =
) else
[]
let in_decl_of_class_def cd =
let step_m = find_step_method cd in
let in_fields = List.map cvar_of_vd step_m.m_inputs in
[Cdecl_struct ((cname_of_qn cd.cd_name) ^ "_in", in_fields)]
let out_decl_of_class_def cd =
(* Fields corresponding to output variables. *)
let step_m = find_step_method cd in
let out_fields = List.map cvar_of_vd step_m.m_outputs in
[Cdecl_struct ((cname_of_qn cd.cd_name) ^ "_out", out_fields)]
let async_decl_of_class_def cd =
let struct_field suffix name =
let qn = qn_append cd.cd_name suffix in
(name, Cty_id qn)
in
let fields = [
struct_field "_in" "in";
struct_field "_out" "out"
] in
let fields = if is_stateful cd.cd_name then
(struct_field "_mem" "self") :: fields
else
fields
in
[Cdecl_struct ((cname_of_qn cd.cd_name) ^ "_async", fields)]
(** [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 body =
if cd.cd_stateful then
let var_env = List.map cvar_of_vd cd.cd_mems in
let vr = vr_direct IdentSet.empty in
let reset = find_reset_method cd in
cstm_of_act_list vr var_env cd.cd_objs reset.m_body
cstm_of_act_list IdentSet.empty var_env cd.cd_objs reset.m_body
else
[]
in
@ -934,6 +772,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 =
@ -943,38 +782,21 @@ let cdefs_and_cdecls_of_class_def cd =
Idents.enter_node cd.cd_name;
let step_m = find_step_method cd in
let memory_struct_decl = mem_decl_of_class_def cd in
let in_struct_decl = in_decl_of_class_def cd in
let out_struct_decl = out_decl_of_class_def cd in
let async_struct_decl = async_decl_of_class_def cd in
let objs = async_global_objs_defs cd in
let objs_decls = async_global_objs_decls cd in
let step = fun_def_of_step_fun cd.cd_name cd.cd_objs cd.cd_mems
cd.cd_objs step_m in
(* TODO(Arduino): let the user choose the backend they want *)
let copy_in = AvrBackend.gen_copy_func_in cd in
let copy_out = AvrBackend.gen_copy_func_out cd in
let async_stub =
fun_stub_def_of_step_fun cd.cd_name step_m
(cdef_name copy_in) (cdef_name copy_out)
in
let async_step =
async_fun_def_of_step_fun cd.cd_name cd.cd_objs cd.cd_mems
cd.cd_objs step_m (cdef_name copy_in) (cdef_name copy_out)
in
let step_fun_def = fun_def_of_step_fun cd.cd_name
cd.cd_objs cd.cd_mems cd.cd_objs step_m in
(* C function for resetting our memory structure. *)
let reset = reset_fun_def_of_class_def cd in
let defs = [step; copy_in; copy_out; async_stub; async_step] in
let defs =
let reset_fun_def = reset_fun_def_of_class_def cd in
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_stateful cd.cd_name then
reset :: defs
([res_fun_decl; step_fun_decl], [reset_fun_def; step_fun_def])
else
defs
in
let decls = List.map cdecl_of_cfundef defs in
([step_fun_decl], [step_fun_def]) in
memory_struct_decl @ in_struct_decl @ out_struct_decl @ async_struct_decl
@ objs_decls @ decls, objs @ defs
memory_struct_decl @ out_struct_decl @ decls,
defs
(** {2 Type translation} *)
@ -1061,17 +883,9 @@ let global_file_header name prog =
| s -> s ^ "_types")
dependencies in
let dependencies_types = AvrBackend.includes @ dependencies_types in
let classes = program_classes prog in
let async_objs = List.flatten
(List.map filter_async_objs classes)
in
let decls_and_defs = List.map cdefs_and_cdecls_of_class_def classes in
let decls_and_defs =
(AvrBackend.decls_and_defs async_objs) :: decls_and_defs
in
let (decls, defs) = List.split decls_and_defs in
let (decls, defs) =
List.split (List.map cdefs_and_cdecls_of_class_def classes) in
let decls = List.concat decls
and defs = List.concat defs in

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

@ -36,8 +36,6 @@ open Types
open Signature
open C
open Cgen
open Async
open Async_avr
open Compiler_utils
(** {1 Main C function generation} *)
@ -297,13 +295,10 @@ let main_def_of_class_def cd =
@ [Csexpr funcall]
@ printf_calls
@
(if !Compiler_options.hepts_simulation || !Compiler_options.simple_simul
(if !Compiler_options.hepts_simulation
then []
else [Csexpr (Cfun_call ("puts", [Cconst (Cstrlit "")]))])
@ (if !Compiler_options.simple_simul
then []
else [Csexpr (Cfun_call ("fflush", [Cvar "stdout"]))])
in
@ [Csexpr (Cfun_call ("fflush", [Cvar "stdout"]))] in
(* Do not forget to initialize memory via reset if needed. *)
let rst_i =
@ -317,62 +312,45 @@ let main_def_of_class_def cd =
(** [main_skel var_list prologue body] generates a C main() function using the
variable list [var_list], prologue [prologue] and loop body [body]. *)
let main_skel var_list prologue body =
let args = if !Compiler_options.simple_simul then
[]
else
[("argc", Cty_int); ("argv", Cty_ptr (Cty_ptr Cty_char))]
in
let cvars = if !Compiler_options.simple_simul then
var_list
else
(step_counter, Cty_int) :: (max_step, Cty_int) :: var_list
in
let body_block = if !Compiler_options.simple_simul then
prologue
@ [
Cwhile (mk_int 1, body);
Creturn (mk_int 0)
]
else
[
(*
step_count = 0;
max_step = 0;
if (argc == 2)
max_step = atoi(argv[1]);
*)
Caffect (CLvar step_counter, mk_int 0);
Caffect (CLvar max_step, mk_int 0);
Cif (Cbop ("==", Cvar "argc", mk_int 2),
[Caffect (CLvar max_step,
Cfun_call ("atoi",
[Carray (Cvar "argv",
mk_int 1)]))], []);
]
@ prologue
(* while (!max_step || step_c < max_step) *)
@ [
Cwhile (Cbop ("||",
Cuop ("!", Cvar max_step),
Cbop ("<",
Cvar step_counter,
Cvar max_step)),
(* step_counter = step_counter + 1; *)
Caffect (CLvar step_counter,
Cbop ("+",
Cvar step_counter,
mk_int 1))
:: body);
Creturn (mk_int 0)
]
in
Cfundef {
C.f_name = "main";
f_retty = Cty_int;
f_args = args;
f_args = [("argc", Cty_int); ("argv", Cty_ptr (Cty_ptr Cty_char))];
f_body = {
var_decls = vardecl_of_cvars cvars;
block_body = body_block
var_decls =
(step_counter, Cty_int) :: (max_step, Cty_int) :: var_list;
block_body =
[
(*
step_count = 0;
max_step = 0;
if (argc == 2)
max_step = atoi(argv[1]);
*)
Caffect (CLvar step_counter, mk_int 0);
Caffect (CLvar max_step, mk_int 0);
Cif (Cbop ("==", Cvar "argc", mk_int 2),
[Caffect (CLvar max_step,
Cfun_call ("atoi",
[Carray (Cvar "argv",
mk_int 1)]))], []);
]
@ prologue
(* while (!max_step || step_c < max_step) *)
@ [
Cwhile (Cbop ("||",
Cuop ("!", Cvar max_step),
Cbop ("<",
Cvar step_counter,
Cvar max_step)),
(* step_counter = step_counter + 1; *)
Caffect (CLvar step_counter,
Cbop ("+",
Cvar step_counter,
mk_int 1))
:: body);
Creturn (mk_int 0);
];
}
}
@ -407,22 +385,6 @@ let mk_main name p =
(defs, nvar_l @ var_l, res @ res_l, nstep_l @ step_l)
with Not_found -> ([],var_l,res_l,step_l) in
let res_l = List.fold_left
(fun res cd -> (async_reset cd) @ res)
res_l
classes
in
(*
* We add these instructions at the end because otherwise the timer
* could be triggered while the initial reset of the async nodes is
* not yet terminated.
*)
let async_objs = List.flatten
(List.map filter_async_objs classes)
in
let res_l = res_l @ AvrBackend.main_init async_objs in
[("_main.c", Csource (defs @ [main_skel var_l res_l step_l]));
("_main.h", Cheader ([name], []))];
) else

3
compiler/obc/obc.ml
View file

@ -113,13 +113,10 @@ and var_dec =
v_mutable : bool;
v_loc : location }
and ack = { ack_name : ack_name; ack_params : static_exp list }
type obj_dec =
{ o_ident : obj_ident;
o_class : class_name;
o_params : static_exp list;
o_ack : ack option;
(** size of the array if the declaration is an array of obj *)
o_size : static_exp list option;
o_loc : location }

12
compiler/obc/obc_printer.ml
View file

@ -41,12 +41,6 @@ let print_vd ff vd =
print_type ff vd.v_type;
fprintf ff "@]"
let print_ack ff ack =
fprintf ff "@[%s@,%a@]"
ack.ack_name
(print_list_r print_static_exp "("","")")
ack.ack_params
let print_obj ff o =
fprintf ff "@[<v>"; print_ident ff o.o_ident;
fprintf ff " : "; print_qualname ff o.o_class;
@ -54,9 +48,6 @@ let print_obj ff o =
(match o.o_size with
| Some se -> fprintf ff "%a" (print_list_r print_static_exp "[" "][" "]") se
| None -> ());
(match o.o_ack with
| Some ack -> fprintf ff " @[async[%a]@]" print_ack ack
| None -> ());
fprintf ff "@]"
let rec print_lhs ff e =
@ -123,6 +114,7 @@ let print_method_name ff = function
| Mstep -> fprintf ff "step"
| Mreset -> fprintf ff "reset"
let rec print_act ff a =
let print_lhs_tuple ff var_list = match var_list with
| [] -> ()
@ -206,7 +198,7 @@ let print_class_def ff
end;
if objs <> [] then begin
fprintf ff "@[<hov 4>obj ";
print_list print_obj "" "; " "" ff objs;
print_list print_obj "" ";" "" ff objs;
fprintf ff ";@]@,"
end;
if mem <> [] || objs <> [] then fprintf ff "@,";

2
compiler/utilities/global/compiler_options.ml
View file

@ -84,8 +84,6 @@ let hepts_simulation = ref false
let create_object_file = ref false
let simple_simul = ref true
let boolean = ref false
let nosink = ref false

13
examples/async/simple.ept
View file

@ -1,13 +0,0 @@
node f(x : int) returns (y : int)
let
y = 0 fby x;
tel
node main() returns (y : int)
var
x : int;
let
x = 1 + (0 fby x);
y = async f(x) on timer_ms(5);
tel

59
lib/c/avr.c
View file

@ -1,59 +0,0 @@
/***********************************************************************/
/* */
/* Heptagon */
/* */
/* Gwenael Delaval, LIG/INRIA, UJF */
/* Leonard Gerard, Parkas, ENS */
/* Adrien Guatto, Parkas, ENS */
/* Cedric Pasteur, Parkas, ENS */
/* Marc Pouzet, Parkas, ENS */
/* */
/* Copyright 2012 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/> */
/* */
/***********************************************************************/
#include <util/atomic.h>
#include <avr/interrupt.h>
#include <avr/io.h>
#include <assert.h>
#include "avr.h"
ISR(TIMER1_COMPA_vect) {
run_timers();
}
static inline void set_ocr1a(uint16_t value) {
OCR1AH = value >> 8;
OCR1AL = value;
}
/* Source: https://adnbr.co.uk/articles/counting-milliseconds */
void init_timer1(unsigned int ms) {
assert(ms < 1000);
TCCR1B |= _BV(WGM12) | _BV(CS11);
set_ocr1a(((ms * F_CPU) / 1000) / 8);
TIMSK1 |= _BV(OCIE1A);
sei();
}
void atomic_memcpy(void *dest, const void *src, size_t size) {
ATOMIC_BLOCK(ATOMIC_RESTORESTATE) {
memcpy(dest, src, size);
}
}

48
lib/c/avr.h
View file

@ -1,48 +0,0 @@
/***********************************************************************/
/* */
/* Heptagon */
/* */
/* Gwenael Delaval, LIG/INRIA, UJF */
/* Leonard Gerard, Parkas, ENS */
/* Adrien Guatto, Parkas, ENS */
/* Cedric Pasteur, Parkas, ENS */
/* Marc Pouzet, Parkas, ENS */
/* */
/* Copyright 2012 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/> */
/* */
/***********************************************************************/
#ifndef DECADES_AVR_H
#define DECADES_AVR_H
#ifdef __AVR__
#include <stddef.h>
#include <string.h>
#ifndef F_CPU
#error "F_CPU must be defined"
#endif
void run_timers();
void init_timer1(unsigned int ms);
void atomic_memcpy(void *dest, const void *src, size_t size);
#endif
#endif

2
lib/c/pervasives.h
View file

@ -31,10 +31,8 @@
#ifndef DECADES_PERVASIVES_H
#define DECADES_PERVASIVES_H
#include <string.h>
typedef float real;
typedef char *string;
/* between(i, n) returns idx between 0 and n-1. */
static inline int between(int idx, int n)