2012-06-27 18:09:30 +02:00
|
|
|
(***********************************************************************)
|
|
|
|
(* *)
|
|
|
|
(* Heptagon *)
|
|
|
|
(* *)
|
|
|
|
(* Gwenael Delaval, LIG/INRIA, UJF *)
|
|
|
|
(* Leonard Gerard, Parkas, ENS *)
|
|
|
|
(* Adrien Guatto, Parkas, ENS *)
|
|
|
|
(* Cedric Pasteur, Parkas, ENS *)
|
2012-06-29 01:43:15 +02:00
|
|
|
(* Marc Pouzet, Parkas, ENS *)
|
2012-06-27 18:09:30 +02:00
|
|
|
(* *)
|
|
|
|
(* 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/> *)
|
|
|
|
(* *)
|
|
|
|
(***********************************************************************)
|
2011-04-20 11:19:18 +02:00
|
|
|
open Idents
|
2011-04-20 15:41:15 +02:00
|
|
|
open Types
|
|
|
|
open Signature
|
2011-07-21 08:50:45 +02:00
|
|
|
open Clocks
|
2011-04-20 15:41:15 +02:00
|
|
|
open Minils
|
2011-04-26 18:02:18 +02:00
|
|
|
open Linearity
|
2011-04-20 11:19:18 +02:00
|
|
|
open Interference_graph
|
2011-04-26 18:02:18 +02:00
|
|
|
open Containers
|
2011-04-20 16:52:34 +02:00
|
|
|
open Printf
|
|
|
|
|
2011-04-27 08:26:40 +02:00
|
|
|
let print_interference_graphs = false
|
2011-04-29 13:58:31 +02:00
|
|
|
let verbose_mode = false
|
2011-04-21 14:42:14 +02:00
|
|
|
|
2012-06-20 09:17:13 +02:00
|
|
|
module TyEnv =
|
|
|
|
ListMap(struct
|
|
|
|
type t = ty
|
|
|
|
let compare = Global_compare.type_compare
|
|
|
|
end)
|
|
|
|
|
|
|
|
module VarEnv = struct
|
|
|
|
include Idents.Env
|
|
|
|
|
|
|
|
let add_ivar env iv =
|
|
|
|
let x = var_ident_of_ivar iv in
|
|
|
|
if mem x env then
|
|
|
|
add x (IvarSet.add iv (find x env)) env
|
|
|
|
else
|
|
|
|
add x (IvarSet.singleton iv) env
|
|
|
|
end
|
2011-04-21 14:42:14 +02:00
|
|
|
|
2012-06-20 09:17:13 +02:00
|
|
|
let print_debug fmt =
|
2011-04-21 14:42:14 +02:00
|
|
|
if verbose_mode then
|
2012-06-20 09:17:13 +02:00
|
|
|
Format.printf fmt
|
|
|
|
else
|
|
|
|
Format.ifprintf Format.std_formatter fmt
|
2011-04-21 14:42:14 +02:00
|
|
|
|
|
|
|
let print_debug_ivar_env name env =
|
|
|
|
if verbose_mode then (
|
|
|
|
Format.printf "%s: " name;
|
2012-06-20 09:17:13 +02:00
|
|
|
IvarEnv.iter (fun k v -> Format.printf "%a : %d; " print_ivar k v) env;
|
2011-04-21 14:42:14 +02:00
|
|
|
Format.printf "@."
|
|
|
|
)
|
|
|
|
|
2012-06-20 09:17:13 +02:00
|
|
|
let print_debug_var_env name env =
|
2012-02-09 11:06:14 +01:00
|
|
|
if verbose_mode then (
|
|
|
|
Format.printf "%s: " name;
|
2012-06-20 09:17:13 +02:00
|
|
|
VarEnv.iter (fun _ l -> IvarSet.iter (fun k -> Format.printf "%a; " print_ivar k) l) env;
|
2012-02-09 11:06:14 +01:00
|
|
|
Format.printf "@."
|
|
|
|
)
|
|
|
|
|
2012-01-24 10:29:05 +01:00
|
|
|
(** @return whether [ty] corresponds to a record type. *)
|
2012-01-30 17:48:47 +01:00
|
|
|
let is_record_type ty = match Modules.unalias_type ty with
|
2012-01-24 10:29:05 +01:00
|
|
|
| Tid n ->
|
|
|
|
(match Modules.find_type n with
|
|
|
|
| Tstruct _ -> true
|
|
|
|
| _ -> false)
|
|
|
|
| _ -> false
|
|
|
|
|
|
|
|
let is_array_or_struct ty =
|
|
|
|
match Modules.unalias_type ty with
|
|
|
|
| Tarray _ -> true
|
|
|
|
| Tid n ->
|
|
|
|
(match Modules.find_type n with
|
|
|
|
| Signature.Tstruct _ -> true
|
|
|
|
| _ -> false)
|
|
|
|
| _ -> false
|
|
|
|
|
2012-01-30 17:48:47 +01:00
|
|
|
let is_enum ty = match Modules.unalias_type ty with
|
|
|
|
| Tid n ->
|
|
|
|
(match Modules.find_type n with
|
|
|
|
| Tenum _ -> true
|
|
|
|
| _ -> false)
|
|
|
|
| _ -> false
|
|
|
|
|
2011-04-20 15:41:15 +02:00
|
|
|
module InterfRead = struct
|
2011-10-04 14:34:36 +02:00
|
|
|
exception Const_extvalue
|
|
|
|
|
2011-04-20 15:41:15 +02:00
|
|
|
let rec vars_ck acc = function
|
2012-06-20 09:17:13 +02:00
|
|
|
| Con(ck2, _, n) -> (Ivar n)::(vars_ck acc ck2)
|
2011-04-20 15:41:15 +02:00
|
|
|
| Cbase | Cvar { contents = Cindex _ } -> acc
|
|
|
|
| Cvar { contents = Clink ck } -> vars_ck acc ck
|
|
|
|
|
2012-01-25 09:34:58 +01:00
|
|
|
let rec vars_ct acc ct = match ct with
|
|
|
|
| Ck ck -> vars_ck acc ck
|
|
|
|
| Cprod ct_list -> List.fold_left vars_ct acc ct_list
|
|
|
|
|
2012-06-20 09:17:13 +02:00
|
|
|
let rec ivar_of_extvalue w' = match w'.w_desc with
|
2011-04-20 15:41:15 +02:00
|
|
|
| Wvar x -> Ivar x
|
|
|
|
| Wfield(w, f) -> Ifield (ivar_of_extvalue w, f)
|
2012-06-20 09:17:13 +02:00
|
|
|
| Wwhen(w, _, _) -> Iwhen (ivar_of_extvalue w, w'.w_ck)
|
2011-10-04 14:34:36 +02:00
|
|
|
| Wconst _ -> raise Const_extvalue
|
2011-10-17 15:28:04 +02:00
|
|
|
| Wreinit (_, w) -> ivar_of_extvalue w
|
2011-04-20 15:41:15 +02:00
|
|
|
|
2011-04-27 14:52:37 +02:00
|
|
|
let ivar_of_pat p = match p with
|
|
|
|
| Evarpat x -> Ivar x
|
|
|
|
| _ -> assert false
|
|
|
|
|
2011-04-20 15:41:15 +02:00
|
|
|
let ivars_of_extvalues wl =
|
2011-10-04 14:34:36 +02:00
|
|
|
let tr_one acc w =
|
|
|
|
try
|
|
|
|
(ivar_of_extvalue w)::acc
|
|
|
|
with
|
|
|
|
| Const_extvalue -> acc
|
2011-04-20 15:41:15 +02:00
|
|
|
in
|
|
|
|
List.fold_left tr_one [] wl
|
|
|
|
|
|
|
|
let read_extvalue funs acc w =
|
|
|
|
(* recursive call *)
|
2012-06-20 09:17:13 +02:00
|
|
|
(*let _, acc = Mls_mapfold.extvalue funs acc w in*)
|
2011-04-20 15:41:15 +02:00
|
|
|
let acc =
|
2011-10-04 14:34:36 +02:00
|
|
|
try
|
2012-06-20 09:17:13 +02:00
|
|
|
(ivar_of_extvalue w)::acc
|
2011-10-04 14:34:36 +02:00
|
|
|
with
|
|
|
|
| Const_extvalue -> acc
|
2011-04-20 15:41:15 +02:00
|
|
|
in
|
|
|
|
w, vars_ck acc w.w_ck
|
|
|
|
|
|
|
|
let read_exp funs acc e =
|
|
|
|
(* recursive call *)
|
|
|
|
let _, acc = Mls_mapfold.exp funs acc e in
|
|
|
|
(* special cases *)
|
|
|
|
let acc = match e.e_desc with
|
|
|
|
| Emerge(x,_) | Eapp(_, _, Some x)
|
2012-06-20 09:17:13 +02:00
|
|
|
| Eiterator (_, _, _, _, _, Some x) -> (Ivar x)::acc
|
2011-04-20 15:41:15 +02:00
|
|
|
| _ -> acc
|
|
|
|
in
|
2012-02-09 11:48:36 +01:00
|
|
|
e, acc
|
2011-04-20 15:41:15 +02:00
|
|
|
|
|
|
|
let rec vars_pat acc = function
|
2012-06-20 09:17:13 +02:00
|
|
|
| Evarpat x -> x::acc
|
2011-04-20 15:41:15 +02:00
|
|
|
| Etuplepat pat_list -> List.fold_left vars_pat acc pat_list
|
|
|
|
|
|
|
|
let def eq =
|
2012-06-20 09:17:13 +02:00
|
|
|
vars_pat [] eq.eq_lhs
|
|
|
|
let def_ivars eq =
|
|
|
|
List.map (fun x -> Ivar x) (def eq)
|
2011-04-20 15:41:15 +02:00
|
|
|
|
2011-04-26 18:02:18 +02:00
|
|
|
let rec nth_var_from_pat j pat =
|
|
|
|
match j, pat with
|
|
|
|
| 0, Evarpat x -> x
|
|
|
|
| n, Etuplepat l -> nth_var_from_pat 0 (List.nth l n)
|
|
|
|
| _, _ -> assert false
|
|
|
|
|
2011-04-20 15:41:15 +02:00
|
|
|
let read_exp e =
|
|
|
|
let funs = { Mls_mapfold.defaults with
|
|
|
|
Mls_mapfold.exp = read_exp;
|
|
|
|
Mls_mapfold.extvalue = read_extvalue } in
|
2012-06-20 09:17:13 +02:00
|
|
|
let _, acc = Mls_mapfold.exp_it funs [] e in
|
2011-04-20 15:41:15 +02:00
|
|
|
acc
|
|
|
|
|
|
|
|
let read eq =
|
|
|
|
read_exp eq.eq_rhs
|
|
|
|
end
|
|
|
|
|
|
|
|
|
2011-04-20 14:05:55 +02:00
|
|
|
module World = struct
|
2011-04-20 15:41:15 +02:00
|
|
|
let vds = ref Env.empty
|
2012-06-20 09:17:13 +02:00
|
|
|
let memories = ref IdentSet.empty
|
2011-04-26 18:02:18 +02:00
|
|
|
let igs = ref []
|
2011-04-20 11:19:18 +02:00
|
|
|
|
2011-04-20 15:41:15 +02:00
|
|
|
let init f =
|
2011-04-20 11:19:18 +02:00
|
|
|
(* build vds cache *)
|
2011-04-20 15:41:15 +02:00
|
|
|
let build env vds =
|
|
|
|
List.fold_left (fun env vd -> Env.add vd.v_ident vd env) env vds
|
2011-04-20 11:19:18 +02:00
|
|
|
in
|
2011-04-20 15:41:15 +02:00
|
|
|
let env = build Env.empty f.n_input in
|
2011-04-20 11:19:18 +02:00
|
|
|
let env = build env f.n_output in
|
|
|
|
let env = build env f.n_local in
|
2012-06-07 15:27:07 +02:00
|
|
|
let env =
|
|
|
|
match f.n_contract with
|
|
|
|
None -> env
|
2012-06-20 09:17:13 +02:00
|
|
|
| Some c ->
|
2012-06-07 15:27:07 +02:00
|
|
|
let env = build env c.c_local in
|
|
|
|
build env c.c_controllables in
|
2011-04-26 18:02:18 +02:00
|
|
|
igs := [];
|
2011-04-20 11:19:18 +02:00
|
|
|
vds := env;
|
2012-06-20 09:17:13 +02:00
|
|
|
(* build the set of memories *)
|
2011-04-20 11:19:18 +02:00
|
|
|
let mems = Mls_utils.node_memory_vars f in
|
2012-06-20 09:17:13 +02:00
|
|
|
let s = List.fold_left (fun s (x, _) -> IdentSet.add x s) IdentSet.empty mems in
|
|
|
|
memories := s
|
2011-04-20 11:19:18 +02:00
|
|
|
|
|
|
|
let vd_from_ident x =
|
2012-03-30 14:43:33 +02:00
|
|
|
try Env.find x !vds
|
|
|
|
with Not_found ->
|
|
|
|
Format.eprintf "Unknown variable %a@." print_ident x;
|
|
|
|
Misc.internal_error "interference"
|
2011-04-20 11:19:18 +02:00
|
|
|
|
|
|
|
let rec ivar_type iv = match iv with
|
|
|
|
| Ivar x ->
|
|
|
|
let vd = vd_from_ident x in
|
|
|
|
vd.v_type
|
|
|
|
| Ifield(_, f) ->
|
2011-04-20 18:20:53 +02:00
|
|
|
let n = Modules.find_field f in
|
|
|
|
let fields = Modules.find_struct n in
|
|
|
|
Signature.field_assoc f fields
|
2012-06-20 09:17:13 +02:00
|
|
|
| Iwhen (iv, _) -> ivar_type iv
|
|
|
|
|
|
|
|
let ivar_clock iv = match iv with
|
|
|
|
| Iwhen (_, ck) -> ck
|
|
|
|
| _ ->
|
|
|
|
let vd = vd_from_ident (var_ident_of_ivar iv) in
|
|
|
|
vd.v_clock
|
2011-04-20 11:19:18 +02:00
|
|
|
|
2011-04-20 14:05:55 +02:00
|
|
|
let is_optimized_ty ty =
|
2012-02-08 11:13:02 +01:00
|
|
|
(!Compiler_options.interf_all (* && not (is_enum ty)) *) ) || is_array_or_struct ty
|
2011-04-20 14:05:55 +02:00
|
|
|
|
|
|
|
let is_optimized iv =
|
|
|
|
is_optimized_ty (ivar_type iv)
|
|
|
|
|
|
|
|
let is_memory x =
|
2012-06-20 09:17:13 +02:00
|
|
|
IdentSet.mem x !memories
|
2011-04-20 14:05:55 +02:00
|
|
|
|
2011-04-20 11:19:18 +02:00
|
|
|
let node_for_ivar iv =
|
2011-04-20 15:41:15 +02:00
|
|
|
let rec _node_for_ivar igs iv =
|
2011-04-20 11:19:18 +02:00
|
|
|
match igs with
|
2012-06-20 09:17:13 +02:00
|
|
|
| [] -> print_debug "Var not in graph: %a@." print_ivar iv; raise Not_found
|
2011-04-20 11:19:18 +02:00
|
|
|
| ig::igs ->
|
|
|
|
(try
|
|
|
|
ig, node_for_value ig iv
|
|
|
|
with Not_found ->
|
|
|
|
_node_for_ivar igs iv)
|
|
|
|
in
|
2012-06-20 09:17:13 +02:00
|
|
|
_node_for_ivar !igs (remove_iwhen iv)
|
2011-04-20 11:19:18 +02:00
|
|
|
|
|
|
|
let node_for_name x =
|
|
|
|
node_for_ivar (Ivar x)
|
|
|
|
end
|
|
|
|
|
|
|
|
(** Helper functions to work with the multiple interference graphs *)
|
|
|
|
|
2011-04-20 15:41:15 +02:00
|
|
|
let by_ivar def f x y =
|
2011-04-27 15:10:22 +02:00
|
|
|
if World.is_optimized x then (
|
|
|
|
let igx, nodex = World.node_for_ivar x in
|
|
|
|
let igy, nodey = World.node_for_ivar y in
|
|
|
|
if igx == igy then
|
|
|
|
f igx nodex nodey
|
|
|
|
else
|
|
|
|
def
|
|
|
|
) else
|
|
|
|
def
|
2011-04-20 11:19:18 +02:00
|
|
|
|
2011-04-20 15:41:15 +02:00
|
|
|
let by_name def f x y =
|
2011-04-27 15:10:22 +02:00
|
|
|
if World.is_optimized (Ivar x) then (
|
|
|
|
let igx, nodex = World.node_for_name x in
|
|
|
|
let igy, nodey = World.node_for_name y in
|
|
|
|
if igx == igy then
|
|
|
|
f igx nodex nodey
|
|
|
|
else
|
|
|
|
def
|
|
|
|
) else
|
|
|
|
def
|
2011-04-20 11:19:18 +02:00
|
|
|
|
2011-04-20 15:41:15 +02:00
|
|
|
let add_interference_link_from_name = by_name () add_interference_link
|
|
|
|
let add_interference_link_from_ivar = by_ivar () add_interference_link
|
|
|
|
let add_affinity_link_from_name = by_name () add_affinity_link
|
|
|
|
let add_affinity_link_from_ivar = by_ivar () add_affinity_link
|
|
|
|
let add_same_value_link_from_name = by_name () add_affinity_link
|
|
|
|
let add_same_value_link_from_ivar = by_ivar () add_affinity_link
|
|
|
|
let coalesce_from_name = by_name () coalesce
|
2011-04-26 18:02:18 +02:00
|
|
|
let coalesce_from_ivar = by_ivar () coalesce
|
2011-04-20 15:41:15 +02:00
|
|
|
let have_same_value_from_name = by_name false have_same_value
|
2012-06-20 09:17:13 +02:00
|
|
|
let have_same_value_from_ivar = by_ivar false have_same_value
|
2011-04-20 11:19:18 +02:00
|
|
|
|
2011-04-21 16:49:58 +02:00
|
|
|
let remove_from_ivar iv =
|
2011-04-21 13:42:28 +02:00
|
|
|
try
|
2011-04-21 16:49:58 +02:00
|
|
|
let ig, v = World.node_for_ivar iv in
|
2011-04-21 13:42:28 +02:00
|
|
|
G.remove_vertex ig.g_graph v
|
|
|
|
with
|
|
|
|
| Not_found -> (* var not in graph, just ignore it *) ()
|
2011-04-20 11:19:18 +02:00
|
|
|
|
|
|
|
|
2012-06-20 09:17:13 +02:00
|
|
|
(** Adds all the fields of a variable to the list [l] (when it corresponds to a record). *)
|
|
|
|
let rec all_ivars l iv ck ty =
|
|
|
|
if not (World.is_optimized_ty ty) then
|
|
|
|
l
|
|
|
|
else (
|
|
|
|
let iv' = match ck with None -> iv | Some ck -> Iwhen(iv, ck) in
|
|
|
|
let l = iv'::l in
|
|
|
|
match Modules.unalias_type ty with
|
|
|
|
| Tid n ->
|
|
|
|
(try
|
|
|
|
let fields = Modules.find_struct n in
|
|
|
|
List.fold_left (all_ivars_field iv ck) l fields
|
|
|
|
with
|
|
|
|
Not_found -> l
|
|
|
|
)
|
|
|
|
| _ -> l
|
|
|
|
)
|
|
|
|
|
|
|
|
and all_ivars_field iv ck l { f_name = n; f_type = ty } =
|
|
|
|
let new_iv = match ck with
|
|
|
|
| None -> Ifield(iv, n)
|
|
|
|
| Some ck -> Iwhen (Ifield(iv, n), ck)
|
2011-04-20 11:19:18 +02:00
|
|
|
in
|
2012-06-20 09:17:13 +02:00
|
|
|
all_ivars l new_iv ck ty
|
2011-04-20 11:19:18 +02:00
|
|
|
|
2012-06-20 09:17:13 +02:00
|
|
|
let all_ivars_list ivs =
|
|
|
|
let add_one acc iv =
|
|
|
|
let ck = match iv with
|
|
|
|
| Iwhen (_, ck) -> Some ck
|
|
|
|
| _ -> None
|
|
|
|
in
|
|
|
|
let iv = remove_iwhen iv in
|
|
|
|
all_ivars acc iv ck (World.ivar_type iv)
|
|
|
|
in
|
|
|
|
List.fold_left add_one [] ivs
|
2011-05-02 17:59:12 +02:00
|
|
|
|
2012-06-20 09:17:13 +02:00
|
|
|
(* TODO: variables with no use ?? *)
|
2011-04-20 15:41:15 +02:00
|
|
|
let compute_live_vars eqs =
|
2012-06-20 09:17:13 +02:00
|
|
|
let aux (alive_vars, res) eq =
|
|
|
|
let read_ivars = all_ivars_list (InterfRead.read eq) in
|
|
|
|
let def_ivars = InterfRead.def eq in
|
|
|
|
(* add vars used in the equation *)
|
|
|
|
let alive_vars = List.fold_left VarEnv.add_ivar alive_vars read_ivars in
|
|
|
|
(* remove vars defined in this equation *)
|
|
|
|
let alive_vars =
|
|
|
|
List.fold_left (fun alive_vars id -> VarEnv.remove id alive_vars) alive_vars def_ivars
|
|
|
|
in
|
|
|
|
print_debug "%a@," Mls_printer.print_eq eq;
|
|
|
|
print_debug_var_env "alive" alive_vars;
|
|
|
|
let alive_vars_list = VarEnv.fold (fun _ ivs acc -> (IvarSet.elements ivs)@acc) alive_vars [] in
|
|
|
|
let res = (eq, alive_vars_list)::res in
|
|
|
|
alive_vars, res
|
2011-04-20 11:19:18 +02:00
|
|
|
in
|
2012-06-20 09:17:13 +02:00
|
|
|
let _, res = List.fold_left aux (VarEnv.empty, []) (List.rev eqs) in
|
2011-04-20 11:19:18 +02:00
|
|
|
res
|
|
|
|
|
|
|
|
(** [should_interfere x y] returns whether variables x and y
|
|
|
|
can interfere. *)
|
2012-06-20 09:17:13 +02:00
|
|
|
let should_interfere (ivx, ivy) =
|
|
|
|
let tyx = World.ivar_type ivx in
|
|
|
|
let tyy = World.ivar_type ivy in
|
|
|
|
if Global_compare.type_compare tyx tyy <> 0 then
|
2011-04-20 11:19:18 +02:00
|
|
|
false
|
|
|
|
else (
|
2012-06-20 09:17:13 +02:00
|
|
|
let x_is_mem = World.is_memory (var_ident_of_ivar ivx) in
|
|
|
|
let x_is_when = is_when_ivar ivx in
|
|
|
|
let y_is_mem = World.is_memory (var_ident_of_ivar ivy) in
|
|
|
|
let y_is_when = is_when_ivar ivy in
|
|
|
|
let ckx = World.ivar_clock ivx in
|
|
|
|
let cky = World.ivar_clock ivy in
|
|
|
|
let are_copies = have_same_value_from_ivar ivx ivy in
|
|
|
|
(* a register with a slow clock is still alive even when it is not activated.
|
|
|
|
However, if we read a fast register on a slow rhythm,
|
|
|
|
we can share it with other variables on disjoint slow rhythms as we know
|
|
|
|
that the value of the register will
|
|
|
|
be done at the end of the step. *)
|
|
|
|
let disjoint_clocks =
|
2012-06-20 17:09:17 +02:00
|
|
|
not ((x_is_mem && not x_is_when) || (y_is_mem && not y_is_when)) && Clocks.are_disjoint ckx cky
|
2012-06-20 09:17:13 +02:00
|
|
|
in
|
2011-04-20 11:19:18 +02:00
|
|
|
not (disjoint_clocks or are_copies)
|
|
|
|
)
|
|
|
|
|
2011-04-20 15:41:15 +02:00
|
|
|
let should_interfere = Misc.memoize_couple should_interfere
|
2011-04-20 11:19:18 +02:00
|
|
|
|
2012-06-20 09:17:13 +02:00
|
|
|
|
2011-04-20 11:19:18 +02:00
|
|
|
(** Builds the (empty) interference graphs corresponding to the
|
|
|
|
variable declaration list vds. It just creates one graph per type
|
|
|
|
and one node per declaration. *)
|
2011-04-21 13:42:28 +02:00
|
|
|
let init_interference_graph () =
|
2011-04-20 11:19:18 +02:00
|
|
|
(** Adds a node for the variable and all fields of a variable. *)
|
|
|
|
let rec add_ivar env iv ty =
|
2012-06-20 09:17:13 +02:00
|
|
|
let ivars = all_ivars [] iv None ty in
|
|
|
|
List.fold_left (fun env iv -> TyEnv.add_element (World.ivar_type iv) (mk_node iv) env) env ivars
|
2011-04-20 11:19:18 +02:00
|
|
|
in
|
2011-04-21 13:42:28 +02:00
|
|
|
let env = Env.fold
|
|
|
|
(fun _ vd env -> add_ivar env (Ivar vd.v_ident) vd.v_type) !World.vds TyEnv.empty in
|
2011-04-20 15:41:15 +02:00
|
|
|
World.igs := TyEnv.fold (fun ty l acc -> (mk_graph l ty)::acc) env []
|
2011-04-20 11:19:18 +02:00
|
|
|
|
|
|
|
|
|
|
|
(** Adds interferences between all the variables in
|
|
|
|
the list. If force is true, then interference is added
|
|
|
|
whatever the variables are, without checking if interference
|
|
|
|
is real. *)
|
|
|
|
let rec add_interferences_from_list force vars =
|
2012-06-20 09:17:13 +02:00
|
|
|
let add_interference ivx ivy =
|
|
|
|
if force or should_interfere (ivx, ivy) then
|
|
|
|
add_interference_link_from_ivar ivx ivy
|
2011-04-20 11:19:18 +02:00
|
|
|
in
|
2011-04-20 15:41:15 +02:00
|
|
|
Misc.iter_couple add_interference vars
|
2011-04-20 11:19:18 +02:00
|
|
|
|
|
|
|
(** Adds to the interference graphs [igs] the
|
|
|
|
interference resulting from the live vars sets
|
|
|
|
stored in hash. *)
|
2011-04-20 15:41:15 +02:00
|
|
|
let add_interferences live_vars =
|
2011-04-20 11:19:18 +02:00
|
|
|
List.iter (fun (_, vars) -> add_interferences_from_list false vars) live_vars
|
|
|
|
|
2012-01-24 10:29:05 +01:00
|
|
|
(** Spill non linear inputs. *)
|
2011-04-21 13:42:28 +02:00
|
|
|
let spill_inputs f =
|
2011-04-26 18:02:18 +02:00
|
|
|
let spilled_inp = List.filter (fun vd -> not (is_linear vd.v_linearity)) f.n_input in
|
2012-06-20 09:17:13 +02:00
|
|
|
let spilled_inp = List.map (fun vd -> Ivar vd.v_ident) spilled_inp in
|
|
|
|
let spilled_inp = all_ivars_list spilled_inp in
|
|
|
|
List.iter remove_from_ivar spilled_inp
|
2012-01-24 10:29:05 +01:00
|
|
|
|
|
|
|
(** If we optimize all types, we need to spill outputs and memories so
|
|
|
|
that register allocation by the C compiler is not disturbed. *)
|
|
|
|
let spill_mems_outputs f =
|
2012-06-20 09:17:13 +02:00
|
|
|
let add_output l vd =
|
|
|
|
if not (is_array_or_struct vd.v_type) then (Ivar vd.v_ident)::l else l
|
2012-01-24 10:29:05 +01:00
|
|
|
in
|
2012-06-20 09:17:13 +02:00
|
|
|
let add_memory x l =
|
|
|
|
let iv = Ivar x in
|
|
|
|
if not (is_array_or_struct (World.ivar_type iv)) then iv::l else l
|
2012-01-24 10:29:05 +01:00
|
|
|
in
|
2012-06-20 09:17:13 +02:00
|
|
|
let spilled_vars = List.fold_left add_output [] f.n_output in
|
|
|
|
let spilled_vars = IdentSet.fold add_memory !World.memories spilled_vars in
|
|
|
|
let spilled_vars = all_ivars_list spilled_vars in
|
|
|
|
List.iter remove_from_ivar spilled_vars
|
2011-04-20 11:19:18 +02:00
|
|
|
|
|
|
|
(** [filter_vars l] returns a list of variables whose fields appear in
|
|
|
|
a list of ivar.*)
|
|
|
|
let rec filter_fields = function
|
|
|
|
| [] -> []
|
2011-04-20 15:41:15 +02:00
|
|
|
| (Ifield (id, _))::l -> id::(filter_fields l)
|
2011-04-20 11:19:18 +02:00
|
|
|
| _::l -> filter_fields l
|
|
|
|
|
|
|
|
(** Adds the interference between records variables
|
|
|
|
caused by interferences between their fields. *)
|
|
|
|
let add_records_field_interferences () =
|
2011-04-20 15:41:15 +02:00
|
|
|
let add_record_interf g n1 n2 =
|
|
|
|
if interfere g n1 n2 then
|
|
|
|
let v1 = filter_fields !(G.V.label n1) in
|
|
|
|
let v2 = filter_fields !(G.V.label n2) in
|
|
|
|
Misc.iter_couple_2 add_interference_link_from_ivar v1 v2
|
2011-04-20 11:19:18 +02:00
|
|
|
in
|
2011-04-20 15:41:15 +02:00
|
|
|
List.iter (iter_interf add_record_interf) !World.igs
|
2011-04-20 11:19:18 +02:00
|
|
|
|
|
|
|
|
|
|
|
|
2011-04-26 18:02:18 +02:00
|
|
|
(** Coalesce the nodes corresponding to all semilinear variables
|
|
|
|
with the same location. *)
|
|
|
|
let coalesce_linear_vars () =
|
|
|
|
let coalesce_one_var _ vd memlocs =
|
|
|
|
if World.is_optimized_ty vd.v_type then
|
|
|
|
(match vd.v_linearity with
|
|
|
|
| Ltop -> memlocs
|
|
|
|
| Lat r ->
|
|
|
|
if LocationEnv.mem r memlocs then (
|
|
|
|
coalesce_from_name vd.v_ident (LocationEnv.find r memlocs);
|
|
|
|
memlocs
|
|
|
|
) else
|
|
|
|
LocationEnv.add r vd.v_ident memlocs
|
|
|
|
| _ -> assert false)
|
|
|
|
else
|
|
|
|
memlocs
|
|
|
|
in
|
|
|
|
ignore (Env.fold coalesce_one_var !World.vds LocationEnv.empty)
|
|
|
|
|
|
|
|
let find_targeting f =
|
|
|
|
let find_output outputs_lins (acc,i) l =
|
2011-04-27 15:10:10 +02:00
|
|
|
match l with
|
|
|
|
| Lvar _ ->
|
|
|
|
let idx = Misc.index (fun l1 -> l = l1) outputs_lins in
|
|
|
|
if idx >= 0 then
|
|
|
|
(i, idx)::acc, i+1
|
|
|
|
else
|
|
|
|
acc, i+1
|
|
|
|
| _ -> acc, i+1
|
2011-04-26 18:02:18 +02:00
|
|
|
in
|
|
|
|
let desc = Modules.find_value f in
|
|
|
|
let inputs_lins = linearities_of_arg_list desc.node_inputs in
|
|
|
|
let outputs_lins = linearities_of_arg_list desc.node_outputs in
|
|
|
|
let acc, _ = List.fold_left (find_output outputs_lins) ([], 0) inputs_lins in
|
|
|
|
acc
|
|
|
|
|
|
|
|
|
2011-04-20 11:19:18 +02:00
|
|
|
(** [process_eq igs eq] adds to the interference graphs igs
|
|
|
|
the links corresponding to the equation. Interferences
|
|
|
|
corresponding to live vars sets are already added by build_interf_graph.
|
|
|
|
*)
|
2011-04-20 15:41:15 +02:00
|
|
|
let process_eq ({ eq_lhs = pat; eq_rhs = e } as eq) =
|
2011-04-20 11:19:18 +02:00
|
|
|
(** Other cases*)
|
|
|
|
match pat, e.e_desc with
|
2011-06-07 10:49:36 +02:00
|
|
|
| _, Eiterator((Imap|Imapi), { a_op = Enode _ | Efun _ }, _, pw_list, w_list, _) ->
|
2011-04-20 15:41:15 +02:00
|
|
|
let invars = InterfRead.ivars_of_extvalues w_list in
|
2011-06-07 10:49:36 +02:00
|
|
|
let pinvars = InterfRead.ivars_of_extvalues pw_list in
|
2012-06-20 09:17:13 +02:00
|
|
|
let outvars = InterfRead.def_ivars eq in
|
2011-06-07 10:49:36 +02:00
|
|
|
(* because of the encoding of the fold, the outputs are written before
|
|
|
|
the partially applied inputs are read so they must interfere *)
|
|
|
|
List.iter (fun inv -> List.iter (add_interference_link_from_ivar inv) outvars) pinvars;
|
|
|
|
(* affinities between inputs and outputs *)
|
2011-04-20 11:19:18 +02:00
|
|
|
List.iter (fun inv -> List.iter
|
2011-06-07 10:49:36 +02:00
|
|
|
(add_affinity_link_from_ivar inv) outvars) invars;
|
2011-04-27 14:52:37 +02:00
|
|
|
| Evarpat x, Eiterator((Ifold|Ifoldi), { a_op = Enode _ | Efun _ }, _, pw_list, w_list, _) ->
|
|
|
|
(* because of the encoding of the fold, the output is written before
|
|
|
|
the inputs are read so they must interfere *)
|
2011-05-02 16:40:42 +02:00
|
|
|
let w_list, _ = Misc.split_last w_list in
|
2011-04-27 14:52:37 +02:00
|
|
|
let invars = InterfRead.ivars_of_extvalues w_list in
|
|
|
|
let pinvars = InterfRead.ivars_of_extvalues pw_list in
|
|
|
|
List.iter (add_interference_link_from_ivar (Ivar x)) invars;
|
|
|
|
List.iter (add_interference_link_from_ivar (Ivar x)) pinvars
|
|
|
|
| Etuplepat l, Eiterator(Imapfold, { a_op = Enode _ | Efun _ }, _, pw_list, w_list, _) ->
|
2011-04-27 15:10:22 +02:00
|
|
|
let w_list, _ = Misc.split_last w_list in
|
|
|
|
let invars = InterfRead.ivars_of_extvalues w_list in
|
2011-04-27 14:52:37 +02:00
|
|
|
let pinvars = InterfRead.ivars_of_extvalues pw_list in
|
|
|
|
let outvars, acc_out = Misc.split_last (List.map InterfRead.ivar_of_pat l) in
|
|
|
|
(* because of the encoding of the fold, the output is written before
|
|
|
|
the inputs are read so they must interfere *)
|
|
|
|
List.iter (add_interference_link_from_ivar acc_out) invars;
|
|
|
|
List.iter (add_interference_link_from_ivar acc_out) pinvars;
|
2011-06-07 10:49:36 +02:00
|
|
|
(* because of the encoding of the fold, the outputs are written before
|
|
|
|
the partially applied inputs are read so they must interfere *)
|
|
|
|
List.iter (fun inv -> List.iter (add_interference_link_from_ivar inv) outvars) pinvars;
|
2011-04-27 14:52:37 +02:00
|
|
|
(* it also interferes with outputs. We add it here because it will not hold
|
|
|
|
if it is not used. *)
|
|
|
|
List.iter (add_interference_link_from_ivar acc_out) outvars;
|
2011-06-07 10:49:36 +02:00
|
|
|
(*affinity between inputs and outputs*)
|
2011-04-27 14:52:37 +02:00
|
|
|
List.iter (fun inv -> List.iter (add_affinity_link_from_ivar inv) outvars) invars
|
2011-04-20 15:41:15 +02:00
|
|
|
| Evarpat x, Efby(_, w) -> (* x = _ fby y *)
|
2011-10-04 14:34:36 +02:00
|
|
|
(try
|
|
|
|
add_affinity_link_from_ivar (InterfRead.ivar_of_extvalue w) (Ivar x)
|
|
|
|
with
|
|
|
|
| InterfRead.Const_extvalue -> ())
|
2012-06-20 09:17:13 +02:00
|
|
|
| Evarpat x, Eapp({ a_op = Eupdate }, args, _) ->
|
|
|
|
let w, _ = Misc.assert_1min args in
|
|
|
|
(try
|
|
|
|
add_affinity_link_from_ivar (InterfRead.ivar_of_extvalue w) (Ivar x)
|
|
|
|
with
|
|
|
|
| InterfRead.Const_extvalue -> ())
|
|
|
|
| Evarpat x, Eapp({ a_op = Efield_update }, args, _) ->
|
|
|
|
let w1, w2 = Misc.assert_2 args in
|
|
|
|
(* if we generate code for o = { a with .f = b } that is:
|
|
|
|
o=a; o.f = b
|
|
|
|
then we need to make sure that b interferes with all fields of o *)
|
|
|
|
if !Compiler_options.memcpy_array_and_struct then
|
|
|
|
(try
|
|
|
|
let all_iv = all_ivars [] (Ivar x) None w1.w_ty in
|
|
|
|
let iv2 = InterfRead.ivar_of_extvalue w2 in
|
|
|
|
List.iter (add_interference_link_from_ivar iv2) all_iv;
|
|
|
|
with
|
|
|
|
| InterfRead.Const_extvalue -> ());
|
2011-10-17 10:16:50 +02:00
|
|
|
(try
|
2012-06-20 09:17:13 +02:00
|
|
|
let iv1 = InterfRead.ivar_of_extvalue w1 in
|
|
|
|
add_affinity_link_from_ivar iv1 (Ivar x)
|
2011-10-17 10:16:50 +02:00
|
|
|
with
|
|
|
|
| InterfRead.Const_extvalue -> ())
|
2011-04-20 15:41:15 +02:00
|
|
|
| Evarpat x, Eextvalue w ->
|
2011-04-20 11:19:18 +02:00
|
|
|
(* Add links between variables with the same value *)
|
2011-10-04 14:34:36 +02:00
|
|
|
(try
|
|
|
|
add_same_value_link_from_ivar (InterfRead.ivar_of_extvalue w) (Ivar x)
|
|
|
|
with
|
|
|
|
| InterfRead.Const_extvalue -> ())
|
2011-04-20 11:19:18 +02:00
|
|
|
| _ -> () (* do nothing *)
|
|
|
|
|
|
|
|
(** Add the special init and return equations to the dependency graph
|
|
|
|
(resp at the bottom and top) *)
|
|
|
|
let add_init_return_eq f =
|
2012-06-20 09:17:13 +02:00
|
|
|
let pat_from_dec_list decs =
|
|
|
|
Etuplepat (List.map (fun vd -> Evarpat vd.v_ident) decs)
|
|
|
|
in
|
|
|
|
|
|
|
|
let tuple_from_dec_and_mem_list decs =
|
|
|
|
let exp_of_vd vd =
|
|
|
|
mk_extvalue ~clock:vd.v_clock ~ty:vd.v_type ~linearity:vd.v_linearity (Wvar vd.v_ident)
|
|
|
|
in
|
|
|
|
let exp_of_mem x = exp_of_vd (World.vd_from_ident x) in
|
|
|
|
let decs = List.map exp_of_vd decs in
|
|
|
|
let mems = IdentSet.fold (fun iv acc -> (exp_of_mem iv)::acc) !World.memories [] in
|
|
|
|
Eapp(mk_app Earray, decs@mems, None)
|
|
|
|
in
|
|
|
|
|
2011-04-20 11:19:18 +02:00
|
|
|
(** a_1,..,a_p = __init__ *)
|
2012-06-20 09:17:13 +02:00
|
|
|
let eq_init = mk_equation false (pat_from_dec_list f.n_input)
|
2011-09-07 17:51:31 +02:00
|
|
|
(mk_extvalue_exp Cbase Initial.tint Ltop (Wconst (Initial.mk_static_int 0))) in
|
2012-06-20 09:17:13 +02:00
|
|
|
(** __return__ = o_1,..,o_q, mem_1, ..., mem_k *)
|
2011-11-20 23:21:24 +01:00
|
|
|
let eq_return = mk_equation false (Etuplepat [])
|
2012-06-20 09:17:13 +02:00
|
|
|
(mk_exp Cbase Tinvalid Ltop (tuple_from_dec_and_mem_list f.n_output)) in
|
2011-04-20 11:19:18 +02:00
|
|
|
(eq_init::f.n_equs)@[eq_return]
|
|
|
|
|
|
|
|
|
|
|
|
let build_interf_graph f =
|
|
|
|
World.init f;
|
|
|
|
(** Init interference graph *)
|
2011-04-21 13:42:28 +02:00
|
|
|
init_interference_graph ();
|
2011-04-20 11:19:18 +02:00
|
|
|
|
|
|
|
let eqs = add_init_return_eq f in
|
|
|
|
(** Build live vars sets for each equation *)
|
|
|
|
let live_vars = compute_live_vars eqs in
|
|
|
|
(* Coalesce linear variables *)
|
2011-04-26 18:02:18 +02:00
|
|
|
coalesce_linear_vars ();
|
2011-04-20 11:19:18 +02:00
|
|
|
(** Other cases*)
|
|
|
|
List.iter process_eq f.n_equs;
|
|
|
|
(* Add interferences from live vars set*)
|
|
|
|
add_interferences live_vars;
|
|
|
|
(* Add interferences between records implied by IField values*)
|
|
|
|
add_records_field_interferences ();
|
2011-04-21 13:42:28 +02:00
|
|
|
(* Splill inputs that are not modified *)
|
|
|
|
spill_inputs f;
|
2012-01-24 10:29:05 +01:00
|
|
|
(* Spill outputs and memories that are not arrays or struts*)
|
|
|
|
if !Compiler_options.interf_all then
|
|
|
|
spill_mems_outputs f;
|
2011-04-20 11:19:18 +02:00
|
|
|
|
|
|
|
(* Return the graphs *)
|
|
|
|
!World.igs
|
2011-04-20 14:05:55 +02:00
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
(** Color the nodes corresponding to fields using
|
|
|
|
the color attributed to the record. This makes sure that
|
|
|
|
if a and b are shared, then a.f and b.f are too. *)
|
|
|
|
let color_fields ig =
|
|
|
|
let process n =
|
2011-04-20 15:41:15 +02:00
|
|
|
let fields = filter_fields !(G.V.label n) in
|
2011-04-20 14:05:55 +02:00
|
|
|
match fields with
|
|
|
|
| [] -> ()
|
|
|
|
| id::_ -> (* we only look at the first as they will all have the same color *)
|
2011-04-20 15:41:15 +02:00
|
|
|
let _, top_node = World.node_for_ivar id in
|
2011-04-20 14:05:55 +02:00
|
|
|
G.Mark.set n (G.Mark.get top_node)
|
|
|
|
in
|
|
|
|
G.iter_vertex process ig.g_graph
|
|
|
|
|
|
|
|
(** Color an interference graph.*)
|
|
|
|
let color_interf_graphs igs =
|
|
|
|
let record_igs, igs =
|
2011-04-20 15:41:15 +02:00
|
|
|
List.partition (fun ig -> is_record_type ig.g_type) igs in
|
2011-04-20 14:05:55 +02:00
|
|
|
(* First color interference graphs of record types *)
|
2011-04-21 10:44:25 +02:00
|
|
|
List.iter Dcoloring.color record_igs;
|
2011-04-20 14:05:55 +02:00
|
|
|
(* Then update fields colors *)
|
2011-04-20 15:41:15 +02:00
|
|
|
List.iter color_fields igs;
|
2011-04-20 14:05:55 +02:00
|
|
|
(* and finish the coloring *)
|
2011-04-21 10:44:25 +02:00
|
|
|
List.iter Dcoloring.color igs
|
2011-04-20 14:05:55 +02:00
|
|
|
|
2011-04-20 16:52:34 +02:00
|
|
|
let print_graphs f igs =
|
|
|
|
let cpt = ref 0 in
|
|
|
|
let print_graph ig =
|
|
|
|
let s = (Names.shortname f.n_name)^ (string_of_int !cpt) in
|
2011-04-21 10:44:25 +02:00
|
|
|
Interference2dot.print_graph (Names.fullname f.n_name) s ig;
|
2011-04-20 16:52:34 +02:00
|
|
|
cpt := !cpt + 1
|
|
|
|
in
|
|
|
|
List.iter print_graph igs
|
|
|
|
|
2011-04-20 14:05:55 +02:00
|
|
|
(** Create the list of lists of variables stored together,
|
|
|
|
from the interference graph.*)
|
|
|
|
let create_subst_lists igs =
|
|
|
|
let create_one_ig ig =
|
2011-04-21 10:44:25 +02:00
|
|
|
List.map (fun x -> ig.g_type, x) (Dcoloring.values_by_color ig)
|
2011-04-20 14:05:55 +02:00
|
|
|
in
|
|
|
|
List.flatten (List.map create_one_ig igs)
|
|
|
|
|
2011-04-20 16:52:34 +02:00
|
|
|
let node _ acc f =
|
2011-04-20 14:05:55 +02:00
|
|
|
(** Build the interference graphs *)
|
|
|
|
let igs = build_interf_graph f in
|
|
|
|
(** Color the graph *)
|
|
|
|
color_interf_graphs igs;
|
2011-04-21 16:49:58 +02:00
|
|
|
if print_interference_graphs then
|
2011-04-20 16:52:34 +02:00
|
|
|
print_graphs f igs;
|
2011-04-20 14:05:55 +02:00
|
|
|
(** Remember the choice we made for code generation *)
|
2011-04-20 15:41:15 +02:00
|
|
|
{ f with n_mem_alloc = create_subst_lists igs }, acc
|
2011-04-20 14:05:55 +02:00
|
|
|
|
|
|
|
let program p =
|
2011-04-20 15:41:15 +02:00
|
|
|
let funs = { Mls_mapfold.defaults with Mls_mapfold.node_dec = node } in
|
|
|
|
let p, _ = Mls_mapfold.program_it funs () p in
|
2011-04-20 14:05:55 +02:00
|
|
|
p
|