CristalCaveGem » LustreC

open LustreSpec 

open Corelang

open Machine_code 

let rec eliminate elim instr =

  let e_expr = eliminate_expr elim in

  match instr with  

  | MLocalAssign (i,v) -> MLocalAssign (i, e_expr v)

  | MStateAssign (i,v) -> MStateAssign (i, e_expr v)

  | MReset i           -> instr

  | MStep (il, i, vl)  -> MStep(il, i, List.map e_expr vl)

  | MBranch (g,hl)     -> 

    MBranch

      (e_expr g, 

       (List.map 

	  (fun (l, il) -> l, List.map (eliminate elim) il) 

	  hl

       )

      )

and eliminate_expr elim expr =

  match expr with

  | LocalVar v -> if List.mem_assoc v elim then List.assoc v elim else expr

  | Fun (id, vl) -> Fun (id, List.map (eliminate_expr elim) vl)

  | Array(vl) -> Array(List.map (eliminate_expr elim) vl)

  | Access(v1, v2) -> Access(eliminate_expr elim v1, eliminate_expr elim v2)

  | Power(v1, v2) -> Access(eliminate_expr elim v1, eliminate_expr elim v2)

  | Cst _ | StateVar _ -> expr

(* see if elim has to take in account the provided instr:

   if so, upodate elim and return the remove flag,

   otherwise, the expression should be kept and elim is left untouched *)

let update_elim elim instr =

  Format.eprintf "SHOULD WE STORE THE EXPRESSION IN INSTR %a TO ELIMINATE IT@." pp_instr instr;

  let apply elim v new_e = 

    (v, new_e)::List.map (fun (v, e) -> v, eliminate_expr [v, new_e] e) elim 

  in

  match instr with

  (* Simple cases*)

  | MLocalAssign (v, (Cst _ as e)) 

  | MLocalAssign (v, (LocalVar _ as e)) 

  | MLocalAssign (v, (StateVar _ as e)) -> true, apply elim v e

  (* When optimization >= 3, we also inline any basic operator call. 

     All those are returning a single ouput *)

  | MStep([v], id, vl) when

      List.mem id Basic_library.internal_funs 

      && !Options.optimization >= 3

      -> 	  assert false 

(*    true, apply elim v (Fun(id, vl))*)

  | MLocalAssign (v, ((Fun (id, il)) as e)) when 

      List.mem id Basic_library.internal_funs (* this will avoid inlining ite *)

      && !Options.optimization >= 3 

	-> (

	  Format.eprintf "WE STORE THE EXPRESSION DEFINING %s TO ELIMINATE IT@." v.var_id;

	  true, apply elim v e

	)

  | _ -> 

    (* default case, we keep the instruction and do not modify elim *)

    false, elim

(** We iterate in the order, recording simple local assigns in an accumulator

    1. each expression is rewritten according to the accumulator

    2. local assigns then rewrite occurrences of the lhs in the computed accumulator

*)

let optimize_minstrs instrs = 

  let rev_instrs, eliminate = 

    List.fold_left (fun (rinstrs, elim) instr ->

      (* each subexpression in instr that could be rewritten by the elim set is

	 rewritten *)

      let instr = eliminate elim instr in

      (* if instr is a simple local assign, then (a) elim is simplified with it (b) it

	 is stored as the elim set *)

      let remove, elim = update_elim elim instr in

      (if remove then rinstrs else instr::rinstrs), elim

    ) ([],[]) instrs 

  in

  let eliminated_vars = List.map fst eliminate in

  eliminated_vars, List.rev rev_instrs

(** Perform optimization on machine code:

    - iterate through step instructions and remove simple local assigns

*)

let optimize_machine machine =

  let eliminated_vars, new_instrs = optimize_minstrs machine.mstep.step_instrs in

  let new_locals = 

    List.filter (fun v -> not (List.mem v eliminated_vars)) machine.mstep.step_locals 

  in

  {

    machine with

      mstep = { 

	machine.mstep with 

	  step_locals = new_locals;

	  step_instrs = new_instrs

      }

  }

let optimize_machines machines =

  List.map optimize_machine machines

(* Local Variables: *)

(* compile-command:"make -C .." *)

(* End: *)

open Corelang

(* Consts unfoooolding *)

let is_const i consts = 

  List.exists (fun c -> c.const_id = i) consts

let get_const i consts =

  let c = List.find (fun c -> c.const_id = i) consts in

  c.const_value

let rec expr_unfold_consts consts e = 

{ e with expr_desc = expr_desc_unfold_consts consts e.expr_desc }

and expr_desc_unfold_consts consts e =

  let unfold = expr_unfold_consts consts in

  match e with

  | Expr_const _ -> e

  | Expr_ident i -> if is_const i consts then Expr_const (get_const i consts) else e

  | Expr_array el -> Expr_array (List.map unfold el)

  | Expr_access (e1, d) -> Expr_access (unfold e1, d)

  | Expr_power (e1, d) -> Expr_power (unfold e1, d)

  | Expr_tuple el -> Expr_tuple (List.map unfold el)

  | Expr_ite (c, t, e) -> Expr_ite (unfold c, unfold t, unfold e)

  | Expr_arrow (e1, e2)-> Expr_arrow (unfold e1, unfold e2) 

  | Expr_fby (e1, e2) -> Expr_fby (unfold e1, unfold e2)

  (* | Expr_concat (e1, e2) -> Expr_concat (unfold e1, unfold e2) *)

  (* | Expr_tail e' -> Expr_tail (unfold e') *)

  | Expr_pre e' -> Expr_pre (unfold e')

  | Expr_when (e', i, l)-> Expr_when (unfold e', i, l)

  | Expr_merge (i, hl) -> Expr_merge (i, List.map (fun (t, h) -> (t, unfold h)) hl)

  | Expr_appl (i, e', i') -> Expr_appl (i, unfold e', i')

  | Expr_uclock (e', i) -> Expr_uclock (unfold e', i) 

  | Expr_dclock (e', i) -> Expr_dclock (unfold e', i)

  | Expr_phclock _ -> e  

let eq_unfold_consts consts eq =

  { eq with eq_rhs = expr_unfold_consts consts eq.eq_rhs }

let node_unfold_consts consts node = 

  { node with node_eqs = List.map (eq_unfold_consts consts) node.node_eqs }

let prog_unfold_consts prog =

  let consts = get_consts prog in

    List.map (

      fun decl -> match decl.top_decl_desc with 

	| Node nd -> {decl with top_decl_desc = Node (node_unfold_consts consts nd)}

	| _       -> decl

    ) prog 

(* Local Variables: *)

(* compile-command:"make -C .." *)

(* End: *)