(** This module performs a transformation of a [Clight] program with potentially
32 and 16 bits integers to an equivalent [Clight] program that only uses 8
bits integers.
The main changes are: defining two types that represent 32 and 16 bits
integers with a structure of 8 bits integers, making the substitution,
replacing primitive integer operations on 32 and 16 bits integers with new
functions emulating them on the new types, and finally defining a global
variable for each 32 and 16 bits integer constant, which is then replaced by
its associated variable. *)
let rec seq = function
| [] -> Clight.Sskip
| [stmt] -> stmt
| stmt :: l -> Clight.Ssequence (stmt, seq l)
let call tmp f_id args_and_type res_type =
let tmpe = Clight.Expr (Clight.Evar tmp, res_type) in
let (args, args_type) = List.split args_and_type in
let f_var = Clight.Evar f_id in
let f_type = Clight.Tfunction (args_type, res_type) in
let f = Clight.Expr (f_var, f_type) in
(tmpe, Clight.Scall (Some tmpe, f, args))
let replace_primitives_expression fresh unop_assoc binop_assoc =
let rec aux e =
let Clight.Expr (ed, t) = e in
let expr ed = Clight.Expr (ed, t) in
match ed with
| Clight.Econst_int _ | Clight.Econst_float _ | Clight.Evar _
| Clight.Esizeof _ ->
(e, Clight.Sskip, [])
| Clight.Ederef e ->
let (e', stmt, tmps) = aux e in
(expr (Clight.Ederef e'), stmt, tmps)
| Clight.Eaddrof e ->
let (e', stmt, tmps) = aux e in
(expr (Clight.Eaddrof e'), stmt, tmps)
| Clight.Eunop (unop, Clight.Expr (ed', t'))
when List.mem_assoc (unop, t') unop_assoc ->
let (e', stmt, tmps) = aux (Clight.Expr (ed', t')) in
let tmp = fresh () in
let (tmpe, call) =
call tmp (List.assoc (unop, t') unop_assoc) [(e', t')] t in
let stmt = seq [stmt ; call] in
(tmpe, stmt, tmps @ [(tmp, t)])
| Clight.Ebinop (binop, Clight.Expr (ed1, t1), Clight.Expr (ed2, t2))
when List.mem_assoc (binop, t1, t2) binop_assoc ->
let (e1, stmt1, tmps1) = aux (Clight.Expr (ed1, t1)) in
let (e2, stmt2, tmps2) = aux (Clight.Expr (ed2, t2)) in
let tmp = fresh () in
let (tmpe, call) =
call tmp (List.assoc (binop, t1, t2) binop_assoc)
[(e1, t1) ; (e2, t2)] t in
let stmt = seq [stmt1 ; stmt2 ; call] in
(tmpe, stmt, tmps1 @ tmps2 @ [(tmp, t)])
| _ -> (e, Clight.Sskip, []) (* TODO *)
in
aux
let replace_primitives_expression_list fresh unop_assoc binop_assoc =
let f (l, stmt, tmps) e =
let (e', stmt', tmps') =
replace_primitives_expression fresh unop_assoc binop_assoc e in
(l @ [e], seq [stmt ; stmt'], tmps @ tmps') in
List.fold_left f ([], Clight.Sskip, [])
let replace_primitives_statement fresh unop_assoc binop_assoc =
let aux_exp =
replace_primitives_expression fresh unop_assoc binop_assoc in
let aux_exp_list =
replace_primitives_expression_list fresh unop_assoc binop_assoc in
let rec aux = function
| Clight.Sskip | Clight.Sbreak | Clight.Scontinue | Clight.Sgoto _
| Clight.Sreturn None
as stmt -> (stmt, [])
| Clight.Slabel (lbl, stmt) ->
let (stmt', tmps) = aux stmt in
(Clight.Slabel (lbl, stmt'), tmps)
| Clight.Scost (lbl, stmt) ->
let (stmt', tmps) = aux stmt in
(Clight.Scost (lbl, stmt'), tmps)
| Clight.Sassign (e1, e2) ->
let (e1', stmt1, tmps1) = aux_exp e1 in
let (e2', stmt2, tmps2) = aux_exp e2 in
let stmt = seq [stmt1 ; stmt2 ; Clight.Sassign (e1', e2')] in
(stmt, tmps1 @ tmps2)
| Clight.Scall (None, f, args) ->
let (f', stmt1, tmps1) = aux_exp f in
let (args', stmt2, tmps2) = aux_exp_list args in
let stmt = seq [stmt1 ; stmt2 ; Clight.Scall (None, f', args')] in
(stmt, tmps1 @ tmps2)
| Clight.Scall (Some e, f, args) ->
let (e', stmt1, tmps1) = aux_exp e in
let (f', stmt2, tmps2) = aux_exp f in
let (args', stmt3, tmps3) = aux_exp_list args in
let stmt = seq [stmt1 ; stmt2 ; stmt3 ;
Clight.Scall (Some e', f', args')] in
(stmt, tmps1 @ tmps2 @ tmps3)
| Clight.Sifthenelse (e, stmt1, stmt2) ->
let (e', stmte, tmpse) = aux_exp e in
let (stmt1', tmps1) = aux stmt1 in
let (stmt2', tmps2) = aux stmt2 in
let stmt = seq [stmte ; Clight.Sifthenelse (e', stmt1', stmt2')] in
(stmt, tmpse @ tmps1 @ tmps2)
| Clight.Swhile (e, stmt) ->
let (e', stmte, tmpse) = aux_exp e in
let (stmt', tmps) = aux stmt in
let stmt = seq [stmte ; Clight.Swhile (e', seq [stmt' ; stmte])] in
(stmt, tmpse @ tmps)
| Clight.Sdowhile (e, stmt) ->
let (e', stmte, tmpse) = aux_exp e in
let (stmt', tmps) = aux stmt in
let stmt = seq [Clight.Sdowhile (e', seq [stmt' ; stmte])] in
(stmt, tmpse @ tmps)
| Clight.Sfor (stmt1, e, stmt2, stmt3) ->
let (e', stmte, tmpse) = aux_exp e in
let (stmt1', tmps1) = aux stmt1 in
let (stmt2', tmps2) = aux stmt2 in
let (stmt3', tmps3) = aux stmt3 in
let stmt = seq [stmt1' ; stmte ;
Clight.Swhile (e', seq [stmt2' ; stmt3' ; stmte])] in
(stmt, tmpse @ tmps1 @ tmps2 @ tmps3)
| Clight.Sswitch (e, lbl_stmts) ->
let (e', stmte, tmpse) = aux_exp e in
let (lbl_stmts', tmps) = aux_lbl_stmts lbl_stmts in
let stmt = seq [stmte ; Clight.Sswitch (e', lbl_stmts')] in
(stmt, tmpse @ tmps)
| Clight.Sreturn (Some e) ->
let (e', stmte, tmpse) = aux_exp e in
let stmt = seq [stmte ; Clight.Sreturn (Some e')] in
(stmt, tmpse)
| Clight.Ssequence (stmt1, stmt2) ->
let (stmt1', tmps1) = aux stmt1 in
let (stmt2', tmps2) = aux stmt2 in
let stmt = seq [stmt1' ; stmt2'] in
(stmt, tmps1 @ tmps2)
and aux_lbl_stmts = function
| Clight.LSdefault stmt ->
let (stmt', tmps) = aux stmt in
(Clight.LSdefault stmt', tmps)
| Clight.LScase (i, stmt, lbl_stmts) ->
let (stmt', tmps1) = aux stmt in
let (lbl_stmts', tmps2) = aux_lbl_stmts lbl_stmts in
(Clight.LScase (i, stmt', lbl_stmts'), tmps1 @ tmps2)
in
aux
let replace_primitives_internal fresh unop_assoc binop_assoc def =
let (new_body, tmps) =
replace_primitives_statement fresh unop_assoc binop_assoc
def.Clight.fn_body in
{ def with Clight.fn_vars = def.Clight.fn_vars @ tmps ;
Clight.fn_body = new_body }
let replace_primitives_funct fresh unop_assoc binop_assoc (id, fundef) =
let fundef' = match fundef with
| Clight.Internal def ->
Clight.Internal
(replace_primitives_internal fresh unop_assoc binop_assoc def)
| _ -> fundef in
(id, fundef')
let replace_primitives fresh unop_assoc binop_assoc p =
let prog_funct =
List.map (replace_primitives_funct fresh unop_assoc binop_assoc)
p.Clight.prog_funct in
{ p with Clight.prog_funct = prog_funct }
let translate p =
let (p, unop_assoc, binop_assoc) = Runtime.add p in
let p = ClightCasts.simplify p in
let labs = ClightAnnotator.all_labels p in
let tmp_prefix = StringTools.Gen.fresh_prefix labs "_tmp" in
let tmp_universe = StringTools.Gen.new_universe tmp_prefix in
let fresh () = StringTools.Gen.fresh tmp_universe in
let p = replace_primitives fresh unop_assoc binop_assoc p in
(* TODO: do the translation *)
p