(** 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 error_prefix = "Clight32 to Clight8"
let error s = Error.global_error error_prefix s
let cint32s = Clight.Tint (Clight.I32, AST.Signed)
let cint32u = Clight.Tint (Clight.I32, AST.Unsigned)
let cint8s = Clight.Tint (Clight.I8, AST.Signed)
let cint8u = Clight.Tint (Clight.I8, AST.Unsigned)
(* Change the main so that it returns a 8 bits integer. Indeed, 32 bits integers
will be replaced by structures, and returning a structure from the main is
not Clight compliant. *)
let main_ret_type = function
| Clight.Tint (_, AST.Signed) -> cint8s
| Clight.Tint (_, AST.Unsigned) -> cint8u
| _ -> error "The main should return an integer which is not the case."
let f_ctype ctype _ = ctype
let f_expr e _ _ = e
let f_expr_descr ed _ _ = ed
let f_stmt ret_type stmt sub_exprs_res sub_stmts_res =
match stmt, sub_exprs_res with
| Clight.Sreturn (Some _), e :: _ ->
let e' = Clight.Expr (Clight.Ecast (ret_type, e), ret_type) in
Clight.Sreturn (Some e')
| _ -> ClightFold.statement_fill_subs stmt sub_exprs_res sub_stmts_res
let body_returns ret_type =
ClightFold.statement f_ctype f_expr f_expr_descr (f_stmt ret_type)
let fundef_returns_char = function
| Clight.Internal cfun ->
let ret_type = main_ret_type cfun.Clight.fn_return in
let body = body_returns ret_type cfun.Clight.fn_body in
Clight.Internal {cfun with Clight.fn_return = ret_type ;
Clight.fn_body = body }
| Clight.External _ as fundef -> fundef
let main_returns_char p = match p.Clight.prog_main with
| None -> p
| Some main ->
let main_def = List.assoc main p.Clight.prog_funct in
let main_def = fundef_returns_char main_def in
let prog_funct =
MiscPottier.update_list_assoc main main_def p.Clight.prog_funct in
{ p with Clight.prog_funct = prog_funct }
(* Replacement *)
let seq =
List.fold_left
(fun stmt1 stmt2 -> Clight.Ssequence (stmt1, stmt2))
Clight.Sskip
let is_complex = function
| Clight.Tstruct _ | Clight.Tunion _ -> true
| _ -> false
let is_subst_complex type_substitutions res_type =
if List.mem_assoc res_type type_substitutions then
is_complex (List.assoc res_type type_substitutions)
else false
let addrof_with_type e ctype =
let ctype = Clight.Tpointer ctype in
(Clight.Expr (Clight.Eaddrof e, ctype), ctype)
let address_if_subst_complex type_substitutions =
let f l (e, ctype) =
let arg_and_type =
if is_subst_complex type_substitutions ctype then addrof_with_type e ctype
else (e, ctype) in
l @ [arg_and_type] in
List.fold_left f []
let make_call_struct tmpe res_type f_var args args_types =
let (res_e, res_type) = addrof_with_type tmpe res_type in
let f_type = Clight.Tfunction (res_type :: args_types, Clight.Tvoid) in
let f = Clight.Expr (f_var, f_type) in
Clight.Scall (None, f, res_e :: args)
let make_call_wo_struct tmpe res_type f_var args args_types =
let f_type = Clight.Tfunction (args_types, res_type) in
let f = Clight.Expr (f_var, f_type) in
Clight.Scall (Some tmpe, f, args)
let make_call type_substitutions tmp f_id args_with_types res_type =
let tmpe = Clight.Expr (Clight.Evar tmp, res_type) in
let args_with_types =
address_if_subst_complex type_substitutions args_with_types in
let (args, args_types) = List.split args_with_types in
let f_var = Clight.Evar f_id in
let call =
if is_subst_complex type_substitutions res_type then make_call_struct
else make_call_wo_struct in
(tmpe, call tmpe res_type f_var args args_types)
let call fresh replaced type_substitutions replacement_assoc
args added_stmt added_tmps ret_type =
let tmp = fresh () in
let replacement_fun_name = List.assoc replaced replacement_assoc in
let (tmpe, call) =
make_call type_substitutions tmp replacement_fun_name args ret_type in
let stmt = seq (added_stmt @ [call]) in
(tmpe, stmt, added_tmps @ [(tmp, ret_type)])
let replace_ident replacement_assoc x t =
let new_name = match t with
| Clight.Tfunction _
when List.mem_assoc (Runtime.Fun x) replacement_assoc ->
let replacement_fun_name = List.assoc (Runtime.Fun x) replacement_assoc in
replacement_fun_name
| _ -> x in
(Clight.Expr (Clight.Evar new_name, t), Clight.Sskip, [])
let replace_expression fresh type_substitutions replacement_assoc e =
let rec aux (Clight.Expr (ed, t) as e) =
let expr ed = Clight.Expr (ed, t) in
match ed with
| Clight.Econst_int _ | Clight.Econst_float _ | Clight.Esizeof _ ->
(e, Clight.Sskip, [])
| Clight.Evar x -> replace_ident replacement_assoc x t
| 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') as e'))
when List.mem_assoc (Runtime.Unary (unop, t')) replacement_assoc ->
let (e', stmt, tmps) = aux e' in
call fresh (Runtime.Unary (unop, t'))
type_substitutions replacement_assoc [(e', t')]
[stmt] tmps t
| Clight.Eunop (unop, e') ->
let (e', stmt, tmps) = aux e' in
(expr (Clight.Eunop (unop, e')), stmt, tmps)
| Clight.Ebinop (binop,
(Clight.Expr (ed1, t1) as e1),
(Clight.Expr (ed2, t2) as e2))
when
List.mem_assoc (Runtime.Binary (binop, t1, t2)) replacement_assoc ->
let (e1, stmt1, tmps1) = aux e1 in
let (e2, stmt2, tmps2) = aux e2 in
call fresh (Runtime.Binary (binop, t1, t2))
type_substitutions replacement_assoc
[(e1, t1) ; (e2, t2)] [stmt1 ; stmt2] (tmps1 @ tmps2) t
| Clight.Ebinop (binop, e1, e2) ->
let (e1, stmt1, tmps1) = aux e1 in
let (e2, stmt2, tmps2) = aux e2 in
let stmt = seq [stmt1 ; stmt2] in
(expr (Clight.Ebinop (binop, e1, e2)), stmt, tmps1 @ tmps2)
| Clight.Ecast (t, (Clight.Expr (_, t') as e'))
when List.mem_assoc (Runtime.Cast (t, t')) replacement_assoc ->
let (e', stmt, tmps) = aux e' in
call fresh (Runtime.Cast (t, t'))
type_substitutions replacement_assoc [(e', t')] [stmt]
tmps t
| Clight.Ecast (t', e') ->
let (e', stmt, tmps) = aux e' in
(expr (Clight.Ecast (t', e')), stmt, tmps)
| Clight.Econdition (e1, e2, e3) ->
let (e1, stmt1, tmps1) = aux e1 in
let (e2, stmt2, tmps2) = aux e2 in
let (e3, stmt3, tmps3) = aux e3 in
let stmt = seq [stmt1 ; stmt2 ; stmt3] in
(expr (Clight.Econdition (e1, e2, e3)), stmt, tmps1 @ tmps2 @ tmps3)
| Clight.Eandbool (e1, e2) ->
let (e1, stmt1, tmps1) = aux e1 in
let (e2, stmt2, tmps2) = aux e2 in
let stmt = seq [stmt1 ; stmt2] in
(expr (Clight.Eandbool (e1, e2)), stmt, tmps1 @ tmps2)
| Clight.Eorbool (e1, e2) ->
let (e1, stmt1, tmps1) = aux e1 in
let (e2, stmt2, tmps2) = aux e2 in
let stmt = seq [stmt1 ; stmt2] in
(expr (Clight.Eorbool (e1, e2)), stmt, tmps1 @ tmps2)
| Clight.Efield (e', field) ->
let (e', stmt, tmps) = aux e' in
(expr (Clight.Efield (e', field)), stmt, tmps)
| Clight.Ecost (lbl, e') ->
let (e', stmt, tmps) = aux e' in
(expr (Clight.Ecost (lbl, e')), stmt, tmps)
| Clight.Ecall (id, e1, e2) ->
let (e1, stmt1, tmps1) = aux e1 in
let (e2, stmt2, tmps2) = aux e2 in
let stmt = seq [stmt1 ; stmt2] in
(expr (Clight.Ecall (id, e1, e2)), stmt, tmps1 @ tmps2)
in
aux e
let replace_expression_list fresh type_substitutions replacement_assoc =
let f (l, stmt, tmps) e =
let (e', stmt', tmps') =
replace_expression fresh type_substitutions replacement_assoc e in
(l @ [e'], seq [stmt ; stmt'], tmps @ tmps') in
List.fold_left f ([], Clight.Sskip, [])
let replace_statement fresh type_substitutions replacement_assoc =
let aux_exp =
replace_expression fresh type_substitutions replacement_assoc in
let aux_exp_list =
replace_expression_list fresh type_substitutions replacement_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 [stmt3' ; stmt2' ; 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 f_ctype type_substitutions ctype sub_ctypes_res = match ctype with
| _ when List.mem_assoc ctype type_substitutions ->
List.assoc ctype type_substitutions
| _ -> ClightFold.ctype_fill_subs ctype sub_ctypes_res
let replace_ctype type_substitutions =
ClightFold.ctype (f_ctype type_substitutions)
let f_expr = ClightFold.expr_fill_subs
let f_expr_descr = ClightFold.expr_descr_fill_subs
let f_stmt = ClightFold.statement_fill_subs
let statement_replace_ctype type_substitutions =
ClightFold.statement (f_ctype type_substitutions) f_expr f_expr_descr f_stmt
let replace_internal fresh type_substitutions replacement_assoc def =
let (new_body, tmps) =
replace_statement fresh type_substitutions replacement_assoc
def.Clight.fn_body in
let new_body = statement_replace_ctype type_substitutions new_body in
let f (x, t) = (x, replace_ctype type_substitutions t) in
let params = List.map f def.Clight.fn_params in
let vars = List.map f (def.Clight.fn_vars @ tmps) in
{ Clight.fn_return = replace_ctype type_substitutions def.Clight.fn_return ;
Clight.fn_params = params ;
Clight.fn_vars = vars ;
Clight.fn_body = new_body }
let replace_funct fresh type_substitutions replacement_assoc (id, fundef) =
let fundef' = match fundef with
| Clight.Internal def ->
Clight.Internal
(replace_internal fresh type_substitutions replacement_assoc def)
| _ -> fundef in
(id, fundef')
let replace fresh type_substitutions replacement_assoc p =
let prog_funct =
List.map (replace_funct fresh type_substitutions replacement_assoc)
p.Clight.prog_funct in
{ p with Clight.prog_funct = prog_funct }
(* The constant replacement replaces each 32 bits and 16 bits integer constant
by a global variable of the same value. They will be replaced by the
appropriate structural value by the global replacement that comes
afterwards. *)
module CstMap =
Map.Make
(struct
type t = (int * Clight.intsize * Clight.ctype)
let compare = Pervasives.compare
end)
let f_subs fresh replace subs map =
let f (l, map) x =
let (x, map) = replace fresh map x in
(l @ [x], map) in
List.fold_left f ([], map) subs
let rec replace_constant_expr fresh map (Clight.Expr (ed, t) as e) =
match ed, t with
| Clight.Econst_int i, Clight.Tint (Clight.I8, _) ->
(e, map)
| Clight.Econst_int i, Clight.Tint (size, _)
when CstMap.mem (i, size, t) map ->
let id = CstMap.find (i, size, t) map in
(Clight.Expr (Clight.Evar id, t), map)
| Clight.Econst_int i, Clight.Tint (size, _) ->
let id = fresh () in
let map = CstMap.add (i, size, t) id map in
let id = CstMap.find (i, size, t) map in
(Clight.Expr (Clight.Evar id, t), map)
| _ ->
let (sub_ctypes, sub_exprs) = ClightFold.expr_descr_subs ed in
let (sub_exprs, map) = f_subs fresh replace_constant_expr sub_exprs map in
let ed = ClightFold.expr_descr_fill_subs ed sub_ctypes sub_exprs in
(Clight.Expr (ed, t), map)
let rec replace_constant_stmt fresh map stmt =
let (sub_exprs, sub_stmts) = ClightFold.statement_subs stmt in
let (sub_exprs, map) =
f_subs fresh replace_constant_expr sub_exprs map in
let (sub_stmts, map) =
f_subs fresh replace_constant_stmt sub_stmts map in
(ClightFold.statement_fill_subs stmt sub_exprs sub_stmts, map)
let replace_constant_fundef fresh (functs, map) (id, fundef) =
match fundef with
| Clight.Internal cfun ->
let (body, map) = replace_constant_stmt fresh map cfun.Clight.fn_body in
let fundef = Clight.Internal { cfun with Clight.fn_body = body } in
(functs @ [(id, fundef)], map)
| Clight.External _ -> (functs @ [(id, fundef)], map)
let init_datas i size =
[match size with
| Clight.I8 -> Clight.Init_int8 i
| Clight.I16 -> Clight.Init_int16 i
| Clight.I32 -> Clight.Init_int32 i]
let globals_of_map map =
let f (i, size, t) id l = l @ [((id, init_datas i size), t)] in
CstMap.fold f map []
let replace_constant p =
let tmp_universe = ClightAnnotator.fresh_universe "_cst" p in
let fresh () = StringTools.Gen.fresh tmp_universe in
let (functs, map) =
List.fold_left (replace_constant_fundef fresh)
([], CstMap.empty) p.Clight.prog_funct in
let csts = globals_of_map map in
{ p with
Clight.prog_funct = functs ; Clight.prog_vars = p.Clight.prog_vars @ csts }
(* Globals replacement *)
let expand_int size i =
let i = Big_int.big_int_of_int i in
let i =
if Big_int.ge_big_int i Big_int.zero_big_int then i
else Big_int.add_big_int i (Big_int.power_int_positive_int 2 size) in
let bound = Big_int.power_int_positive_int 2 8 in
let rec aux n i =
if n >= size then []
else
let (next, chunk) = Big_int.quomod_big_int i bound in
chunk :: (aux (n+1) next) in
List.map (fun i -> Clight.Init_int8 (Big_int.int_of_big_int i)) (aux 0 i)
let expand_init_data = function
| Clight.Init_int16 i -> expand_int 2 i
| Clight.Init_int32 i -> expand_int 4 i
| init_data -> [init_data]
let expand_init_datas init_datas =
List.flatten (List.map expand_init_data init_datas)
let replace_global type_substitutions ((id, init_datas), t) =
let init_datas = expand_init_datas init_datas in
((id, init_datas), replace_ctype type_substitutions t)
let replace_globals type_substitutions p =
let vars = List.map (replace_global type_substitutions) p.Clight.prog_vars in
{ p with Clight.prog_vars = vars }
(* Unsupported operations by the 8051. *)
(* 8 bits signed division *)
let divs_fun s _ =
"signed char " ^ s ^ " (signed char x, signed char y) {\n" ^
" unsigned char x1 = (unsigned char) x;\n" ^
" unsigned char y1 = (unsigned char) y;\n" ^
" signed char sign = 1;\n" ^
" if (x < 0) { x1 = (unsigned char) (-x); sign = -sign; }\n" ^
" if (y < 0) { y1 = (unsigned char) (-y); sign = -sign; }\n" ^
" return (sign * ((signed char) (x1/y1)));\n" ^
"}\n\n"
let divs =
(Runtime.Binary (Clight.Odiv, cint8s, cint8s), "_divs", [], divs_fun, [])
(* 8 bits signed modulo *)
let mods_fun s _ =
"signed char " ^ s ^ " (signed char x, signed char y) {\n" ^
" return (x - (x/y) * y);\n" ^
"}\n\n"
let mods =
(Runtime.Binary (Clight.Omod, cint8s, cint8s), "_mods", [], mods_fun,
[Runtime.Binary (Clight.Odiv, cint8s, cint8s)])
(* Shifts *)
let sh_fun signedness op s _ =
signedness ^ " char " ^ s ^ " (" ^ signedness ^ " char x, " ^
signedness ^ " char y) {\n" ^
" " ^ signedness ^ " char res = x, i;\n" ^
" for (i = 0 ; i < y ; i++) res = res " ^ op ^ " 2;\n" ^
" return res;\n" ^
"}\n\n"
(* 8 bits shifts left *)
let shls_fun = sh_fun "signed" "*"
let shls =
(Runtime.Binary (Clight.Oshl, cint8s, cint8s), "_shls", [], shls_fun, [])
let shlu_fun s _ =
"unsigned char " ^ s ^ " (unsigned char x, unsigned char y) {\n" ^
" return ((unsigned char) ((signed char) x << (signed char) y));\n" ^
"}\n\n"
let shlu =
(Runtime.Binary (Clight.Oshl, cint8u, cint8u), "_shlu", [], shlu_fun,
[Runtime.Binary (Clight.Oshl, cint8s, cint8s)])
(* 8 bits shifts right *)
let shrs_fun s _ =
"signed char " ^ s ^ " (signed char x, signed char y) {\n" ^
" signed char res = x, i;\n" ^
" for (i = 0 ; i < y ; i++) {\n" ^
" res = ((unsigned char) res) / 2;\n" ^
" res = res + ((signed char) 128);\n" ^
" }\n" ^
" return res;\n" ^
"}\n\n"
let shrs =
(Runtime.Binary (Clight.Oshr, cint8s, cint8s), "_shrs", [], shrs_fun, [])
let shru_fun = sh_fun "unsigned" "/"
let shru =
(Runtime.Binary (Clight.Oshr, cint8u, cint8u), "_shru", [], shru_fun, [])
(* int32 *)
let struct_int32 name fields = match fields with
| lolo :: lohi :: hilo :: hihi :: _ ->
Clight.Tstruct
(name,
[(lolo, cint8u) ; (lohi, cint8u) ; (hilo, cint8u) ; (hihi, cint8u)])
| _ -> error ("bad field names when defining type " ^ name ^ ".")
let struct_int32_name = "struct _int32_"
let new_int32 int32 =
let lolo = "lolo" in
let lohi = "lohi" in
let hilo = "hilo" in
let hihi = "hihi" in
(int32, struct_int32_name, [lolo ; lohi ; hilo ; hihi], struct_int32)
let int32s = new_int32 (Clight.Tint (Clight.I32, AST.Signed))
let int32u = new_int32 (Clight.Tint (Clight.I32, AST.Unsigned))
(* 32 bits operations *)
(* 32 bits equality *)
let eq_int32s_fun s l =
let (int32, lolo, lohi, hilo, hihi) = match l with
| (int32, lolo :: lohi :: hilo :: hihi :: _) :: _ ->
(int32, lolo, lohi, hilo, hihi)
| _ -> error ("new type definition not coherent in function " ^ s ^ ".") in
int32 ^ " " ^ s ^ " (" ^ int32 ^ " x, " ^ int32 ^ " y) {\n" ^
" " ^ int32 ^ " res;\n" ^
" res." ^ lolo ^ " = 1;\n" ^
" if (x." ^ lolo ^ " != y." ^ lolo ^ ") res." ^ lolo ^ " = 0;\n" ^
" if (x." ^ lohi ^ " != y." ^ lohi ^ ") res." ^ lolo ^ " = 0;\n" ^
" if (x." ^ hilo ^ " != y." ^ hilo ^ ") res." ^ lolo ^ " = 0;\n" ^
" if (x." ^ hihi ^ " != y." ^ hihi ^ ") res." ^ lolo ^ " = 0;\n" ^
" res." ^ lohi ^ " = 0;\n" ^
" res." ^ hilo ^ " = 0;\n" ^
" res." ^ hihi ^ " = 0;\n" ^
" return (res);\n" ^
"}\n\n"
let eq32s =
(Runtime.Binary (Clight.Oeq, cint32s, cint32s), "eq_int32s",
[struct_int32_name], eq_int32s_fun, [])
(* 32 bits casts *)
let int32s_to_int8s_fun s l =
let (int32, lolo, lohi, hilo, hihi) = match l with
| (int32, lolo :: lohi :: hilo :: hihi :: _) :: _ ->
(int32, lolo, lohi, hilo, hihi)
| _ -> error ("new type definition not coherent in function " ^ s ^ ".") in
"signed char " ^ s ^ " (" ^ int32 ^ " x) {\n" ^
" return ((signed char) x." ^ lolo ^ ");\n" ^
"}\n\n"
let int32s_to_int8s =
(Runtime.Cast (cint8s, cint32s), "int32s_to_int8s", [struct_int32_name],
int32s_to_int8s_fun, [])
(* int16 *)
let struct_int16 name fields = match fields with
| lo :: hi :: _ ->
Clight.Tstruct (name, [(lo, cint8u) ; (hi, cint8u)])
| _ -> error ("bad field names when defining type " ^ name ^ ".")
let struct_int16_name = "struct _int16_"
let new_int16 int16 =
let lo = "lo" in
let hi = "hi" in
(int16, struct_int16_name, [lo ; hi], struct_int16)
let int16s = new_int16 (Clight.Tint (Clight.I16, AST.Signed))
let int16u = new_int16 (Clight.Tint (Clight.I16, AST.Unsigned))
(* int32 and int16 *)
let int32_and_int16_types = [int32s ; int32u ; int16s ; int16u]
let int32_and_int16_replacements = [eq32s ; int32s_to_int8s]
let unsupported = [divs ; mods ; shls ; shlu ; shrs ; shru]
let save_and_parse p =
let tmp_file = Filename.temp_file "clight32toclight8" ".c" in
try
let oc = open_out tmp_file in
output_string oc (ClightPrinter.print_program p) ;
close_out oc ;
let res = ClightParser.process tmp_file in
Misc.SysExt.safe_remove tmp_file ;
res
with Sys_error _ -> failwith "Error reparsing Clight8 transformation."
let add_replacements p new_types replacements =
let p = ClightCasts.simplify p in
let (p, type_substitutions, replacement_assoc) =
Runtime.add p new_types replacements in
let p = ClightCasts.simplify p in
let tmp_universe = ClightAnnotator.fresh_universe "_tmp" p in
let fresh () = StringTools.Gen.fresh tmp_universe in
let p = replace fresh type_substitutions replacement_assoc p in
let p = replace_globals type_substitutions p in
(* Printf.printf "%s\n%!" (ClightPrinter.print_program p) ; *)
let p = save_and_parse p in
ClightCasts.simplify p
let translate p =
let p = main_returns_char p in
let p = replace_constant p in
let p =
add_replacements p int32_and_int16_types int32_and_int16_replacements in
add_replacements p [] unsupported