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

Revert "Fixed problem in clocking" e3676d1e3c

Browse source 
Fixing the actual bug :
* static_exp should not be created without type
after or during the typing pass.
This commit is contained in:
Léonard Gérard 2010-08-03 22:38:42 +02:00
parent 79c4e2a581
commit 4b3c3ba8b5
13 changed files with 65 additions and 50 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
compiler/global/clocks.ml
View file

@ -95,9 +95,9 @@ let rec skeleton ck = function
| Tprod ty_list -> Cprod (List.map (skeleton ck) ty_list)
| Tarray _ | Tid _ -> Ck ck
let rec const_skeleton se = match se.se_desc with
| Stuple se_list -> Cprod (List.map const_skeleton se_list)
| _ -> Ck (new_var ())
let rec const_skeleton ck se = match se.se_desc with
| Stuple se_list -> Cprod (List.map (const_skeleton ck) se_list)
| _ -> Ck ck
let ckofct = function | Ck ck -> ck_repr ck | Cprod ct_list -> Cbase

12
compiler/global/initial.ml
View file

@ -9,6 +9,7 @@
(* initialization of the typing environment *)
open Names
open Types
let tglobal = []
let cglobal = []
@ -22,6 +23,17 @@ let pfloat = Modname({ qual = "Pervasives"; id = "float" })
let mk_pervasives s = Modname({ qual = "Pervasives"; id = s })
let mk_static_int_op op args =
mk_static_exp ~ty:(Tid pint) (Sop (op,args))
let mk_static_int i =
mk_static_exp ~ty:(Tid pint) (Sint i)
let mk_static_bool b =
mk_static_exp ~ty:(Tid pbool) (Sbool b)
(* build the initial environment *)
let initialize () =
List.iter (fun (f, ty) -> Modules.add_type f ty) tglobal;

3
compiler/global/types.ml
View file

@ -34,11 +34,10 @@ let prod = function
| [ty] -> ty
| ty_list -> Tprod ty_list
(** DO NOT use this after the typing, since it gives invalid_type *)
let mk_static_exp ?(loc = no_location) ?(ty = invalid_type) desc =
{ se_desc = desc; se_ty = ty; se_loc = loc }
let static_exp_of_int i =
mk_static_exp (Sint i)
open Pp_tools
open Format

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

@ -9,8 +9,6 @@
(* causality check *)
(* $Id: causality.ml 615 2009-11-20 17:43:14Z pouzet $ *)
open Misc
open Names
open Idents

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

@ -477,7 +477,7 @@ and typing_static_exp const_env se =
let typed_se, ty = typing_static_exp const_env se in
let typed_se_list = List.map (expect_static_exp const_env ty) se_list in
Sarray (typed_se::typed_se_list),
Tarray(ty, mk_static_exp (Sint ((List.length se_list) + 1)))
Tarray(ty, mk_static_int ((List.length se_list) + 1))
| Stuple se_list ->
let typed_se_list, ty_list = List.split
(List.map (typing_static_exp const_env) se_list) in
@ -596,7 +596,7 @@ let rec typing const_env h e =
(* add size constraints *)
let size_constrs =
instanciate_constr m ty_desc.node_params_constraints in
add_size_constraint (Clequal (mk_static_exp (Sint 1), typed_n));
add_size_constraint (Clequal (mk_static_int 1, typed_n));
List.iter add_size_constraint size_constrs;
(* return the type *)
Eiterator(it, { app with a_op = op; a_params = typed_params }
@ -666,8 +666,7 @@ and typing_app const_env h op e_list =
| { a_op = Earray }, exp::e_list ->
let typed_exp, t1 = typing const_env h exp in
let typed_e_list = List.map (expect const_env h t1) e_list in
let n = mk_static_exp ~ty:(Tid Initial.pint)
(Sint (List.length e_list + 1)) in
let n = mk_static_int (List.length e_list + 1) in
Tarray(t1, n), op, typed_exp::typed_e_list
| { a_op = Efield; a_params = [f] }, [e] ->
@ -698,7 +697,7 @@ and typing_app const_env h op e_list =
| { a_op = Earray_fill; a_params = [n] }, [e1] ->
let typed_n = expect_static_exp const_env (Tid Initial.pint) n in
let typed_e1, t1 = typing const_env h e1 in
add_size_constraint (Clequal (mk_static_exp (Sint 1), typed_n));
add_size_constraint (Clequal (mk_static_int 1, typed_n));
Tarray (t1, typed_n), { op with a_params = [typed_n] }, [typed_e1]
| { a_op = Eselect; a_params = idx_list }, [e1] ->
@ -726,11 +725,11 @@ and typing_app const_env h op e_list =
let typed_idx2 = expect_static_exp const_env (Tid Initial.pint) idx2 in
let typed_e, t1 = typing const_env h e in
(*Create the expression to compute the size of the array *)
let e1 = mk_static_exp (Sop (mk_pervasives "-",
[typed_idx2; typed_idx1])) in
let e2 = mk_static_exp (Sop (mk_pervasives "+",
[e1;mk_static_exp (Sint 1) ])) in
add_size_constraint (Clequal (mk_static_exp (Sint 1), e2));
let e1 =
mk_static_int_op (mk_pervasives "-") [typed_idx2; typed_idx1] in
let e2 =
mk_static_int_op (mk_pervasives "+") [e1;mk_static_int 1 ] in
add_size_constraint (Clequal (mk_static_int 1, e2));
Tarray (element_type t1, e2),
{ op with a_params = [typed_idx1; typed_idx2] }, [typed_e]
@ -742,8 +741,8 @@ and typing_app const_env h op e_list =
with
TypingError(kind) -> message e1.e_loc kind
end;
let n = mk_static_exp (Sop (mk_pervasives "+",
[array_size t1; array_size t2])) in
let n =
mk_static_int_op (mk_pervasives "+") [array_size t1; array_size t2] in
Tarray (element_type t1, n), op, [typed_e1; typed_e2]
(*Arity problems*)
@ -823,13 +822,13 @@ and typing_array_subscript const_env h idx_list ty =
| Tarray(ty, exp), idx::idx_list ->
ignore (expect_static_exp const_env (Tid Initial.pint) exp);
let typed_idx = expect_static_exp const_env (Tid Initial.pint) idx in
add_size_constraint (Clequal (mk_static_exp (Sint 0), idx));
let bound = mk_static_exp (Sop(mk_pervasives "-",
[exp; mk_static_exp (Sint 1)])) in
add_size_constraint (Clequal (idx,bound));
let typed_idx_list, ty =
typing_array_subscript const_env h idx_list ty in
typed_idx::typed_idx_list, ty
add_size_constraint (Clequal (mk_static_int 0, idx));
let bound =
mk_static_int_op (mk_pervasives "-") [exp; mk_static_int 1] in
add_size_constraint (Clequal (idx,bound));
let typed_idx_list, ty =
typing_array_subscript const_env h idx_list ty in
typed_idx::typed_idx_list, ty
| _, _ -> error (Esubscripted_value_not_an_array ty)
(* This function checks that the array dimensions matches

9
compiler/heptagon/heptagon.ml
View file

@ -14,6 +14,7 @@ open Idents
open Static
open Signature
open Types
open Initial
type state_name = name
@ -175,12 +176,8 @@ let mk_block ?(statefull = true) ?(defnames = Env.empty) eqs =
{ b_local = []; b_equs = eqs; b_defnames = defnames;
b_statefull = statefull; b_loc = no_location }
let dfalse =
mk_exp (Econst (mk_static_exp (Sconstructor Initial.pfalse)))
(Tid Initial.pbool)
let dtrue =
mk_exp (Econst (mk_static_exp (Sconstructor Initial.ptrue)))
(Tid Initial.pbool)
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] }

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

@ -14,6 +14,7 @@ open Names
open Idents
open Heptagon
open Hept_mapfold
open Initial
let mk_var_exp n ty =
mk_exp (Evar n) ty
@ -28,11 +29,15 @@ let mk_switch_equation e l =
mk_equation (Eswitch (e, l))
let mk_exp_fby_false e =
mk_exp (Epre (Some (mk_static_exp (Sconstructor Initial.pfalse)), e))
mk_exp (Epre (Some (mk_static_bool false), e))
(Tid Initial.pbool)
let mk_constructor constr ty =
mk_static_exp ~ty:ty (Sconstructor constr)
(* Be sure that [initial] is of the right type [e.e_ty] before using this *)
let mk_exp_fby_state initial e =
{ e with e_desc = Epre (Some (mk_static_exp (Sconstructor initial)), e) }
{ e with e_desc = Epre (Some (mk_constructor initial e.e_ty), e) }
(* the list of enumerated types introduced to represent states *)
let state_type_dec_list = ref []
@ -71,8 +76,8 @@ let translate_automaton v eq_list handlers =
let pre_next_resetname = Idents.fresh "pnr" in
let name n = Name(NamesEnv.find n states) in
let state n = mk_exp (Econst (mk_static_exp
(Sconstructor (name n)))) tstatetype in
let state n =
mk_exp (Econst (mk_constructor (name n) tstatetype)) tstatetype in
let statevar n = mk_var_exp n tstatetype in
let boolvar n = mk_var_exp n (Tid Initial.pbool) in

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

@ -14,6 +14,7 @@ open Idents
open Heptagon
open Hept_mapfold
open Types
open Initial
(* We introduce an initialization variable for each block *)
(* Using an asynchronous reset would allow to produce *)
@ -52,8 +53,7 @@ let mk_bool_param n =
let or_op_call e_list = mk_op_app (Efun Initial.por) e_list
let pre_true e =
{ e with e_desc = Epre (Some (mk_static_exp ~ty:(Tid Initial.pbool)
(Sconstructor Initial.ptrue)), e) }
{ e with e_desc = Epre (Some (mk_static_bool true), e) }
let init e = pre_true { dfalse with e_loc = e.e_loc }
let add_resets res e =

2
compiler/main/hept2mls.ml
View file

@ -178,7 +178,7 @@ let switch x ci_eqs_list =
| [] | (_, []) :: _ -> []
| (ci, (y, { e_ty = ty; e_loc = loc }) :: _) :: _ ->
let ci_e_list, ci_eqs_list = split ci_eqs_list in
(y, mk_exp ~exp_ty:ty (Emerge(x, ci_e_list))) ::
(y, mk_exp ~exp_ty:ty ~loc:loc (Emerge(x, ci_e_list))) ::
distribute ci_eqs_list in
check ci_eqs_list;

19
compiler/main/mls2obc.ml
View file

@ -17,6 +17,11 @@ open Types
open Control
open Static
open Obc_mapfold
open Initial
(** Not giving any type and called after typing, DO NOT use it anywhere else *)
let static_exp_of_int i =
Types.mk_static_exp (Types.Sint i)
let gen_obj_name n =
(shortname n) ^ "_mem" ^ (gen_symbol ())
@ -197,13 +202,11 @@ let rec translate_eq map call_context { Minils.eq_lhs = pat; Minils.eq_rhs = e }
[mk_evar cpt;
mk_exp (Econst idx1) ])) in
(* bound = (idx2 - idx1) + 1*)
let bound =
mk_static_exp (Sop(op_from_string "+",
[ mk_static_exp (Sint 1);
mk_static_exp (Sop (op_from_string "-",
[idx2;idx1])) ])) in
let bound = mk_static_int_op (op_from_string "+")
[ mk_static_int 1;
mk_static_int_op (op_from_string "-") [idx2;idx1] ] in
let action =
Afor (cpt, mk_static_exp (Sint 0), bound,
Afor (cpt, mk_static_int 0, bound,
mk_block [Aassgn (mk_lhs (Larray (var_from_name map x,
mk_evar cpt)),
mk_lhs_exp (Larray (lhs_of_exp e, idx)))] )
@ -242,7 +245,7 @@ let rec translate_eq map call_context { Minils.eq_lhs = pat; Minils.eq_rhs = e }
Minils.a_params = [n] }, [e], _) ->
let cpt = Idents.fresh "i" in
let action =
Afor (cpt, mk_static_exp (Sint 0), n,
Afor (cpt, mk_static_int 0, n,
mk_block [Aassgn (mk_lhs (Larray (var_from_name map x,
mk_evar cpt)),
translate map (si, j, s) e) ])
@ -259,7 +262,7 @@ let rec translate_eq map call_context { Minils.eq_lhs = pat; Minils.eq_rhs = e }
let e1 = translate map (si, j, s) e1 in
let e2 = translate map (si, j, s) e2 in
let a1 =
Afor (cpt1, mk_static_exp (Sint 0), n1,
Afor (cpt1, mk_static_int 0, n1,
mk_block [Aassgn (mk_lhs (Larray (x, mk_evar cpt1)),
mk_lhs_exp (Larray (lhs_of_exp e1,
mk_evar cpt1)))] ) in

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

@ -35,7 +35,7 @@ let typ_of_name h x = Env.find x h
let rec typing h e =
let ct = match e.e_desc with
| Econst se -> const_skeleton se
| Econst se -> skeleton (new_var ()) se.se_ty
| Evar x -> Ck (typ_of_name h x)
| Efby (c, e) -> typing h e
| Eapp({a_op = op}, args, r) ->
@ -94,7 +94,7 @@ and expect h expected_ty e =
let actual_ty = typing h e in
try unify actual_ty expected_ty
with
| Unify -> eprintf "e %a : " print_exp e;
| Unify -> eprintf "%a : " print_exp e;
error_message e.e_loc (Etypeclash (actual_ty, expected_ty))
and typing_c_e_list h ck_c n c_e_list =

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

@ -14,7 +14,7 @@ let pp p = if !verbose then Mls_printer.print stdout p
let compile pp p =
(* Clocking *)
let p = do_pass Clocking.program "Clocking" p pp false in
let p = do_pass Clocking.program "Clocking" p pp true in
(* Check that the dataflow code is well initialized *)
(*let p = do_silent_pass Init.program "Initialization check" p !init in *)

2
compiler/minils/parsing/mls_parser.mly
View file

@ -147,9 +147,11 @@ constructor: /* of type longname */
| ln=qualified(CONSTRUCTOR) { ln }
| b=BOOL { Name(if b then "true" else "false") }
/* TODO donner un type !! Phase de typing. */
field:
| ln=longname { mk_static_exp ~loc:(Loc($startpos,$endpos)) (Sconstructor ln)}
/* TODO donner un type !! Phase de typing. */
const : c=_const { mk_static_exp ~loc:(Loc ($startpos,$endpos)) c }
_const:
| i=INT { Sint i }