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

Init is missing all the array stuff, and Ecall is strange, with an issue when reset an op, and a different treatment of op and node.

Browse source
This commit is contained in:
Léonard Gérard 2010-06-18 11:51:52 +02:00
parent ac0066a3d4
commit a20b30909c
1 changed files with 238 additions and 235 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

335
minils/analysis/init.ml
View file

@ -6,7 +6,6 @@
(* Organization : Demons, LRI, University of Paris-Sud, Orsay *) (* Organization : Demons, LRI, University of Paris-Sud, Orsay *)
(* *) (* *)
(**************************************************************************) (**************************************************************************)
(* simple initialization analysis. This is almost trivial since *) (* simple initialization analysis. This is almost trivial since *)
(* input/outputs of a node are forced to be initialized *) (* input/outputs of a node are forced to be initialized *)
(* add a special treatment of clock state variables whose initial *) (* add a special treatment of clock state variables whose initial *)
@ -15,300 +14,304 @@
(* if [clock c = C fby ec] then [merge c (C -> e) ...] is initialized *) (* if [clock c = C fby ec] then [merge c (C -> e) ...] is initialized *)
(* if [e] is initialized only *) (* if [e] is initialized only *)
(* $Id: init.ml 615 2009-11-20 17:43:14Z pouzet $ *)
open Misc open Misc
open Names open Names
open Ident open Ident
open Minils open Minils
open Location open Location
open Format open Format
open Types
type typ = type typ = | Iproduct of typ list | Ileaf of init
| Iproduct of typ list
| Ileaf of init
and init = and init = { mutable i_desc : init_desc; mutable i_index : int}
{ mutable i_desc: init_desc;
mutable i_index: int }
and init_desc = and init_desc = | Izero | Ione | Ivar | Imax of init * init | Ilink of init
| Izero
| Ione
| Ivar
| Imax of init * init
| Ilink of init
type typ_env = type typ_env =
{ t_init: init; (* its initialisation type *) { t_init : init; (* its initialisation type *) t_value : longname option }
t_value: longname option; (* its initial value *)
}
(* its initial value *)
(* typing errors *) (* typing errors *)
exception Unify exception Unify
let index = ref 0 let index = ref 0
let gen_index () = incr index; !index
let new_var () = { i_desc = Ivar; i_index = gen_index () } let gen_index () = (incr index; !index)
let izero = { i_desc = Izero; i_index = gen_index () }
let ione = { i_desc = Ione; i_index = gen_index () } let new_var () = { i_desc = Ivar; i_index = gen_index (); }
let imax i1 i2 = { i_desc = Imax(i1, i2); i_index = gen_index () }
let product l = Iproduct(l) let izero = { i_desc = Izero; i_index = gen_index (); }
let leaf i = Ileaf(i)
let ione = { i_desc = Ione; i_index = gen_index (); }
let imax i1 i2 = { i_desc = Imax (i1, i2); i_index = gen_index (); }
let product l = Iproduct l
let leaf i = Ileaf i
(* basic operation on initialization values *) (* basic operation on initialization values *)
let rec irepr i = let rec irepr i =
match i.i_desc with match i.i_desc with
| Ilink(i_son) -> | Ilink i_son ->
let i_son = irepr i_son in let i_son = irepr i_son in (i.i_desc <- Ilink i_son; i_son)
i.i_desc <- Ilink(i_son);
i_son
| _ -> i | _ -> i
(** Simplification rules for max. Nothing fancy here *) (** Simplification rules for max. Nothing fancy here *)
let max i1 i2 = let max i1 i2 =
let i1 = irepr i1 in let i1 = irepr i1 in
let i2 = irepr i2 in let i2 = irepr i2
match i1.i_desc, i2.i_desc with in
match ((i1.i_desc), (i2.i_desc)) with
| (Izero, Izero) -> izero | (Izero, Izero) -> izero
| (Izero, _) -> i2 | (Izero, _) -> i2
| (_, Izero) -> i1 | (_, Izero) -> i1
| (_, Ione) | (Ione, _) -> ione | (_, Ione) | (Ione, _) -> ione
| _ -> imax i1 i2 | _ -> imax i1 i2
let rec itype = function let rec itype =
| Iproduct(ty_list) -> itype_list ty_list function | Iproduct ty_list -> itype_list ty_list | Ileaf i -> i
| Ileaf(i) -> i
and itype_list ty_list = and itype_list ty_list =
List.fold_left (fun acc ty -> max acc (itype ty)) izero ty_list List.fold_left (fun acc ty -> max acc (itype ty)) izero ty_list
(* saturate an initialization type. Every element must be initialized *) (* saturate an initialization type. Every element must be initialized *)
let rec initialized i = let rec initialized i =
let i = irepr i in let i = irepr i
in
match i.i_desc with match i.i_desc with
| Izero -> () | Izero -> ()
| Ivar -> i.i_desc <- Ilink(izero) | Ivar -> i.i_desc <- Ilink izero
| Imax(i1, i2) -> initialized i1; initialized i2 | Imax (i1, i2) -> (initialized i1; initialized i2)
| Ilink(i) -> initialized i | Ilink i -> initialized i
| Ione -> raise Unify | Ione -> raise Unify
(* build an initialization type from a type *) (* build an initialization type from a type *)
let rec skeleton i ty = let rec skeleton i =
match ty with function
| Tbase _ -> leaf i | Tprod ty_list -> product (List.map (skeleton i) ty_list)
| Tprod(ty_list) -> product (List.map (skeleton i) ty_list) | Tarray _ | Tid _ -> leaf i
(* sub-typing *) (* sub-typing *)
let rec less left_ty right_ty = let rec less left_ty right_ty =
if left_ty == right_ty then () if left_ty == right_ty
then ()
else else
match left_ty, right_ty with (match (left_ty, right_ty) with
| Iproduct(l1), Iproduct(l2) -> List.iter2 less l1 l2 | (Iproduct l1, Iproduct l2) -> List.iter2 less l1 l2
| Ileaf(i1), Ileaf(i2) -> iless i1 i2 | (Ileaf i1, Ileaf i2) -> iless i1 i2
| _ -> raise Unify | _ -> raise Unify)
and iless left_i right_i = and iless left_i right_i =
if left_i == right_i then () if left_i == right_i
then ()
else else
let left_i = irepr left_i in (let left_i = irepr left_i in
let right_i = irepr right_i in let right_i = irepr right_i
if left_i == right_i then () in
if left_i == right_i
then ()
else else
match left_i.i_desc, right_i.i_desc with (match ((left_i.i_desc), (right_i.i_desc)) with
| (Izero, _) | (_, Ione) -> () | (Izero, _) | (_, Ione) -> ()
| _, Izero -> initialized left_i | (_, Izero) -> initialized left_i
| Imax(i1, i2), _ -> | (Imax (i1, i2), _) -> (iless i1 right_i; iless i2 right_i)
iless i1 right_i; iless i2 right_i | (_, Ivar) ->
| _, Ivar -> let left_i = occur_check right_i.i_index left_i
let left_i = occur_check right_i.i_index left_i in in right_i.i_desc <- Ilink left_i
right_i.i_desc <- Ilink(left_i) | (_, Imax (i1, i2)) ->
| _, Imax(i1, i2) ->
let i1 = occur_check left_i.i_index i1 in let i1 = occur_check left_i.i_index i1 in
let i2 = occur_check left_i.i_index i2 in let i2 = occur_check left_i.i_index i2
right_i.i_desc <- Ilink(imax left_i (imax i1 i2)) in right_i.i_desc <- Ilink (imax left_i (imax i1 i2))
| _ -> raise Unify | _ -> raise Unify))
(* an inequation [a < t[a]] becomes [a = t[0]] *) and (* an inequation [a < t[a]] becomes [a = t[0]] *) occur_check index i =
and occur_check index i =
match i.i_desc with match i.i_desc with
| Izero | Ione -> i | Izero | Ione -> i
| Ivar -> if i.i_index = index then izero else i | Ivar -> if i.i_index = index then izero else i
| Imax(i1, i2) -> | Imax (i1, i2) -> max (occur_check index i1) (occur_check index i2)
max (occur_check index i1) (occur_check index i2) | Ilink i -> occur_check index i
| Ilink(i) -> occur_check index i
(* computes the initialization type of a merge *) (* computes the initialization type of a merge *)
let merge opt_c c_i_list = let merge opt_c c_i_list =
let rec search c c_i_list = let rec search c c_i_list =
match c_i_list with match c_i_list with
| [] -> izero | [] -> izero
| (c0, i) :: c_i_list -> if c = c0 then i else search c c_i_list in | (c0, i) :: c_i_list -> if c = c0 then i else search c c_i_list
in
match opt_c with match opt_c with
| None -> List.fold_left (fun acc (_, i) -> max acc i) izero c_i_list | None -> List.fold_left (fun acc (_, i) -> max acc i) izero c_i_list
| Some(c) -> search c c_i_list | Some c -> search c c_i_list
module Printer = struct module Printer =
struct
open Format open Format
let rec print_list_r print po sep pf ff = function let rec print_list_r print po sep pf ff =
function
| [] -> () | [] -> ()
| x :: l -> | x :: l ->
fprintf ff "@[%s%a" po print x; (fprintf ff "@[%s%a" po print x;
List.iter (fprintf ff "%s@]@ @[%a" sep print) l; List.iter (fprintf ff "%s@]@ @[%a" sep print) l;
fprintf ff "%s@]" pf fprintf ff "%s@]" pf)
let rec fprint_init ff i = match i.i_desc with let rec fprint_init ff i =
match i.i_desc with
| Izero -> fprintf ff "0" | Izero -> fprintf ff "0"
| Ione -> fprintf ff "1" | Ione -> fprintf ff "1"
| Ivar -> fprintf ff "0" | Ivar -> fprintf ff "0"
| Imax(i1, i2) -> fprintf ff "@[%a\\/%a@]" fprint_init i1 fprint_init i2 | Imax (i1, i2) ->
| Ilink(i) -> fprint_init ff i fprintf ff "@[%a\\/%a@]" fprint_init i1 fprint_init i2
| Ilink i -> fprint_init ff i
let rec fprint_typ ff = function let rec fprint_typ ff =
| Ileaf(i) -> fprint_init ff i function
| Iproduct(ty_list) -> | Ileaf i -> fprint_init ff i
fprintf ff "@[%a@]" (print_list_r fprint_typ "("" *"")") ty_list | Iproduct ty_list ->
fprintf ff "@[%a@]" (print_list_r fprint_typ "(" " *" ")") ty_list
let output_typ oc ty = let output_typ oc ty =
let ff = formatter_of_out_channel oc in let ff = formatter_of_out_channel oc
fprintf ff "@["; in (fprintf ff "@["; fprint_typ ff ty; fprintf ff "@?@]")
fprint_typ ff ty;
fprintf ff "@?@]"
end
module Error = struct end
module Error =
struct
open Location open Location
type error = | Eclash of typ * typ type error = | Eclash of typ * typ
exception Error of location * error exception Error of location * error
let error loc kind = raise (Error(loc, kind)) let error loc kind = raise (Error (loc, kind))
let message loc kind = let message loc kind =
begin match kind with ((match kind with
| Eclash(left_ty, right_ty) -> | Eclash (left_ty, right_ty) ->
Printf.eprintf "%aInitialization error: this expression has type \ Printf.eprintf
"%aInitialization error: this expression has type \
%a, \n\ %a, \n\
but is expected to have type %a\n" but is expected to have type %a\n"
output_location loc output_location loc Printer.output_typ left_ty Printer.
Printer.output_typ left_ty output_typ right_ty);
Printer.output_typ right_ty raise Misc.Error)
end;
raise Misc.Error end
end
let less_exp e actual_ty expected_ty = let less_exp e actual_ty expected_ty =
try try less actual_ty expected_ty
less actual_ty expected_ty with
with | Unify -> Error.message e.e_loc (Error.Eclash(actual_ty, expected_ty)) | Unify -> Error.message e.e_loc (Error.Eclash (actual_ty, expected_ty))
let rec typing h e = let rec typing h e =
match e.e_desc with match e.e_desc with
| Econst(c) -> leaf izero | Econst c -> leaf izero
| Evar(x) -> let { t_init = i } = Env.find x h in leaf i | Evar x -> let { t_init = i } = Env.find x h in leaf i
| Efby(None, e) -> | Efby (None, e) -> (expect h e (skeleton izero e.e_ty); leaf ione)
expect h e (skeleton izero e.e_ty); | Efby ((Some _), e) -> (expect h e (skeleton izero e.e_ty); leaf izero)
leaf ione | Etuple e_list -> product (List.map (typing h) e_list)
| Efby(Some _, e) ->
expect h e (skeleton izero e.e_ty); (*TODO traitement singulier et empêche reset d'un 'op'*)
leaf izero | Ecall (op, e_list, None) when op.op_kind = Eop ->
| Etuple(e_list) -> let i = List.fold_left (fun acc e -> itype (typing h e)) izero e_list
product (List.map (typing h) e_list) in skeleton i e.e_ty
| Eop(_, e_list) -> | Ecall (op, e_list, reset) when op.op_kind = Enode ->
let i = List.fold_left (fun acc e -> itype (typing h e)) izero e_list in
skeleton i e.e_ty
| Eapp(_, e_list) ->
List.iter (fun e -> expect h e (skeleton izero e.e_ty)) e_list; List.iter (fun e -> expect h e (skeleton izero e.e_ty)) e_list;
skeleton izero e.e_ty let i = match reset with
| Eevery(_, e_list, n) -> | None -> izero
List.iter (fun e -> expect h e (skeleton izero e.e_ty)) e_list; | Some(n) -> let { t_init = i } = Env.find n h in i
let { t_init = i } = Env.find n h in in skeleton i e.e_ty
skeleton i e.e_ty | Ewhen (e, c, n) ->
| Ewhen(e, c, n) ->
let { t_init = i1 } = Env.find n h in let { t_init = i1 } = Env.find n h in
let i2 = itype (typing h e) in let i2 = itype (typing h e) in skeleton (max i1 i2) e.e_ty
skeleton (max i1 i2) e.e_ty | Eifthenelse (e1, e2, e3) ->
| Eifthenelse(e1, e2, e3) ->
let i1 = itype (typing h e1) in let i1 = itype (typing h e1) in
let i2 = itype (typing h e2) in let i2 = itype (typing h e2) in
let i3 = itype (typing h e3) in let i3 = itype (typing h e3) in
let i = max i1 (max i2 i3) in let i = max i1 (max i2 i3) in skeleton i e.e_ty
skeleton i e.e_ty | Emerge (n, c_e_list) ->
| Emerge(n, c_e_list) ->
let { t_init = i; t_value = opt_c } = Env.find n h in let { t_init = i; t_value = opt_c } = Env.find n h in
let i = let i =
merge opt_c merge opt_c
(List.map (fun (c, e) -> (c, itype (typing h e))) c_e_list) in (List.map (fun (c, e) -> (c, (itype (typing h e)))) c_e_list)
skeleton i e.e_ty in skeleton i e.e_ty
| Efield(e1,n) -> | Efield (e1, n) -> let i = itype (typing h e1) in skeleton i e.e_ty
let i = itype (typing h e1) in | Estruct l ->
skeleton i e.e_ty
| Estruct(l) ->
let i = let i =
List.fold_left List.fold_left (fun acc (_, e) -> max acc (itype (typing h e))) izero
(fun acc (_, e) -> max acc (itype (typing h e))) izero l in l
skeleton i e.e_ty in skeleton i e.e_ty
| Efield_update _ | Econstvar _ | Earray _ | Earray_op _ ->
leaf izero (* TODO FIXME array_op dans init *)
and expect h e expected_ty = and expect h e expected_ty =
let actual_ty = typing h e in let actual_ty = typing h e in less_exp e actual_ty expected_ty
less_exp e actual_ty expected_ty
let rec typing_pat h = function let rec typing_pat h =
| Evarpat(x) -> let { t_init = i } = Env.find x h in leaf i function
| Etuplepat(pat_list) -> | Evarpat x -> let { t_init = i } = Env.find x h in leaf i
product (List.map (typing_pat h) pat_list) | Etuplepat pat_list -> product (List.map (typing_pat h) pat_list)
let typing_eqs h eq_list = let typing_eqs h eq_list =
List.iter List.iter
(fun { eq_lhs = pat; eq_rhs = e } -> (fun { eq_lhs = pat; eq_rhs = e } ->
let ty_pat = typing_pat h pat in let ty_pat = typing_pat h pat in expect h e ty_pat)
expect h e ty_pat) eq_list eq_list
let build h eq_list = let build h eq_list =
let rec build_pat h = function let rec build_pat h =
| Evarpat(x) -> Env.add x { t_init = new_var (); t_value = None } h function
| Etuplepat(pat_list) -> List.fold_left build_pat h pat_list in | Evarpat x -> Env.add x { t_init = new_var (); t_value = None; } h
| Etuplepat pat_list -> List.fold_left build_pat h pat_list in
let build_equation h { eq_lhs = pat; eq_rhs = e } = let build_equation h { eq_lhs = pat; eq_rhs = e } =
match pat, e.e_desc with match (pat, (e.e_desc)) with
| Evarpat(x), Efby(Some(Cconstr c), _) -> | (Evarpat x, Efby ((Some (Cconstr c)), _)) ->
(* we keep the initial value of state variables *) (* we keep the initial value of state variables *)
Env.add x { t_init = new_var (); t_value = Some(c) } h Env.add x { t_init = new_var (); t_value = Some c; } h
| _ -> build_pat h pat in | _ -> build_pat h pat
List.fold_left build_equation h eq_list in List.fold_left build_equation h eq_list
let sbuild h dec = let sbuild h dec =
List.fold_left List.fold_left
(fun h { v_name = n } -> Env.add n { t_init = izero; t_value = None } h) (fun h { v_name = n } -> Env.add n { t_init = izero; t_value = None; } h)
h dec h dec
let typing_contract h contract = let typing_contract h contract =
match contract with match contract with
| None -> h | None -> h
| Some { c_local = l_list; c_eq = eq_list; c_assume = e_a; | Some
c_enforce = e_g; c_controllables = c_list } -> {
c_local = l_list;
c_eq = eq_list;
c_assume = e_a;
c_enforce = e_g;
c_controllables = c_list
} ->
let h = sbuild h c_list in let h = sbuild h c_list in
let h' = build h eq_list in let h' = build h eq_list
typing_eqs h' eq_list; in
(* assumption *) (* assumption *)
expect h' e_a (skeleton izero e_a.e_ty);
(* property *) (* property *)
(typing_eqs h' eq_list;
expect h' e_a (skeleton izero e_a.e_ty);
expect h' e_g (skeleton izero e_g.e_ty); expect h' e_g (skeleton izero e_g.e_ty);
h h)
let typing_node { n_name = f; n_input = i_list; n_output = o_list; let typing_node {
n_name = f;
n_input = i_list;
n_output = o_list;
n_contract = contract; n_contract = contract;
n_local = l_list; n_equs = eq_list } = n_local = l_list;
n_equs = eq_list
} =
let h = sbuild Env.empty i_list in let h = sbuild Env.empty i_list in
let h = sbuild h o_list in let h = sbuild h o_list in
let h = typing_contract h contract in let h = typing_contract h contract in
let h = build h eq_list in typing_eqs h eq_list
let h = build h eq_list in let program (({ p_nodes = p_node_list } as p)) =
typing_eqs h eq_list (List.iter typing_node p_node_list; p)
let program ({ p_nodes = p_node_list } as p) =
List.iter typing_node p_node_list;
p