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

compile ! nearly all tests passed.

Browse source
This commit is contained in:
Leonard Gerard 2011-05-09 19:32:12 +02:00 committed by Léonard Gérard
parent 22354aca0a
commit a8215c8083
19 changed files with 339 additions and 323 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
compiler/global/clocks.ml
View file

@ -38,6 +38,16 @@ let gen_index () = (incr index; !index)
(** returns a new clock variable *)
let fresh_clock () = Cvar { contents = Cindex (gen_index ()); }
(** returns a new clock type corresponding to the data type [ty] *)
let rec fresh_ct ty = match ty with
| Tprod ty_list ->
(match ty_list with
| [] -> Ck (fresh_clock())
| _ -> Cprod (List.map fresh_ct ty_list))
| Tarray (t, _) -> fresh_ct t
| Tid _ | Tinvalid -> Ck (fresh_clock())
(** returns the canonic (short) representant of a [ck]
and update it to this value. *)
let rec ck_repr ck = match ck with
@ -90,19 +100,26 @@ and unify_list t1_list t2_list =
with _ -> raise Unify
let rec skeleton ck = function
let prod ck_l = match ck_l with
| [ck] -> Ck ck
| _ -> Cprod (List.map (fun ck -> Ck ck) ck_l)
(*
let rec tuple ck = function
| Tprod ty_list ->
(match ty_list with
| [] -> Ck ck
| _ -> Cprod (List.map (skeleton ck) ty_list))
| Tarray (t, _) -> skeleton ck t
| _ -> Cprod (List.map (tuple ck) ty_list))
| Tarray (t, _) -> tuple ck t
| Tid _ | Tinvalid -> Ck ck
*)
(*
let max ck_1 ck_2 = match ck_repr ck_1, ck_reprck_2 with
|
(* TODO here it implicitely says that the base clock is Cbase
and that all tuple is on Cbase *)
let ckofct = function | Ck ck -> ck_repr ck | Cprod _ -> Cbase
let rec optim_base_ck base_ck ct = match ct with
| Ck ck ->
| Cprod c_l ->
*)

4
compiler/global/global_printer.ml
View file

@ -149,8 +149,8 @@ let print_ident ff id = Format.fprintf ff "%s" (name id)
| Cvar { contents = Cindex _ } -> fprintf ff "base"
| Cvar { contents = Clink ck } -> print_ck ff ck
let rec print_clock ff = function
let rec print_ct ff = function
| Ck ck -> print_ck ff ck
| Cprod ct_list ->
fprintf ff "@[<2>(%a)@]" (print_list_r print_clock """ *""") ct_list
fprintf ff "@[<2>(%a)@]" (print_list_r print_ct """ *""") ct_list

1
compiler/global/idents.ml
View file

@ -138,6 +138,7 @@ let ident_of_name s =
let id = { num = !num; source = s; is_generated = false } in
UniqueNames.assign_name id; id
let source_name id = id.source
let name id = UniqueNames.name id
let enter_node n = UniqueNames.enter_node n

5
compiler/global/idents.mli
View file

@ -18,6 +18,9 @@ val ident_compare : ident -> ident -> int
(** Get the full name of an identifier (it is guaranteed to be unique) *)
val name : ident -> string
(** Get the source name of an identifier (useful when dealing with signatures *)
val source_name : ident -> string
(** [gen_fresh pass_name kind_to_string kind]
generate a fresh ident with a sweet [name].
It should be used to define a [fresh] function specific to a pass. *)
@ -27,7 +30,7 @@ val gen_fresh : string -> ('a -> string) -> 'a -> ident
generates a fresh ident with a sweet [name] *)
val gen_var : string -> string -> ident
(** [ident_of_name n] returns an identifier corresponding
(** [ident_of_name n] returns an fresh identifier corresponding
to a _source_ variable (do not use it for generated variables). *)
val ident_of_name : string -> ident

13
compiler/global/signature.ml
View file

@ -9,12 +9,15 @@
(* global data in the symbol tables *)
open Names
open Types
open Clocks
(** Warning: Whenever these types are modified,
interface_format_version should be incremented. *)
let interface_format_version = "30"
type ck =
| Cbase
| Con of ck * constructor_name * name
(** Node argument : inputs and outputs *)
type arg = {
a_name : name option;
@ -50,6 +53,14 @@ type type_def =
type const_def = { c_type : ty; c_value : static_exp }
let rec ck_to_sck ck =
let ck = Clocks.ck_repr ck in
match ck with
| Clocks.Cbase -> Cbase
| Clocks.Con (ck,c,x) -> Con(ck_to_sck ck, c, Idents.source_name x)
| _ -> Misc.internal_error "Signature couldn't translate ck" 1
let names_of_arg_list l = List.map (fun ad -> ad.a_name) l
let types_of_arg_list l = List.map (fun ad -> ad.a_type) l

5
compiler/heptagon/hept_utils.ml
View file

@ -19,9 +19,10 @@ open Initial
open Heptagon
(* Helper functions to create AST. *)
let mk_exp desc ?(ct_annot = Clocks.invalid_clock) ?(loc = no_location) ty =
(* TODO : After switch, all mk_exp should take care of level_ck *)
let mk_exp desc ?(level_ck = Cbase) ?(ct_annot = None) ?(loc = no_location) ty =
{ e_desc = desc; e_ty = ty; e_ct_annot = ct_annot;
e_base_ck = Cbase; e_loc = loc; }
e_level_ck = level_ck; e_loc = loc; }
let mk_app ?(params=[]) ?(unsafe=false) op =
{ a_op = op; a_params = params; a_unsafe = unsafe }

82
compiler/heptagon/heptagon.ml
View file

@ -29,8 +29,8 @@ type iterator_type =
type exp = {
e_desc : desc;
e_ty : ty;
e_ct_annot : ct;
e_base_ck : ck;
e_ct_annot : ct option; (* exists when a source annotation exists *)
e_level_ck : ck; (* set by the switch pass, represents the base activation of the expression *)
e_loc : location }
and desc =
@ -188,82 +188,4 @@ and interface_desc =
| Itypedef of type_dec
| Iconstdef of const_dec
| Isignature of signature
(*
(* Helper functions to create AST. *)
let mk_exp desc ?(ct_annot = Clocks.invalid_clock) ?(loc = no_location) ty =
{ e_desc = desc; e_ty = ty; e_ct_annot = ct_annot;
e_base_ck = Cbase; e_loc = loc; }
let mk_app ?(params=[]) ?(unsafe=false) op =
{ a_op = op; a_params = params; a_unsafe = unsafe }
let mk_op_app ?(params=[]) ?(unsafe=false) ?(reset=None) op args =
Eapp(mk_app ~params:params ~unsafe:unsafe op, args, reset)
let mk_type_dec name desc =
{ t_name = name; t_desc = desc; t_loc = no_location; }
let mk_equation stateful desc =
{ eq_desc = desc; eq_stateful = stateful; eq_loc = no_location; }
let mk_var_dec ?(last = Var) ?(clock = fresh_clock()) name ty =
{ v_ident = name; v_type = ty; v_clock = clock;
v_last = last; v_loc = no_location }
let mk_block stateful ?(defnames = Env.empty) ?(locals = []) eqs =
{ b_local = locals; b_equs = eqs; b_defnames = defnames;
b_stateful = stateful; b_loc = no_location; }
let dfalse =
mk_exp (Econst (mk_static_bool false)) (Tid Initial.pbool)
let dtrue =
mk_exp (Econst (mk_static_bool true)) (Tid Initial.pbool)
let mk_ifthenelse e1 e2 e3 =
{ e3 with e_desc = mk_op_app Eifthenelse [e1; e2; e3] }
let mk_simple_equation stateful pat e =
mk_equation stateful (Eeq(pat, e))
let mk_switch_equation stateful e l =
mk_equation stateful (Eswitch (e, l))
let mk_signature name ins outs stateful params loc =
{ sig_name = name;
sig_inputs = ins;
sig_stateful = stateful;
sig_outputs = outs;
sig_params = params;
sig_loc = loc }
let mk_node
?(input = []) ?(output = []) ?(contract = None) ?(local = [])
?(stateful = true) ?(loc = no_location) ?(param = []) ?(constraints = [])
name block =
{ n_name = name;
n_stateful = stateful;
n_input = input;
n_output = output;
n_contract = contract;
n_block = block;
n_loc = loc;
n_params = param;
n_params_constraints = constraints }
(** @return the set of variables defined in [pat]. *)
let vars_pat pat =
let rec _vars_pat locals acc = function
| Evarpat x ->
if (IdentSet.mem x locals) or (IdentSet.mem x acc)
then acc
else IdentSet.add x acc
| Etuplepat pat_list -> List.fold_left (_vars_pat locals) acc pat_list
in _vars_pat IdentSet.empty IdentSet.empty pat
(** @return whether an object of name [n] belongs to
a list of [var_dec]. *)
let rec vd_mem n = function
| [] -> false
| vd::l -> vd.v_ident = n or (vd_mem n l)
*)

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

@ -193,8 +193,8 @@ nonmt_params:
;
param:
| ident_list COLON ty_ident
{ List.map (fun id -> mk_var_dec id $3 Var (Loc($startpos,$endpos))) $1 }
| idl=ident_list COLON ty=ty_ident ck=ck
{ List.map (fun id -> mk_var_dec id ty ck Var (Loc($startpos,$endpos))) idl }
;
out_params:
@ -248,12 +248,12 @@ loc_params:
var_last:
| ident_list COLON ty_ident
{ List.map (fun id -> mk_var_dec id $3 Var (Loc($startpos,$endpos))) $1 }
| LAST IDENT COLON ty_ident EQUAL exp
{ [ mk_var_dec $2 $4 (Last(Some($6))) (Loc($startpos,$endpos)) ] }
| LAST IDENT COLON ty_ident
{ [ mk_var_dec $2 $4 (Last(None)) (Loc($startpos,$endpos)) ] }
| idl=ident_list COLON ty=ty_ident ck=ck
{ List.map (fun id -> mk_var_dec id ty ck Var (Loc($startpos,$endpos))) idl }
| LAST id=IDENT COLON ty=ty_ident ck=ck EQUAL e=exp
{ [ mk_var_dec id ty ck (Last(Some(e))) (Loc($startpos,$endpos)) ] }
| LAST id=IDENT COLON ty=ty_ident ck=ck
{ [ mk_var_dec id ty ck (Last(None)) (Loc($startpos,$endpos)) ] }
;
ident_list:
@ -268,9 +268,13 @@ ty_ident:
{ Tarray ($1, $3) }
;
ck:
| /*empty */ { None }
| ON ck=on_ck { Some ck }
on_ck:
| /*empty */ { Cbase }
| b=on_ck ON c=constructor_or_bool LPAREN x=IDENT RPAREN { Con (b,c,x) }
| c=constructor_or_bool LPAREN x=IDENT RPAREN { Con(Cbase,c,x) }
| b=on_ck ON c=constructor_or_bool LPAREN x=IDENT RPAREN { Con(b,c,x) }
equs:
| /* empty */ { [] }
@ -630,8 +634,8 @@ nonmt_params_signature:
;
param_signature:
| IDENT COLON ty_ident ck=on_ck { mk_arg (Some $1) $3 ck }
| ty_ident ck=on_ck { mk_arg None $1 ck }
| IDENT COLON ty_ident ck=ck { mk_arg (Some $1) $3 ck }
| ty_ident ck=ck { mk_arg None $1 ck }
;
%%

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

@ -65,11 +65,14 @@ and ck =
| Cbase
| Con of ck * constructor_name * var_name
and ct =
| Ck of ck
| Cprod of ct list
and exp =
{ e_desc : edesc;
e_ct_annot : Clocks.ct;
e_loc : location }
{ e_desc : edesc;
e_ct_annot : ct option ;
e_loc : location }
and edesc =
| Econst of static_exp
@ -144,10 +147,11 @@ and present_handler =
p_block : block; }
and var_dec =
{ v_name : var_name;
v_type : ty;
v_last : last;
v_loc : location; }
{ v_name : var_name;
v_type : ty;
v_clock : ck option;
v_last : last;
v_loc : location; }
and last = Var | Last of exp option
@ -198,7 +202,7 @@ and program_desc =
type arg =
{ a_type : ty;
a_clock : ck;
a_clock : ck option;
a_name : var_name option }
type signature =
@ -223,7 +227,7 @@ and interface_desc =
(* {3 Helper functions to create AST} *)
let mk_exp desc ?(ct_annot = Clocks.invalid_clock) loc =
let mk_exp desc ?(ct_annot = None) loc =
{ e_desc = desc; e_ct_annot = ct_annot; e_loc = loc }
let mk_app op params =
@ -256,8 +260,8 @@ let mk_equation desc loc =
let mk_interface_decl desc loc =
{ interf_desc = desc; interf_loc = loc }
let mk_var_dec name ty last loc =
{ v_name = name; v_type = ty;
let mk_var_dec name ty ck last loc =
{ v_name = name; v_type = ty; v_clock = ck;
v_last = last; v_loc = loc }
let mk_block locals eqs loc =

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

@ -233,13 +233,25 @@ let rec translate_type loc ty =
with
| ScopingError err -> message loc err
let rec translate_some_clock loc env ck = match ck with
| None -> Clocks.fresh_clock()
| Some(ck) -> translate_clock loc env ck
and translate_clock loc env ck = match ck with
| Cbase -> Clocks.Cbase
| Con(ck,c,x) -> Clocks.Con(translate_clock loc env ck, qualify_constrs c, Rename.var loc env x)
let rec translate_ct loc env ct = match ct with
| Ck ck -> Clocks.Ck (translate_clock loc env ck)
| Cprod c_l -> Clocks.Cprod (List.map (translate_ct loc env) c_l)
let rec translate_exp env e =
try
{ Heptagon.e_desc = translate_desc e.e_loc env e.e_desc;
Heptagon.e_ty = Types.invalid_type;
Heptagon.e_base_ck = Clocks.Cbase;
Heptagon.e_ct_annot = e.e_ct_annot;
Heptagon.e_level_ck = Clocks.Cbase;
Heptagon.e_ct_annot = Misc.optional (translate_ct e.e_loc env) e.e_ct_annot;
Heptagon.e_loc = e.e_loc }
with ScopingError(error) -> message e.e_loc error
@ -374,9 +386,10 @@ and translate_var_dec env vd =
{ Heptagon.v_ident = Rename.var vd.v_loc env vd.v_name;
Heptagon.v_type = translate_type vd.v_loc vd.v_type;
Heptagon.v_last = translate_last vd.v_last;
Heptagon.v_clock = Clocks.fresh_clock(); (* TODO add clock annotations *)
Heptagon.v_clock = translate_some_clock vd.v_loc env vd.v_clock;
Heptagon.v_loc = vd.v_loc }
(** [env] should contain the declared variables prior to this translation *)
and translate_vd_list env =
List.map (translate_var_dec env)
@ -398,26 +411,27 @@ let params_of_var_decs =
(translate_type vd.v_loc vd.v_type))
let args_of_var_decs =
List.map (fun vd -> Signature.mk_arg
(Some vd.v_name)
(translate_type vd.v_loc vd.v_type)
Clocks.Cbase) (* before clocking and without annotations, default choice.*)
(* before the clocking the clock is wrong in the signature *)
List.map (fun vd -> Signature.mk_arg (Some (Idents.source_name vd.Heptagon.v_ident))
vd.Heptagon.v_type Signature.Cbase)
let translate_node node =
let n = current_qual node.n_name in
Idents.enter_node n;
(* Inputs and outputs define the initial local env *)
let env0 = Rename.append Rename.empty (node.n_input @ node.n_output) in
let params = params_of_var_decs node.n_params in
let inputs = translate_vd_list env0 node.n_input in
let input_env = Rename.append Rename.empty (node.n_input) in
(* inputs should refer only to inputs *)
let inputs = translate_vd_list input_env node.n_input in
(* Inputs and outputs define the initial local env *)
let env0 = Rename.append input_env node.n_output in
let outputs = translate_vd_list env0 node.n_output in
let b, env = translate_block env0 node.n_block in
let contract =
Misc.optional (translate_contract env) node.n_contract in
(* the env of the block is used in the contract translation *)
(* the env of the block is used in the contract translation *)
let contract = Misc.optional (translate_contract env) node.n_contract in
(* add the node signature to the environment *)
let i = args_of_var_decs node.n_input in
let o = args_of_var_decs node.n_output in
let i = args_of_var_decs inputs in
let o = args_of_var_decs outputs in
let p = params_of_var_decs node.n_params in
add_value n (Signature.mk_node i o node.n_stateful p);
{ Heptagon.n_name = n;
@ -483,14 +497,30 @@ let translate_program p =
Heptagon.p_desc = desc; }
let translate_signature s =
let translate_arg a =
Signature.mk_arg a.a_name
(translate_type s.sig_loc a.a_type)
(translate_clock s.sig_loc a.a_clock))
(* helper functions, having [env] as being the list of existing var names *)
let rec append env sa_l = match sa_l with
| [] -> env
| sa::sa_l -> match sa.a_name with
| None -> append env sa_l
| Some x -> append (x::env) sa_l
and translate_some_clock loc env ck = match ck with
| None -> Signature.Cbase
| Some ck -> translate_clock loc env ck
and translate_clock loc env ck = match ck with
| Cbase -> Signature.Cbase
| Con(ck,c,x) ->
if not (List.mem x env)
then message loc (Evar_unbound x)
else Signature.Con(translate_clock loc env ck, qualify_constrs c, x)
and translate_arg env a =
Signature.mk_arg a.a_name (translate_type s.sig_loc a.a_type)
(translate_some_clock s.sig_loc env a.a_clock)
in
let n = current_qual s.sig_name in
let i = List.map translate_arg s.sig_inputs in
let o = List.map translate_arg s.sig_outputs in
let env = append [] s.sig_inputs in
let i = List.map (translate_arg env) s.sig_inputs in
let env = append env s.sig_outputs in
let o = List.map (translate_arg env) s.sig_outputs in
let p = params_of_var_decs s.sig_params in
add_value n (Signature.mk_node i o s.sig_stateful p);
mk_signature n i o s.sig_stateful p s.sig_loc

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

@ -105,7 +105,7 @@ let current_level env = match env with
(** Set the base clock of an expression to the current level of the [env] *)
let annot_exp e env =
{ e with e_base_ck = current_level env }
{ e with e_level_ck = current_level env }
end

39
compiler/main/hept2mls.ml
View file

@ -104,45 +104,46 @@ let rec translate_extvalue e =
mk_extvalue (Wfield (translate_extvalue e, fn))
| _ -> Error.message e.Heptagon.e_loc Error.Enormalization
let translate
({ Heptagon.e_desc = desc; Heptagon.e_ty = ty;
Heptagon.e_loc = loc } as e) =
let mk_exp = mk_exp ~loc:loc in
match desc with
let translate ({ Heptagon.e_desc = desc; Heptagon.e_ty = ty; Heptagon.e_level_ck = b_ck;
Heptagon.e_ct_annot = a_ct; Heptagon.e_loc = loc } as e) =
let desc = match desc with
| Heptagon.Econst _
| Heptagon.Evar _
| Heptagon.Ewhen _
| Heptagon.Eapp({ Heptagon.a_op = Heptagon.Efield }, _, _) ->
let w = translate_extvalue e in
mk_exp ty (Eextvalue w)
Eextvalue w
| Heptagon.Epre(None, e) ->
mk_exp ty (Efby(None, translate_extvalue e))
Efby(None, translate_extvalue e)
| Heptagon.Epre(Some c, e) ->
mk_exp ty (Efby(Some c, translate_extvalue e))
Efby(Some c, translate_extvalue e)
| Heptagon.Efby ({ Heptagon.e_desc = Heptagon.Econst c }, e) ->
mk_exp ty (Efby(Some c, translate_extvalue e))
Efby(Some c, translate_extvalue e)
| Heptagon.Estruct f_e_list ->
let f_e_list = List.map
(fun (f, e) -> (f, translate_extvalue e)) f_e_list in
mk_exp ty (Estruct f_e_list)
Estruct f_e_list
| Heptagon.Eapp({ Heptagon.a_op = Heptagon.Earrow }, _, _) ->
Error.message loc Error.Eunsupported_language_construct
| Heptagon.Eapp(app, e_list, reset) ->
mk_exp ty (Eapp (translate_app app,
List.map translate_extvalue e_list,
translate_reset reset))
Eapp (translate_app app, List.map translate_extvalue e_list, translate_reset reset)
| Heptagon.Eiterator(it, app, n, pe_list, e_list, reset) ->
mk_exp ty
(Eiterator (translate_iterator_type it,
Eiterator (translate_iterator_type it,
translate_app app, n,
List.map translate_extvalue pe_list,
List.map translate_extvalue e_list,
translate_reset reset))
translate_reset reset)
| Heptagon.Efby _
| Heptagon.Elast _ ->
Error.message loc Error.Eunsupported_language_construct
| Heptagon.Emerge (x, c_e_list) ->
mk_exp ty (Emerge (x, List.map (fun (c,e)-> c, translate_extvalue e) c_e_list))
Emerge (x, List.map (fun (c,e)-> c, translate_extvalue e) c_e_list)
in
match a_ct with
| None -> mk_exp b_ck ty ~loc:loc desc
| Some ct -> mk_exp b_ck ty ~ct:ct ~loc:loc desc
let rec translate_pat = function
| Heptagon.Evarpat(n) -> Evarpat n
@ -167,8 +168,8 @@ let translate_contract contract =
Heptagon.c_controllables = l_c } ->
Some { c_local = List.map translate_var v;
c_eq = List.map translate_eq eq_list;
c_assume = translate e_a;
c_enforce = translate e_g;
c_assume = translate_extvalue e_a;
c_enforce = translate_extvalue e_g;
c_controllables = List.map translate_var l_c }
let node n =

4
compiler/main/mls2obc.ml
View file

@ -11,12 +11,12 @@
open Misc
open Names
open Idents
open Clocks
open Signature
open Obc
open Obc_utils
open Obc_mapfold
open Types
open Clocks
open Static
open Initial
@ -361,7 +361,7 @@ let empty_call_context = None
[v] var decs *)
let rec translate_eq map call_context { Minils.eq_lhs = pat; Minils.eq_rhs = e }
(v, si, j, s) =
let { Minils.e_desc = desc; Minils.e_ck = ck; Minils.e_loc = loc } = e in
let { Minils.e_desc = desc; Minils.e_base_ck = ck; Minils.e_loc = loc } = e in
match (pat, desc) with
| Minils.Evarpat n, Minils.Efby (opt_c, e) ->
let x = var_from_name map n in

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

@ -8,9 +8,19 @@
(**************************************************************************)
(* clock checking *)
(* v_clock is expected to contain correct clocks before entering here :
either explicit with Cbase representing the node activation clock
or fresh_clock() for unannoted variables.
Idem for e_ct : if explicit, it represents a clock annotation.
Unification is done on this mutable fields.
e_base_ck is set according to node signatures.
*)
open Misc
open Idents
open Minils
open Global_printer
open Mls_printer
open Signature
open Types
@ -19,139 +29,152 @@ open Location
open Format
(** Error Kind *)
type error_kind = | Etypeclash of ct * ct
type error_kind = | Etypeclash of ct * ct | Eclockclash of ck * ck | Edefclock
let error_message loc = function
| Etypeclash (actual_ct, expected_ct) ->
Format.eprintf "%aClock Clash: this expression has clock %a,@\n\
but is expected to have clock %a.@."
print_location loc
print_clock actual_ct
print_clock expected_ct;
print_ct actual_ct
print_ct expected_ct;
raise Errors.Error
| Eclockclash (actual_ck, expected_ck) ->
Format.eprintf "%aClock Clash: this value has clock %a,@\n\
but is exprected to have clock %a.@."
print_location loc
print_ck actual_ck
print_ck expected_ck;
raise Errors.Error
| Edefclock ->
Format.eprintf "%aArguments defining clocks should be given as names@."
print_location loc;
raise Errors.Error
let typ_of_name h x = Env.find x h
let ck_of_name h x = Env.find x h
let rec typing_extvalue h w =
let ct = match w.w_desc with
| Wconst se -> skeleton (fresh_clock ()) se.se_ty
| Wvar x -> Ck (typ_of_name h x)
let ck = match w.w_desc with
| Wconst se -> fresh_clock()
| Wvar x -> ck_of_name h x
| Wwhen (w1, c, n) ->
let ck_n = typ_of_name h n in
(expect h (skeleton ck_n w1.w_ty) w1; skeleton (Con (ck_n, c, n)) w1.w_ty)
let ck_n = ck_of_name h n in
expect_extvalue h ck_n w1;
Con (ck_n, c, n)
| Wfield (w1, f) ->
let ck = fresh_clock () in
let ct = skeleton ck w1.w_ty in (expect h (Ck ck) w1; ct)
in (w.w_ck <- ckofct ct; ct)
typing_extvalue h w1
in
w.w_ck <- ck;
ck
and expect h expected_ty e =
let actual_ty = typing_extvalue h e in
try unify actual_ty expected_ty
and expect_extvalue h expected_ck e =
let actual_ck = typing_extvalue h e in
try unify_ck actual_ck expected_ck
with
| Unify -> eprintf "%a : " print_extvalue e;
error_message e.w_loc (Etypeclash (actual_ty, expected_ty))
error_message e.w_loc (Eclockclash (actual_ck, expected_ck))
let rec typing h e =
let ct = match e.e_desc with
| Eextvalue w -> typing_extvalue h w
| Efby (_, e) -> typing_extvalue h e
| Eapp({a_op = op}, args, r) ->
let ck = match r with
| None -> fresh_clock ()
| Some(reset) -> typ_of_name h reset in
typing_op op args h e ck
(* Typed exactly as a fun or a node... *)
| Eiterator (_, _, _, pargs, args, r) ->
let ck = match r with
| None -> fresh_clock()
| Some(reset) -> typ_of_name h reset
in
List.iter (expect h (Ck ck)) pargs;
List.iter (expect h (Ck ck)) args;
skeleton ck e.e_ty
| Emerge (n, c_e_list) ->
let ck_c = typ_of_name h n in
(typing_c_e_list h ck_c n c_e_list; skeleton ck_c e.e_ty)
let rec typing_pat h = function
| Evarpat x -> Ck (ck_of_name h x)
| Etuplepat pat_list -> Cprod (List.map (typing_pat h) pat_list)
let typing_app h base pat op w_list = match op with
| Earray_fill | Eselect | Eselect_dyn | Eselect_trunc | Eupdate | Eequal
| Eselect_slice | Econcat | Earray | Efield_update | Eifthenelse ->
List.iter (expect_extvalue h base) w_list;
Ck base
| ( 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
| [],[] -> env
| a::a_l, v::v_l -> (match a.a_name with
| None -> build_env a_l v_l env
| Some n -> build_env a_l v_l ((n,v)::env))
| _ -> Misc.internal_error "Clocking, non matching signature" 2
in
let env_pat = build_env node.node_outputs pat_id_list [] in
let env_args = build_env node.node_inputs w_list [] in
(* implement with Cbase as base, replace name dep by ident dep *)
let rec sigck_to_ck sck = match sck with
| Signature.Cbase -> base
| Signature.Con (sck,c,x) ->
(* find x in the envs : *)
let id = try List.assoc x env_pat
with Not_found ->
try
let w = List.assoc x env_args in
(match w.w_desc with
| Wvar id -> id
| _ -> error_message w.w_loc Edefclock)
with Not_found ->
Misc.internal_error "Clocking, non matching signature" 3
in
Clocks.Con (sigck_to_ck sck, c, id)
in
List.iter2 (fun a w -> expect_extvalue h (sigck_to_ck a.a_clock) w) node.node_inputs w_list;
Clocks.prod (List.map (fun a -> sigck_to_ck a.a_clock) node.node_outputs)
let typing_eq h { eq_lhs = pat; eq_rhs = e } =
(* typing the expression *)
let ct,base = match e.e_desc with
| Eextvalue w
| Efby (_, w) ->
let ck = typing_extvalue h w in
Ck ck, ck
| Emerge (x, c_e_list) ->
let ck = ck_of_name h x in
List.iter (fun (c,e) -> expect_extvalue h (Con (ck,c,x)) e) c_e_list;
Ck ck, ck
| Estruct l ->
let ck = fresh_clock () in
(List.iter
(fun (_, e) -> let ct = skeleton ck e.w_ty in expect h ct e) l;
Ck ck)
in (e.e_ck <- ckofct ct; ct)
List.iter (fun (_, e) -> expect_extvalue h ck e) l;
Ck ck, ck
| Eapp({a_op = op}, args, r) ->
let ck_r = match r with
| None -> fresh_clock ()
| Some(reset) -> ck_of_name h reset in
let ct = typing_app h ck_r pat op args in
ct, ck_r
| Eiterator (_, _, _, pargs, args, r) ->
(* Typed exactly as a fun or a node... *)
let ck_r = match r with
| None -> fresh_clock()
| Some(reset) -> ck_of_name h reset
in
List.iter (expect_extvalue h ck_r) pargs;
List.iter (expect_extvalue h ck_r) args;
(*TODO*)
Ck ck_r, ck_r
in
e.e_base_ck <- base;
begin
try unify ct e.e_ct
with Unify ->
eprintf "Incoherent clock annotation.@\n";
error_message e.e_loc (Etypeclash (ct,e.e_ct))
end;
e.e_ct <- ct;
(* typing the full equation *)
let pat_ct = typing_pat h pat in
begin
try unify ct pat_ct
with Unify ->
eprintf "Incoherent clock between right and left side of the equation@\n";
error_message e.e_loc (Etypeclash (ct, pat_ct))
end
and typing_op op e_list h e ck = match op with
| (Eequal | Efun _ | Enode _) -> (*LA*)
List.iter (fun e -> expect h (skeleton ck e.w_ty) e) e_list;
skeleton ck e.e_ty
| Eifthenelse ->
let e1, e2, e3 = assert_3 e_list in
let ct = skeleton ck e.e_ty
in (expect h (Ck ck) e1; expect h ct e2; expect h ct e3; ct)
| Efield_update ->
let e1, e2 = assert_2 e_list in
let ct = skeleton ck e.e_ty
in (expect h (Ck ck) e1; expect h ct e2; ct)
| Earray ->
(List.iter (expect h (Ck ck)) e_list; skeleton ck e.e_ty)
| Earray_fill -> let e = assert_1 e_list in typing_extvalue h e
| Eselect -> let e = assert_1 e_list in typing_extvalue h e
| Eselect_dyn -> (* TODO defe not treated ? *)
let e1, defe, idx = assert_2min e_list in
let ct = skeleton ck e1.w_ty
in (List.iter (expect h ct) (e1::defe::idx); ct)
| Eselect_trunc ->
let e1, idx = assert_1min e_list in
let ct = skeleton ck e1.w_ty
in (List.iter (expect h ct) (e1::idx); ct)
| Eupdate ->
let e1, e2, idx = assert_2min e_list in
let ct = skeleton ck e.e_ty
in (expect h (Ck ck) e1; expect h ct e2; List.iter (expect h ct) idx; ct)
| Eselect_slice -> let e = assert_1 e_list in typing_extvalue h e
| Econcat ->
let e1, e2 = assert_2 e_list in
let ct = skeleton ck e.e_ty
in (expect h (Ck ck) e1; expect h ct e2; ct)
and typing_c_e_list h ck_c n c_e_list =
let rec typrec =
function
| [] -> ()
| (c, e) :: c_e_list ->
(expect h (skeleton (Con (ck_c, c, n)) e.w_ty) e; typrec c_e_list)
in typrec c_e_list
let typing_eqs h eq_list = List.iter (typing_eq h) eq_list
let expect_exp h expected_ty e =
let actual_ty = typing h e in
try unify actual_ty expected_ty
with
| Unify -> eprintf "%a : " print_exp e;
error_message e.e_loc (Etypeclash (actual_ty, expected_ty))
let append_env h vds =
List.fold_left (fun h { v_ident = n; v_clock = ck } -> Env.add n ck h) h vds
let rec typing_pat h =
function
| Evarpat x -> Ck (typ_of_name h x)
| Etuplepat pat_list -> Cprod (List.map (typing_pat h) pat_list)
let typing_eqs h eq_list = (*TODO FIXME*)
let typing_eq { eq_lhs = pat; eq_rhs = e } =
let ty_pat = typing_pat h pat in
(try expect_exp h ty_pat e with
| Errors.Error -> (* DEBUG *)
Format.eprintf "Complete expression: %a@\nClock pattern: %a@."
Mls_printer.print_exp e
Mls_printer.print_clock ty_pat;
raise Errors.Error)
in List.iter typing_eq eq_list
let build h dec =
List.fold_left (fun h { v_ident = n } -> Env.add n (fresh_clock ()) h) h dec
let sbuild h dec base =
List.fold_left (fun h { v_ident = n } -> Env.add n base h) h dec
let typing_contract h contract base =
let typing_contract h contract =
match contract with
| None -> h
| Some { c_local = l_list;
@ -159,32 +182,25 @@ let typing_contract h contract base =
c_assume = e_a;
c_enforce = e_g;
c_controllables = c_list } ->
let h' = build h l_list in
let h' = append_env h l_list in
(* assumption *)
(* property *)
typing_eqs h' eq_list;
expect_exp h' (Ck base) e_a;
expect_exp h' (Ck base) e_g;
sbuild h c_list base
expect_extvalue h' Cbase e_a;
expect_extvalue h' Cbase e_g;
append_env h c_list
let typing_node ({ n_input = i_list;
n_output = o_list;
n_contract = contract;
n_local = l_list;
n_equs = eq_list
} as node) =
let base = Cbase in
let h = sbuild Env.empty i_list base in
let h = sbuild h o_list base in
let h = typing_contract h contract base in
let h = build h l_list in
(typing_eqs h eq_list;
(*update clock info in variables descriptions *)
let set_clock vd = { vd with v_clock = ck_repr (Env.find vd.v_ident h) } in
{ (node) with
n_input = List.map set_clock i_list;
n_output = List.map set_clock o_list;
n_local = List.map set_clock l_list })
let typing_node node =
let h = append_env Env.empty node.n_input in
let h = append_env h node.n_output in
let h = typing_contract h node.n_contract in
let h = append_env h node.n_local in
(typing_eqs h node.n_equs;
(*update clock info in variables descriptions *)
let set_clock vd = { vd with v_clock = ck_repr (Env.find vd.v_ident h) } in
{ node with n_input = List.map set_clock node.n_input;
n_output = List.map set_clock node.n_output;
n_local = List.map set_clock node.n_local })
let program p =
let program_desc pd = match pd with

23
compiler/minils/minils.ml
View file

@ -46,16 +46,18 @@ and extvalue = {
w_loc : location }
and extvalue_desc =
| Wconst of static_exp
| Wconst of static_exp (*no tuple*)
| Wvar of var_ident
| Wfield of extvalue * field_name
| Wwhen of extvalue * constructor_name * var_ident (** extvalue when Constructor(ident) *)
and exp = {
e_desc : edesc;
mutable e_ck: ck;
e_ty : ty;
e_loc : location }
e_desc : edesc;
e_level_ck : ck; (* when no data dep, execute the exp on this clock (set by [switch] *)
mutable e_base_ck : ck;
mutable e_ct : ct;
e_ty : ty;
e_loc : location }
and edesc =
| Eextvalue of extvalue
@ -107,8 +109,8 @@ type var_dec = {
v_loc : location }
type contract = {
c_assume : exp;
c_enforce : exp;
c_assume : extvalue;
c_enforce : extvalue;
c_controllables : var_dec list;
c_local : var_dec list;
c_eq : eq list }
@ -119,8 +121,6 @@ type node_dec = {
n_input : var_dec list;
n_output : var_dec list;
n_contract : contract option;
(* GD: inglorious hack for controller call
mutable n_controller_call : var_ident list * var_ident list; *)
n_local : var_dec list;
n_equs : eq list;
n_loc : location;
@ -150,9 +150,8 @@ let mk_extvalue ~ty ?(clock = fresh_clock()) ?(loc = no_location) desc =
{ w_desc = desc; w_ty = ty;
w_ck = clock; w_loc = loc }
let mk_exp ty ?(clock = fresh_clock()) ?(loc = no_location) desc =
{ e_desc = desc; e_ty = ty;
e_ck = clock; e_loc = loc }
let mk_exp level_ck ty ?(ck = Cbase) ?(ct = fresh_ct ty) ?(loc = no_location) desc =
{ e_desc = desc; e_ty = ty; e_level_ck = level_ck; e_base_ck = ck; e_ct = ct; e_loc = loc }
let mk_var_dec ?(loc = no_location) ?(clock = fresh_clock()) ident ty =
{ v_ident = ident; v_type = ty; v_clock = clock; v_loc = loc }

4
compiler/minils/mls_mapfold.ml
View file

@ -136,8 +136,8 @@ and var_decs funs acc vds = mapfold (var_dec_it funs) acc vds
and contract_it funs acc c = funs.contract funs acc c
and contract funs acc c =
let c_assume, acc = exp_it funs acc c.c_assume in
let c_enforce, acc = exp_it funs acc c.c_enforce in
let c_assume, acc = extvalue_it funs acc c.c_assume in
let c_enforce, acc = extvalue_it funs acc c.c_enforce in
let c_local, acc = var_decs_it funs acc c.c_local in
let c_eq, acc = eqs_it funs acc c.c_eq in
{ c with

16
compiler/minils/mls_printer.ml
View file

@ -1,11 +1,11 @@
open Misc
open Names
open Signature
open Idents
open Types
open Clocks
open Static
open Format
open Signature
open Global_printer
open Pp_tools
open Minils
@ -27,7 +27,7 @@ let rec print_pat ff = function
| Evarpat n -> print_ident ff n
| Etuplepat pat_list ->
fprintf ff "@[<2>(%a)@]" (print_list_r print_pat """,""") pat_list
(*
let rec print_ck ff = function
| Cbase -> fprintf ff "base"
| Con (ck, c, n) ->
@ -35,11 +35,11 @@ let rec print_ck ff = function
| Cvar { contents = Cindex _ } -> fprintf ff "base"
| Cvar { contents = Clink ck } -> print_ck ff ck
let rec print_clock ff = function
let rec print_ct ff = function
| Ck ck -> print_ck ff ck
| Cprod ct_list ->
fprintf ff "@[<2>(%a)@]" (print_list_r print_clock """ *""") ct_list
*)
let print_vd ff { v_ident = n; v_type = ty; v_clock = ck } =
if !Compiler_options.full_type_info then
fprintf ff "%a : %a :: %a" print_ident n print_type ty print_ck ck
@ -86,7 +86,7 @@ and print_trunc_index ff idx =
and print_exp ff e =
if !Compiler_options.full_type_info then
fprintf ff "(%a : %a :: %a)"
print_exp_desc e.e_desc print_type e.e_ty print_ck e.e_ck
print_exp_desc e.e_desc print_type e.e_ty print_ct e.e_ct
else fprintf ff "%a" print_exp_desc e.e_desc
and print_every ff reset =
@ -180,7 +180,7 @@ and print_tag_w_list ff tag_w_list =
and print_eq ff { eq_lhs = p; eq_rhs = e } =
if !Compiler_options.full_type_info
then fprintf ff "@[<2>%a :: %a =@ %a@]"
print_pat p print_ck e.e_ck print_exp e
print_pat p print_ck e.e_base_ck print_exp e
else fprintf ff "@[<2>%a =@ %a@]" print_pat p print_exp e
@ -207,8 +207,8 @@ let print_contract ff { c_local = l; c_eq = eqs;
fprintf ff "@[<v2>contract@\n%a%a@ assume %a@ enforce %a@ with (%a)@]"
print_local_vars l
print_eqs eqs
print_exp e_a
print_exp e_g
print_extvalue e_a
print_extvalue e_g
print_vd_tuple c

22
compiler/minils/mls_utils.ml
View file

@ -46,10 +46,6 @@ let rec vd_mem n = function
| [] -> false
| vd::l -> vd.v_ident = n or (vd_mem n l)
(** @return a signature arguments from the vardecs *)
let args_of_var_decs vds =
List.map (fun vd -> Signature.mk_arg (Some (name vd.v_ident)) vd.v_type) vds
(** @return whether [ty] corresponds to a record type. *)
let is_record_type ty = match ty with
@ -77,6 +73,10 @@ struct
| Cbase | Cvar { contents = Cindex _ } -> acc
| Cvar { contents = Clink ck } -> vars_ck acc ck
let rec vars_ct acc = function
| Ck ck -> vars_ck acc ck
| Cprod c_l -> List.fold_left vars_ct acc c_l
let read_extvalue read_funs (is_left, acc_init) w =
(* recursive call *)
let _,(_, acc) = Mls_mapfold.extvalue read_funs (is_left, acc_init) w in
@ -104,7 +104,7 @@ struct
else acc
| _ -> acc
in
e, (is_left, vars_ck acc e.e_ck)
e, (is_left, vars_ct acc e.e_ct)
let read_exp is_left acc e =
let _, (_, acc) =
@ -136,9 +136,7 @@ struct
let antidep { eq_rhs = e } =
match e.e_desc with Efby _ -> true | _ -> false
let clock { eq_rhs = e } = match e.e_desc with
| Emerge(_, (_, e) :: _) -> e.w_ck
| _ -> e.e_ck
let clock { eq_rhs = e } = e.e_base_ck
let head ck =
let rec headrec ck l =
@ -191,3 +189,11 @@ module AllDep = Dep.Make
let eq_find id = List.find (fun eq -> List.mem id (Vars.def [] eq))
let ident_list_of_pat pat =
let rec f acc pat = match pat with
| Evarpat id -> id::acc
| Etuplepat [] -> acc
| Etuplepat (pat::pat_l) -> f (f acc pat) (Etuplepat pat_l)
in
f [] pat

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

@ -22,8 +22,9 @@ let eq _ (outputs, eqs, env) eq = match eq.eq_lhs, eq.eq_rhs.e_desc with
| Evarpat x, Efby _ ->
if Mls_utils.vd_mem x outputs then
let ty = eq.eq_rhs.e_ty in
let ck = eq.eq_rhs.e_base_ck in
let x_copy = Idents.gen_var "normalize_mem" ("out_"^(Idents.name x)) in
let exp_x = mk_exp ty (Eextvalue (mk_extvalue ~ty:ty (Wvar x))) in
let exp_x = mk_exp ck ty (Eextvalue (mk_extvalue ~ty:ty (Wvar x))) in
let eq_copy = { eq with eq_lhs = Evarpat x_copy; eq_rhs = exp_x } in
let env = Env.add x x_copy env in
eq, (outputs, eq::eq_copy::eqs, env)