diff --git a/compiler/src/toEC.ml b/compiler/src/toEC.ml index f5610ec19..0f2597e59 100644 --- a/compiler/src/toEC.ml +++ b/compiler/src/toEC.ml @@ -4,21 +4,17 @@ open Prog open PrintCommon module E = Expr -let rec pp_list_pre sep pp fmt xs = - let pp_list_pre = pp_list_pre sep pp in - match xs with - | [] -> () - | [x] -> Format.fprintf fmt "%(%)%a" sep pp x - | x :: xs -> Format.fprintf fmt "%(%)%a%a" sep pp x pp_list_pre xs +let pp_option pp fmt = function + | Some x -> pp fmt x + | None -> () -let pp_size fmt sz = - Format.fprintf fmt "%i" (int_of_ws sz) +let pp_list_paren sep pp fmt xs = + if xs = [] then () + else pp_paren (pp_list sep pp) fmt xs -let pp_Tsz fmt sz = - Format.fprintf fmt "W%a" pp_size sz +let pp_Tsz sz = Format.asprintf "W%i" (int_of_ws sz) -let pp_sz_t fmt sz = - Format.fprintf fmt "%a.t" pp_Tsz sz +let pp_sz_t sz = Format.sprintf "W%i.t" (int_of_ws sz) module Scmp = struct type t = string @@ -36,6 +32,7 @@ end module Mty = Map.Make (Tcmp) type env = { + pd : Wsize.wsize; model : model; alls : Ss.t; vars : string Mv.t; @@ -47,63 +44,6 @@ type env = { randombytes : Sint.t ref; } -(* --------------------------------------------------------------- *) - -let rec read_mem_e = function - | Pconst _ | Pbool _ | Parr_init _ |Pvar _ -> false - | Pload _ -> true - | Papp1 (_, e) | Pget (_, _, _, _, e) | Psub (_, _, _, _, e) -> read_mem_e e - | Papp2 (_, e1, e2) -> read_mem_e e1 || read_mem_e e2 - | PappN (_, es) -> read_mem_es es - | Pif (_, e1, e2, e3) -> read_mem_e e1 || read_mem_e e2 || read_mem_e e3 - -and read_mem_es es = List.exists read_mem_e es - -let read_mem_lval = function - | Lnone _ | Lvar _ -> false - | Lmem (_,_,_,_) -> true - | Laset (_,_,_,_,e) | Lasub (_,_,_,_,e)-> read_mem_e e - - -let write_mem_lval = function - | Lnone _ | Lvar _ | Laset _ | Lasub _ -> false - | Lmem _ -> true - -let read_mem_lvals = List.exists read_mem_lval -let write_mem_lvals = List.exists write_mem_lval - -let rec read_mem_i s i = - match i.i_desc with - | Cassgn (x, _, _, e) -> read_mem_lval x || read_mem_e e - | Copn (xs, _, _, es) | Csyscall (xs, Syscall_t.RandomBytes _, es) -> read_mem_lvals xs || read_mem_es es - | Cif (e, c1, c2) -> read_mem_e e || read_mem_c s c1 || read_mem_c s c2 - | Cwhile (_, c1, e, c2) -> read_mem_c s c1 || read_mem_e e || read_mem_c s c2 - | Ccall (xs, fn, es) -> read_mem_lvals xs || Sf.mem fn s || read_mem_es es - | Cfor (_, (_, e1, e2), c) -> read_mem_e e1 || read_mem_e e2 || read_mem_c s c - -and read_mem_c s = List.exists (read_mem_i s) - -let read_mem_f s f = read_mem_c s f.f_body - -let rec write_mem_i s i = - match i.i_desc with - | Cassgn (x, _, _, _) -> write_mem_lval x - | Copn (xs, _, _, _) | Csyscall(xs, Syscall_t.RandomBytes _, _) -> write_mem_lvals xs - | Cif (_, c1, c2) -> write_mem_c s c1 ||write_mem_c s c2 - | Cwhile (_, c1, _, c2) -> write_mem_c s c1 ||write_mem_c s c2 - | Ccall (xs, fn, _) -> write_mem_lvals xs || Sf.mem fn s - | Cfor (_, _, c) -> write_mem_c s c - -and write_mem_c s = List.exists (write_mem_i s) - -let write_mem_f s f = write_mem_c s f.f_body - -let init_use fs = - let add t s f = if t s f then Sf.add f.f_name s else s in - List.fold_left - (fun (sr,sw) f -> add read_mem_f sr f, add write_mem_f sw f) - (Sf.empty, Sf.empty) fs - (* ------------------------------------------------------------------- *) let add_ptr pd x e = (Prog.tu pd, Papp2 (E.Oadd ( E.Op_w pd), Pvar x, e)) @@ -348,9 +288,10 @@ let normalize_name n = let mkfunname env fn = fn.fn_name |> normalize_name |> create_name env -let empty_env model fds arrsz warrsz randombytes = +let empty_env pd model fds arrsz warrsz randombytes = let env = { + pd; model; alls = keywords; vars = Mv.empty; @@ -373,14 +314,13 @@ let empty_env model fds arrsz warrsz randombytes = let get_funtype env f = snd (Mf.find f env.funs) let get_funname env f = fst (Mf.find f env.funs) -let pp_fname env fmt f = Format.fprintf fmt "%s" (get_funname env f) -let pp_syscall env fmt o = +let ec_syscall env o = match o with | Syscall_t.RandomBytes p -> let n = (Conv.int_of_pos p) in env.randombytes := Sint.add n !(env.randombytes); - Format.fprintf fmt "%s.randombytes_%i" syscall_mod_arg n + Format.sprintf "%s.randombytes_%i" syscall_mod_arg n let ty_lval = function | Lnone (_, ty) -> ty @@ -393,24 +333,9 @@ let ty_lval = function let add_Array env n = env.arrsz := Sint.add n !(env.arrsz) -let pp_Array env fmt n = - add_Array env n; - Format.fprintf fmt "Array%i" n - let add_WArray env n = env.warrsz := Sint.add n !(env.warrsz) -let pp_WArray env fmt n = - add_WArray env n; - Format.fprintf fmt "WArray%i" n - -let pp_ty env fmt ty = - match ty with - | Bty Bool -> Format.fprintf fmt "bool" - | Bty Int -> Format.fprintf fmt "int" - | Bty (U ws) -> pp_sz_t fmt ws - | Arr(ws,n) -> Format.fprintf fmt "%a %a.t" pp_sz_t ws (pp_Array env) n - let add_aux env tys = let tbl = Hashtbl.create 10 in let do1 env ty = @@ -448,27 +373,6 @@ let add_glob env x = let s = create_name env (normalize_name x.v_name) in set_var env x s -let pp_var env fmt (x:var) = pp_string fmt (Mv.find x env.vars) - -let pp_zeroext fmt (szi, szo) = - let io, ii = int_of_ws szo, int_of_ws szi in - if ii < io then Format.fprintf fmt "zeroextu%a" pp_size szo - else if ii = io then () - else (* io < ii *) Format.fprintf fmt "truncateu%a" pp_size szo - -let pp_op1 fmt = function - | E.Oword_of_int sz -> - Format.fprintf fmt "%a.of_int" pp_Tsz sz - | E.Oint_of_word sz -> - Format.fprintf fmt "%a.to_uint" pp_Tsz sz - | E.Osignext(szo,_szi) -> - Format.fprintf fmt "sigextu%a" pp_size szo - | E.Ozeroext(szo,szi) -> - pp_zeroext fmt (szi, szo) - | E.Onot -> Format.fprintf fmt "!" - | E.Olnot _ -> Format.fprintf fmt "invw" - | E.Oneg _ -> Format.fprintf fmt "-" - let swap_op2 op e1 e2 = match op with | E.Ogt _ -> e2, e1 @@ -550,264 +454,226 @@ let check_array env x = | Arr(ws, n) -> Sint.mem n !(env.arrsz) && Sint.mem (arr_size ws n) !(env.warrsz) | _ -> true -let pp_initi env pp fmt (x, n, ws) = - let i = create_name env "i" in - Format.fprintf fmt - "@[(%a.init%i (fun %s => %a.[%s]))@]" - (pp_WArray env) (arr_size ws n) (int_of_ws ws) i pp x i - -let pp_print_i fmt z = - if Z.leq Z.zero z then Z.pp_print fmt z - else Format.fprintf fmt "(%a)" Z.pp_print z +let ec_print_i z = + if Z.leq Z.zero z then Z.to_string z + else Format.asprintf "(%a)" Z.pp_print z let pp_access aa = if aa = Warray_.AAdirect then "_direct" else "" -let pp_cast env pp fmt (ty,ety,e) = - if ety = ty then pp fmt e - else - match ty with - | Bty _ -> - Format.fprintf fmt "(%a %a)" pp_zeroext (ws_of_ty ety, ws_of_ty ty) pp e - | Arr(ws, n) -> - let wse, ne = array_kind ety in - let i = create_name env "i" in - Format.fprintf fmt - "@[(%a.init@ (fun %s => (get%i@ %a@ %s)))@]" - (pp_Array env) n - i - (int_of_ws ws) - (pp_initi env pp) (e, ne, wse) - i - - -let rec pp_expr pd env fmt (e:expr) = - match e with - | Pconst z -> Format.fprintf fmt "%a" pp_print_i z +type ec_op2 = + | ArrayGet + | Plus + | Infix of string - | Pbool b -> Format.fprintf fmt "%a" pp_bool b +type ec_op3 = + | Ternary + | If + | InORange - | Parr_init _n -> Format.fprintf fmt "witness" +type ec_ident = string list - | Pvar x -> pp_var env fmt (L.unloc x.gv) +type ec_expr = + | Econst of Z.t (* int. literal *) + | Ebool of bool (* bool literal *) + | Eident of ec_ident (* variable *) + | Eapp of ec_expr * ec_expr list (* op. application *) + | Efun1 of string * ec_expr (* fun s => expr *) + | Eop2 of ec_op2 * ec_expr * ec_expr (* binary operator *) + | Eop3 of ec_op3 * ec_expr * ec_expr * ec_expr (* ternary operator *) + | Elist of ec_expr list (* list litteral *) + | Etuple of ec_expr list (* tuple litteral *) - | Pget(_, aa, ws, x, e) -> - assert (check_array env x.gv); - let x = x.gv in - let x = L.unloc x in - let (xws,n) = array_kind x.v_ty in - if ws = xws && aa = Warray_.AAscale then - Format.fprintf fmt "@[%a.[%a]@]" (pp_var env) x (pp_expr pd env) e - else - Format.fprintf fmt "@[(get%i%s@ %a@ %a)@]" - (int_of_ws ws) - (pp_access aa) - (pp_initi env (pp_var env)) (x, n, xws) (pp_expr pd env) e +let ec_ident s = Eident [s] +let ec_aget a i = Eop2 (ArrayGet, a, i) +let ec_int x = Econst (Z.of_int x) + +let ec_vars env (x:var) = Mv.find x env.vars +let ec_vari env (x:var) = Eident [ec_vars env x] - | Psub (aa, ws, len, x, e) -> - assert (check_array env x.gv); +let glob_mem = ["Glob"; "mem"] +let glob_memi = Eident glob_mem + +let pd_uint env = Eident [Format.sprintf "W%d" (int_of_ws env.pd); "to_uint"] + +let ec_apps1 s e = Eapp (ec_ident s, [e]) + +let iIdent i = ec_ident (Format.sprintf "%i" i) + +let fmt_Array n = Format.sprintf "Array%i" n + +let fmt_WArray n = Format.sprintf "WArray%i" n + +let ec_Array env n = add_Array env n; fmt_Array n + +let ec_WArray env n = add_WArray env n; fmt_WArray n + +let ec_WArray_init env ws n = + Eident [ec_WArray env (arr_size ws n); Format.sprintf "init%i" (int_of_ws ws)] + +let ec_WArray_initf env ws n f = let i = create_name env "i" in - let x = x.gv in - let x = L.unloc x in - let (xws,n) = array_kind x.v_ty in - if ws = xws && aa = Warray_.AAscale then - Format.fprintf fmt "@[(%a.init (fun %s => %a.[(%a + %s)]))@]" - (pp_Array env) len - i - (pp_var env) x - (pp_expr pd env) e - i - else - Format.fprintf fmt - "@[(%a.init (fun %s => (get%i%s@ %a@ (%a + %s))))@]" - (pp_Array env) len - i - (int_of_ws ws) - (pp_access aa) - (pp_initi env (pp_var env)) (x, n, xws) - (pp_expr pd env) e - i + Eapp (ec_WArray_init env ws n, [Efun1 (i, f i)]) - - | Pload (_, sz, x, e) -> - Format.fprintf fmt "(loadW%a Glob.mem (W%d.to_uint %a))" - pp_size sz - (int_of_ws pd) - (pp_wcast pd env) (add_ptr pd (gkvar x) e) - - | Papp1 (op1, e) -> - Format.fprintf fmt "(%a %a)" pp_op1 op1 (pp_wcast pd env) (in_ty_op1 op1, e) - - | Papp2 (op2, e1, e2) -> - let ty1,ty2 = in_ty_op2 op2 in - let te1, te2 = swap_op2 op2 (ty1, e1) (ty2, e2) in - Format.fprintf fmt "(%a %a %a)" - (pp_wcast pd env) te1 pp_op2 op2 (pp_wcast pd env) te2 - - | PappN (op, es) -> - (* FIXME *) - begin match op with - | Opack (ws, we) -> - let i = int_of_pe we in - let rec aux fmt es = - match es with - | [] -> assert false - | [e] -> Format.fprintf fmt "%a" (pp_expr pd env) e - | e::es -> - Format.fprintf fmt "@[((%a %%%% (2 ^ %i)) +@ ((2 ^ %i) * %a))@]" - (pp_expr pd env) e i i aux es in - Format.fprintf fmt "(W%a.of_int %a)" pp_size ws aux (List.rev es) - | Ocombine_flags c -> - Format.fprintf fmt "@[(%s@ %a)@]" - (Printer.string_of_combine_flags c) - (pp_list "@ " (pp_expr pd env)) es - end - - | Pif(_,e1,et,ef) -> - let ty = ty_expr e in - Format.fprintf fmt "(%a ? %a : %a)" - (pp_expr pd env) e1 (pp_wcast pd env) (ty,et) (pp_wcast pd env) (ty,ef) - -and pp_wcast pd env fmt (ty, e) = - pp_cast env (pp_expr pd env) fmt (ty, ty_expr e, e) - -let pp_vdecl env fmt x = - Format.fprintf fmt "%a:%a" - (pp_var env) x - (pp_ty env) x.v_ty - -let pp_params env fmt params = - Format.fprintf fmt "@[%a@]" - (pp_list ",@ " (pp_vdecl env)) params - -let pp_locals env fmt locals = - let locarr = - List.filter (fun x -> match x.v_ty with Arr _ -> true | _ -> false) - locals in - let locarr = - List.sort (fun x1 x2 -> compare x1.v_name x2.v_name) locarr in - - let pp_vdecl = pp_vdecl env in - let pp_loc fmt x = Format.fprintf fmt "var %a;" pp_vdecl x in - - let pp_init fmt x = - Format.fprintf fmt "%a <- witness;" (pp_var env) x in - Format.fprintf fmt "%a@ %a" - (pp_list "@ " pp_loc) locals - (pp_list "@ " pp_init) locarr - -let pp_rty env fmt tys = - if tys = [] then - Format.fprintf fmt "unit" - else - Format.fprintf fmt "@[%a@]" - (pp_list " *@ " (pp_ty env)) tys - -let pp_ret env fmt xs = - match xs with - | [x] -> Format.fprintf fmt "@[return %a;@]" (pp_var env) (L.unloc x) - | _ -> Format.fprintf fmt "@[return (%a);@]" - (pp_list ",@ " (fun fmt x -> pp_var env fmt (L.unloc x))) xs - -let pp_lval1 pd env pp_e fmt (lv, (ety, e)) = - let lty = ty_lval lv in - let pp_e fmt e = pp_e fmt (lty, ety, e) in - match lv with - | Lnone _ -> assert false - | Lmem(_, ws, x, e1) -> - Format.fprintf fmt "@[Glob.mem <-@ (storeW%a Glob.mem (W%d.to_uint %a) %a);@]" pp_size ws - (int_of_ws pd) - (pp_wcast pd env) (add_ptr pd (gkvar x) e1) pp_e e - | Lvar x -> - Format.fprintf fmt "@[%a <-@ %a;@]" (pp_var env) (L.unloc x) pp_e e - | Laset (_, aa, ws, x, e1) -> - assert (check_array env x); - let x = L.unloc x in - let (xws,n) = array_kind x.v_ty in - if ws = xws && aa = Warray_.AAscale then - Format.fprintf fmt "@[%a.[%a] <-@ %a;@]" - (pp_var env) x (pp_expr pd env) e1 pp_e e - else - let nws = n * int_of_ws xws in - let nws8 = nws / 8 in - Format.fprintf fmt - "@[%a <-@ @[(%a.init@ (%a.get%i (%a.set%i%s %a %a %a)));@]@]" - (pp_var env) x - (pp_Array env) n - (pp_WArray env) nws8 - (int_of_ws xws) - (pp_WArray env) nws8 (int_of_ws ws) - (pp_access aa) - (pp_initi env (pp_var env)) (x, n, xws) (pp_expr pd env) e1 pp_e e - | Lasub (aa, ws, len, x, e1) -> - assert (check_array env x); - let x = L.unloc x in - let (xws, n) = array_kind x.v_ty in - if ws = xws && aa = Warray_.AAscale then - let i = create_name env "i" in - Format.fprintf fmt - "@[%a <- @[(%a.init@ @[(fun %s => (if (%a <= %s < (%a + %i))@ then %a.[(%s - %a)]@ else %a.[%s]))@])@];@]" - (pp_var env) x - (pp_Array env) n - i - (pp_expr pd env) e1 - i - (pp_expr pd env) e1 len - pp_e e - i - (pp_expr pd env) e1 - (pp_var env) x - i - else - let nws = n * int_of_ws xws in - let nws8 = nws / 8 in - let pp_start fmt () = - if aa = Warray_.AAscale then - Format.fprintf fmt "(%i * %a)" (int_of_ws ws / 8) (pp_expr pd env) e1 - else - Format.fprintf fmt "%a" (pp_expr pd env) e1 in - let len8 = len * int_of_ws ws / 8 in - let pp_a fmt () = - let i = create_name env "i" in - Format.fprintf fmt - "@[(%a.init8@ (fun %s =>@ (if (%a <= %s < (%a + %i))@ then (%a.get8 %a (%s - %a))@ else (%a.get8 %a %s))))@]" - (pp_WArray env) nws8 - i - pp_start () i pp_start () len8 - (pp_WArray env) len8 (pp_initi env pp_e) (e, len, ws) i pp_start () - (pp_WArray env) nws8 (pp_initi env (pp_var env)) (x,n,xws) i - - in - - Format.fprintf fmt "@[%a <- @[(%a.init@ @[(%a.get%i %a)@])@];@]" - (pp_var env) x - (pp_Array env) n - (pp_WArray env) nws8 (int_of_ws xws) - pp_a () - -let pp_lval env fmt = function - | Lnone _ -> assert false - | Lmem _ -> assert false - | Lvar x -> pp_var env fmt (L.unloc x) - | Laset _ -> assert false - | Lasub _ -> assert false +let ec_Array_init env len = Eident [ec_Array env len; "init"] -let pp_lvals env fmt xs = - match xs with - | [] -> assert false - | [x] -> pp_lval env fmt x - | _ -> Format.fprintf fmt "(%a)" (pp_list ",@ " (pp_lval env)) xs +let ec_initi env (x, n, ws) = + let f i = ec_aget x (ec_ident i) in + ec_WArray_initf env ws n f -let pp_aux_lvs fmt aux = - match aux with - | [] -> assert false - | [x] -> Format.fprintf fmt "%s" x - | xs -> Format.fprintf fmt "(%a)" (pp_list ",@ " pp_string) xs +let ec_initi_var env (x, n, ws) = ec_initi env (ec_vari env x, n, ws) -let pp_wzeroext pp_e fmt tyo tyi e = - if tyi = tyo then pp_e fmt e - else - let szi, szo = ws_of_ty tyi, ws_of_ty tyo in - Format.fprintf fmt "(%a %a)" pp_zeroext (szi, szo) pp_e e +let ec_zeroext (szo, szi) e = + let io, ii = int_of_ws szo, int_of_ws szi in + if ii < io then ec_apps1 (Format.sprintf "zeroextu%i" io) e + else if ii = io then e + else (* io < ii *) ec_apps1 (Format.sprintf "truncateu%i" io) e + +let ec_wzeroext (tyo, tyi) e = + if tyi = tyo then e else ec_zeroext (ws_of_ty tyo, ws_of_ty tyi) e + +let ec_cast env (ty, ety) e = + if ety = ty then e + else + match ty with + | Bty _ -> ec_zeroext (ws_of_ty ty, ws_of_ty ety) e + | Arr(ws, n) -> + let wse, ne = array_kind ety in + let i = create_name env "i" in + let geti = ec_ident (Format.sprintf "get%i" (int_of_ws ws)) in + let init_fun = Efun1 (i, Eapp (geti, [ec_initi env (e, ne, wse); ec_ident i])) in + Eapp (ec_Array_init env n, [init_fun]) + +let ec_op1 op e = match op with + | E.Oword_of_int sz -> + ec_apps1 (Format.sprintf "%s.of_int" (pp_Tsz sz)) e + | E.Oint_of_word sz -> + ec_apps1 (Format.sprintf "%s.to_uint" (pp_Tsz sz)) e + | E.Osignext(szo,_szi) -> + ec_apps1 (Format.sprintf "sigextu%i" (int_of_ws szo)) e + | E.Ozeroext(szo,szi) -> ec_zeroext (szo, szi) e + | E.Onot -> ec_apps1 "!" e + | E.Olnot _ -> ec_apps1 "invw" e + | E.Oneg _ -> ec_apps1 "-" e + + +let rec toec_expr env (e: expr) = + match e with + | Pconst z -> Econst z + | Pbool b -> Ebool b + | Parr_init _n -> ec_ident "witness" + | Pvar x -> ec_vari env (L.unloc x.gv) + | Pget (a, aa, ws, y, e) -> + assert (check_array env y.gv); + let x = L.unloc y.gv in + let (xws, n) = array_kind x.v_ty in + if ws = xws && aa = Warray_.AAscale then + ec_aget (ec_vari env x) (toec_expr env e) + else + Eapp ( + (ec_ident (Format.sprintf "get%i%s" (int_of_ws ws) (pp_access aa))), + [ec_initi_var env (x, n, xws); toec_expr env e] + ) + | Psub (aa, ws, len, x, e) -> + assert (check_array env x.gv); + let i = create_name env "i" in + let x = L.unloc x.gv in + let (xws,n) = array_kind x.v_ty in + if ws = xws && aa = Warray_.AAscale then + Eapp ( + ec_Array_init env len, + [ + Efun1 (i, ec_aget (ec_vari env x) (Eop2 (Plus, toec_expr env e, ec_ident i))) + ]) + else + Eapp ( + ec_Array_init env len, + [ + Efun1 (i, + Eapp (ec_ident (Format.sprintf "get%i%s" (int_of_ws ws) (pp_access aa)), [ + ec_initi_var env (x, n, xws); Eop2 (Plus, toec_expr env e, ec_ident i) + ]) + ) + ]) + | Pload (_, sz, x, e) -> + let load = ec_ident (Format.sprintf "loadW%i" (int_of_ws sz)) in + Eapp (load, [ + glob_memi; + Eapp (pd_uint env, [ec_wcast env (add_ptr env.pd (gkvar x) e)]) + ]) + | Papp1 (op1, e) -> + ec_op1 op1 (ec_wcast env (in_ty_op1 op1, e)) + | Papp2 (op2, e1, e2) -> + let ty1,ty2 = in_ty_op2 op2 in + let te1, te2 = swap_op2 op2 (ty1, e1) (ty2, e2) in + let op = Infix (Format.asprintf "%a" pp_op2 op2) in + Eop2 (op, (ec_wcast env te1), (ec_wcast env te2)) + | PappN (op, es) -> + begin match op with + | Opack (ws, we) -> + let i = int_of_pe we in + let rec aux es = + match es with + | [] -> assert false + | [e] -> toec_expr env e + | e::es -> + let exp2i = Eop2 (Infix "^", iIdent 2, iIdent i) in + Eop2 ( + Infix "+", + Eop2 (Infix "%%", toec_expr env e, exp2i), + Eop2 (Infix "*", exp2i, aux es) + ) + in + ec_apps1 (Format.sprintf "W%i.of_int" (int_of_ws ws)) (aux (List.rev es)) + | Ocombine_flags c -> + Eapp ( + ec_ident (Printer.string_of_combine_flags c), + List.map (toec_expr env) es + ) + end + | Pif(_,e1,et,ef) -> + let ty = ty_expr e in + Eop3 ( + Ternary, + toec_expr env e1, + ec_wcast env (ty, et), + ec_wcast env (ty, ef) + ) + +and toec_cast env ty e = ec_cast env (ty, ty_expr e) (toec_expr env e) +and ec_wcast env (ty, e) = toec_cast env ty e + +let pp_ec_ident fmt ident = Format.fprintf fmt "@[%a@]" (pp_list "." pp_string) ident + +let rec pp_ec_ast_expr fmt e = match e with + | Econst z -> Format.fprintf fmt "%s" (ec_print_i z) + | Ebool b -> pp_bool fmt b + | Eident s -> pp_ec_ident fmt s + | Eapp (f, ops) -> + Format.fprintf fmt "@[(@,%a@,)@]" + (Format.(pp_print_list ~pp_sep:(fun fmt () -> fprintf fmt "@ ")) pp_ec_ast_expr) + (f::ops) + | Efun1 (var, e) -> + Format.fprintf fmt "@[(fun %s => %a)@]" var pp_ec_ast_expr e + | Eop2 (op, e1, e2) -> pp_ec_op2 fmt (op, e1, e2) + | Eop3 (op, e1, e2, e3) -> pp_ec_op3 fmt (op, e1, e2, e3) + | Elist es -> Format.fprintf fmt "@[[%a]@]" (pp_list ";@ " pp_ec_ast_expr) es + | Etuple es -> Format.fprintf fmt "@[(%a)@]" (pp_list ",@ " pp_ec_ast_expr) es + +and pp_ec_op2 fmt (op2, e1, e2) = + let f fmt = match op2 with + | ArrayGet -> Format.fprintf fmt "@[%a.[%a]@]" + | Plus -> Format.fprintf fmt "@[(%a +@ %a)@]" + | Infix s -> (fun pp1 e1 -> Format.fprintf fmt "@[(%a %s@ %a)@]" pp1 e1 s) + in + (f fmt) pp_ec_ast_expr e1 pp_ec_ast_expr e2 + +and pp_ec_op3 fmt (op, e1, e2, e3) = + let f fmt = match op with + | Ternary -> Format.fprintf fmt "@[(%a ? %a : %a)@]" + | If -> Format.fprintf fmt "@[(if %a then %a else %a)@]" + | InORange -> Format.fprintf fmt "@[(%a <= %a < %a)@]" + in + (f fmt) pp_ec_ast_expr e1 pp_ec_ast_expr e2 pp_ec_ast_expr e3 let base_op = function | Sopn.Oasm (Arch_extra.BaseOp (_, o)) -> Sopn.Oasm (Arch_extra.BaseOp(None,o)) @@ -868,394 +734,440 @@ let rec remove_for_i i = { i with i_desc } and remove_for c = List.map remove_for_i c -let pp_opn pd asmOp fmt o = +type ec_lvalue = + | LvIdent of ec_ident + | LvArrItem of ec_ident * ec_expr + +type ec_lvalues = ec_lvalue list + +type ec_instr = + | ESasgn of ec_lvalues * ec_expr + | EScall of ec_lvalues * ec_ident * ec_expr list + | ESsample of ec_lvalues * ec_expr + | ESif of ec_expr * ec_stmt * ec_stmt + | ESwhile of ec_expr * ec_stmt + | ESreturn of ec_expr + | EScomment of string (* comment line *) + +and ec_stmt = ec_instr list + +let pp_ec_lvalue fmt (lval: ec_lvalue) = + match lval with + | LvIdent ident -> pp_ec_ident fmt ident + | LvArrItem (ident, e) -> pp_ec_op2 fmt (ArrayGet, Eident ident, e) + +let pp_ec_lvalues fmt (lvalues: ec_lvalues) = + match lvalues with + | [] -> assert false + | [lv] -> pp_ec_lvalue fmt lv + | _ -> Format.fprintf fmt "@[(%a)@]" (pp_list ",@ " pp_ec_lvalue) lvalues + +let rec pp_ec_ast_stmt fmt stmt = + Format.fprintf fmt "@[%a@]" (pp_list "@ " pp_ec_ast_instr) stmt + +and pp_ec_ast_instr fmt instr = + match instr with + | ESasgn (lv, e) -> Format.fprintf fmt "@[%a <-@ %a;@]" pp_ec_lvalues lv pp_ec_ast_expr e + | EScall (lvs, f, args) -> + let pp_res fmt lvs = + if lvs = [] then + Format.fprintf fmt "" + else + Format.fprintf fmt "%a <%@ " pp_ec_lvalues lvs + in + Format.fprintf fmt "@[%a%a (%a);@]" + pp_res lvs + pp_ec_ast_expr (Eident f) + (pp_list ",@ " pp_ec_ast_expr) args + | ESsample (lv, e) -> Format.fprintf fmt "@[%a <$@ %a;@]" pp_ec_lvalues lv pp_ec_ast_expr e + | ESif (e, c1, c2) -> + Format.fprintf fmt "@[if (%a) {@ %a@ } else {@ %a@ }@]" + pp_ec_ast_expr e pp_ec_ast_stmt c1 pp_ec_ast_stmt c2 + | ESwhile (e, c) -> + Format.fprintf fmt "@[while (%a) {@ %a@ }@]" + pp_ec_ast_expr e pp_ec_ast_stmt c + | ESreturn e -> Format.fprintf fmt "@[return %a;@]" pp_ec_ast_expr e + | EScomment s -> Format.fprintf fmt "@[(* %s *)@]" s + +let ec_opn pd asmOp o = let s = Format.asprintf "%a" (pp_opn pd asmOp) o in - let s = if Ss.mem s keywords then s^"_" else s in - Format.fprintf fmt "%s" s + if Ss.mem s keywords then s^"_" else s -module Normal = struct +let ec_lval env = function + | Lnone _ -> assert false + | Lmem _ -> assert false + | Lvar x -> LvIdent [ec_vars env (L.unloc x)] + | Laset _ -> assert false + | Lasub _ -> assert false - let all_vars lvs = +let ec_lvals env xs = List.map (ec_lval env) xs + +let toec_lval1 env lv e = + match lv with + | Lnone _ -> assert false + | Lmem(_, ws, x, e1) -> + let storewi = ec_ident (Format.sprintf "storeW%i" (int_of_ws ws)) in + let addr = Eapp (pd_uint env, [ec_wcast env (add_ptr env.pd (gkvar x) e1)]) in + ESasgn ([LvIdent glob_mem], Eapp (storewi, [glob_memi; addr; e])) + | Lvar x -> + let lvid = [ec_vars env (L.unloc x)] in + ESasgn ([LvIdent lvid], e) + | Laset (_, aa, ws, x, e1) -> + assert (check_array env x); + let x = L.unloc x in + let (xws,n) = array_kind x.v_ty in + if ws = xws && aa = Warray_.AAscale then + ESasgn ([LvArrItem ([ec_vars env x], toec_expr env e1)], e) + else + let nws = n * int_of_ws xws in + let warray = ec_WArray env (nws / 8) in + let waget = Eident [warray; Format.sprintf "get%i" (int_of_ws xws)] in + let wsi = int_of_ws ws in + let waset = Eident [warray; Format.sprintf "set%i%s" wsi (pp_access aa)] in + let updwa = Eapp (waset, [ec_initi_var env (x, n, xws); toec_expr env e1; e]) in + ESasgn ( + [LvIdent [ec_vars env x]], + Eapp (ec_Array_init env n, [Eapp (waget, [updwa])]) + ) + | Lasub (aa, ws, len, x, e1) -> + assert (check_array env x); + let x = L.unloc x in + let (xws, n) = array_kind x.v_ty in + if ws = xws && aa = Warray_.AAscale then + let i = create_name env "i" in + let range_ub = Eop2 (Plus, toec_expr env e1, ec_int len) in + ESasgn ( + [LvIdent [ec_vars env x]], + Eapp (ec_Array_init env n, [ + Efun1 (i, Eop3 ( + If, + Eop3 (InORange, toec_expr env e1, ec_ident i, range_ub), + ec_aget e (Eop2 (Infix "-", ec_ident i, toec_expr env e1)), + ec_aget (ec_vari env x) (ec_ident i) + )) + ]) + ) + else + let nws = n * int_of_ws xws in + let nws8 = nws / 8 in + let start = + if aa = Warray_.AAscale then + Eop2 (Infix "*", ec_int (int_of_ws ws / 8), toec_expr env e1) + else + toec_expr env e1 + in + let len8 = len * int_of_ws ws / 8 in + let i = create_name env "i" in + let in_range = Eop3 (InORange, start, ec_ident i, Eop2 (Plus, start, ec_int len8)) in + let ainit = Eident [ec_WArray env nws8; "init8"] in + let aw_get8 len = Eident [ec_WArray env len; "get8"] in + let at = Eapp (aw_get8 len8, [ec_initi env (e, len, ws); Eop2 (Infix "-", ec_ident i, start)]) in + let ae = Eapp (aw_get8 nws8, [ec_initi_var env (x, n, xws); ec_ident i]) in + let a = Eapp (ainit, [Efun1 (i, Eop3 (If, in_range, at, ae))]) in + let wag = Eident [ec_WArray env nws8; Format.sprintf "get%i" (int_of_ws xws)] in + ESasgn ( + [LvIdent [ec_vars env x]], + Eapp (ec_Array_init env n, [Eapp (wag, [a])]) + ) + +(* =================----------=============== *) +let all_vars lvs = let is_lvar = function Lvar _ -> true | _ -> false in List.for_all is_lvar lvs - let check_lvals lvs = - all_vars lvs - - let rec init_aux_i pd asmOp env i = - match i.i_desc with - | Cassgn _ -> env - | Cif(_, c1, c2) - | Cwhile(_, c1, _, c2) -> - init_aux pd asmOp (init_aux pd asmOp env c1) c2 +let check_lvals lvs = all_vars lvs + +let rec init_aux_i pd asmOp env i = +match i.i_desc with + | Cassgn (lv, _, _, e) -> ( + match env.model with + | Normal -> env + | ConstantTime -> add_aux (add_aux env [ty_lval lv]) [ty_expr e] + ) + | Copn (lvs, _, op, _) -> ( + match env.model with + | Normal -> + if List.length lvs = 1 then env + else + let tys = List.map Conv.ty_of_cty (Sopn.sopn_tout pd asmOp op) in + let ltys = List.map ty_lval lvs in + if all_vars lvs && ltys = tys then env + else add_aux env tys + | ConstantTime -> + let op = base_op op in + let tys = List.map Conv.ty_of_cty (Sopn.sopn_tout pd asmOp op) in + let env = add_aux env tys in + add_aux env (List.map ty_lval lvs) + ) + | Ccall(lvs, f, _) -> ( + match env.model with + | Normal -> + if lvs = [] then env + else + let tys = (*List.map Conv.ty_of_cty *)(fst (get_funtype env f)) in + let ltys = List.map ty_lval lvs in + if (check_lvals lvs && ltys = tys) then env + else add_aux env tys + | ConstantTime -> + if lvs = [] then env + else add_aux env (List.map ty_lval lvs) + ) + | Csyscall(lvs, o, _) -> ( + match env.model with + | Normal -> + if lvs = [] then env + else + let tys = List.map Conv.ty_of_cty (Syscall.syscall_sig_u o).scs_tout in + let ltys = List.map ty_lval lvs in + if (check_lvals lvs && ltys = tys) then env + else add_aux env tys + | ConstantTime -> + let s = Syscall.syscall_sig_u o in + let otys = List.map Conv.ty_of_cty s.scs_tout in + let env = add_aux env otys in + add_aux env (List.map ty_lval lvs) + ) + | Cif(_, c1, c2) | Cwhile(_, c1, _, c2) -> init_aux pd asmOp (init_aux pd asmOp env c1) c2 | Cfor(_,_,c) -> init_aux pd asmOp (add_aux env [tint]) c - | Copn (lvs, _, op, _) -> - if List.length lvs = 1 then env - else - let tys = List.map Conv.ty_of_cty (Sopn.sopn_tout pd asmOp op) in - let ltys = List.map ty_lval lvs in - if all_vars lvs && ltys = tys then env - else add_aux env tys - | Ccall(lvs, f, _) -> - if lvs = [] then env - else - let tys = (*List.map Conv.ty_of_cty *)(fst (get_funtype env f)) in - let ltys = List.map ty_lval lvs in - if (check_lvals lvs && ltys = tys) then env - else add_aux env tys - | Csyscall(lvs, o, _) -> - if lvs = [] then env - else - let tys = List.map Conv.ty_of_cty (Syscall.syscall_sig_u o).scs_tout in - let ltys = List.map ty_lval lvs in - if (check_lvals lvs && ltys = tys) then env - else add_aux env tys - - and init_aux pd asmOp env c = List.fold_left (init_aux_i pd asmOp) env c - - let pp_assgn_i pd env fmt lv ((etyo, etyi), aux) = - let pp_e fmt aux = - pp_wzeroext pp_string fmt etyo etyi aux in - Format.fprintf fmt "@ %a" (pp_lval1 pd env (pp_cast env pp_e)) (lv, (etyo,aux)) - - - let pp_call pd env fmt lvs etyso etysi pp a = - let ltys = List.map (fun lv -> ty_lval lv) lvs in - if check_lvals lvs && ltys = etyso && etyso = etysi then - Format.fprintf fmt "@[%a %a;@]" (pp_lvals env) lvs pp a - else - let auxs = get_aux env etysi in - Format.fprintf fmt "@[%a %a;@]" pp_aux_lvs auxs pp a; - let tyauxs = List.combine (List.combine etyso etysi) auxs in - List.iter2 (pp_assgn_i pd env fmt) lvs tyauxs - - let rec pp_cmd pd asmOp env fmt c = - Format.fprintf fmt "@[%a@]" (pp_list "@ " (pp_instr pd asmOp env)) c - - and pp_instr pd asmOp env fmt i = - match i.i_desc with - | Cassgn(v, _, _, Parr_init _) -> - let pp_e fmt _ = Format.fprintf fmt "witness" in - pp_lval1 pd env pp_e fmt (v, ((), ())) - - | Cassgn (lv, _, _ty, e) -> - let pp_e = pp_cast env (pp_expr pd env) in - pp_lval1 pd env pp_e fmt (lv , (ty_expr e, e)) - - | Copn([], _, op, _es) -> - (* Erase opn without any return values *) - Format.fprintf fmt "(* Erased call to %a *)" (pp_opn pd asmOp) op - - | Copn(lvs, _, op, es) -> - let op' = base_op op in - (* Since we do not have merge for the moment only the output type can change *) - let otys,itys = ty_sopn pd asmOp op es in - let otys', _ = ty_sopn pd asmOp op' es in - let pp_e fmt (op,es) = - if es = [] then - Format.fprintf fmt "(%a)" (pp_opn pd asmOp) op - else - Format.fprintf fmt "(%a %a)" (pp_opn pd asmOp) op - (pp_list "@ " (pp_wcast pd env)) (List.combine itys es) - in - if List.length lvs = 1 then - let pp_e fmt (op, es) = - pp_wzeroext pp_e fmt (List.hd otys) (List.hd otys') (op, es) in - let pp_e = pp_cast env pp_e in - pp_lval1 pd env pp_e fmt (List.hd lvs , (List.hd otys, (op',es))) - else - let pp fmt (op, es) = - Format.fprintf fmt "<- %a" pp_e (op,es) in - pp_call pd env fmt lvs otys otys' pp (op,es) - - | Ccall(lvs, f, es) -> - let otys, itys = get_funtype env f in - let pp_args fmt es = - pp_list ",@ " (pp_wcast pd env) fmt (List.combine itys es) in - if lvs = [] then - Format.fprintf fmt "@[%a (%a);@]" (pp_fname env) f pp_args es - else - let pp fmt es = - Format.fprintf fmt "<%@ %a (%a)" (pp_fname env) f pp_args es in - pp_call pd env fmt lvs otys otys pp es - - | Csyscall(lvs, o, es) -> - let s = Syscall.syscall_sig_u o in - let otys = List.map Conv.ty_of_cty s.scs_tout in - let itys = List.map Conv.ty_of_cty s.scs_tin in - let pp_args fmt es = - pp_list ",@ " (pp_wcast pd env) fmt (List.combine itys es) in - if lvs = [] then - Format.fprintf fmt "@[%a (%a);@]" (pp_syscall env) o pp_args es - else - let pp fmt es = - Format.fprintf fmt "<%@ %a (%a)" (pp_syscall env) o pp_args es in - pp_call pd env fmt lvs otys otys pp es - - | Cif(e,c1,c2) -> - Format.fprintf fmt "@[if (%a) {@ %a@ } else {@ %a@ }@]" - (pp_expr pd env) e (pp_cmd pd asmOp env) c1 (pp_cmd pd asmOp env) c2 - - | Cwhile(_, c1, e,c2) -> - if c1 = [] then - Format.fprintf fmt "@[while (%a) {@ %a@ }@]" - (pp_expr pd env) e (pp_cmd pd asmOp env) c2 - else - Format.fprintf fmt "@[%a@ while (%a) {@ %a@ }@]" - (pp_cmd pd asmOp env) c1 (pp_expr pd env) e (pp_cmd pd asmOp env) (c2@c1) - - | Cfor(i, (d,e1,e2), c) -> - (* decreasing for loops have bounds swaped *) - let e1, e2 = if d = UpTo then e1, e2 else e2, e1 in - let pp_init, pp_e2 = - match e2 with - (* Can be generalized to the case where e2 is not modified by c and i *) - | Pconst _ -> (fun _fmt () -> ()), (fun fmt () -> pp_expr pd env fmt e2) - | _ -> - let aux = List.hd (get_aux env [tint]) in - let pp_init fmt () = - Format.fprintf fmt "@[%s <-@ %a@];@ " aux (pp_expr pd env) e2 in - let pp_e2 fmt () = pp_string fmt aux in - pp_init, pp_e2 in - let pp_i fmt () = pp_var env fmt (L.unloc i) in - let pp_i1, pp_i2 = - if d = UpTo then pp_i , pp_e2 - else pp_e2, pp_i in - Format.fprintf fmt - "@[%a%a <- %a;@ while ((%a < %a)) {@ @[%a@ %a <- (%a %s 1);@]@ }@]" - pp_init () - pp_i () (pp_expr pd env) e1 - pp_i1 () pp_i2 () - (pp_cmd pd asmOp env) c - pp_i () pp_i () (if d = UpTo then "+" else "-") -end +and init_aux pd asmOp env c = List.fold_left (init_aux_i pd asmOp) env c -module Leak = struct - let pp_leaks pd env fmt es = - Format.fprintf fmt "@[leakages <- ((LeakAddr @[[%a]@]) :: leakages);@]@ " - (pp_list ";@ " (pp_expr pd env)) es +let ece_leaks_e env e = List.map (toec_expr env) (leaks_e env.pd e) - let pp_leaks_e pd env fmt e = - match env.model with - | ConstantTime -> pp_leaks pd env fmt (leaks_e pd e) - | Normal -> () +let ec_newleaks leaks = + let add_leak lacc l = Eop2 (Infix "::", l, lacc) in + List.fold_left add_leak (ec_ident "leakages") leaks + +let ec_addleaks leaks = [ESasgn ([LvIdent ["leakages"]], ec_newleaks leaks)] + +let ec_leaks es = ec_addleaks [Eapp (ec_ident "LeakAddr", [Elist es])] - let pp_leaks_es pd env fmt es = +let ec_leaks_e env e = match env.model with - | ConstantTime -> pp_leaks pd env fmt (leaks_es pd es) - | Normal -> () - - let pp_leaks_opn pd asmOp env fmt op es = + | ConstantTime -> ec_leaks (ece_leaks_e env e) + | Normal -> [] + +let ec_leaks_es env es = match env.model with - | ConstantTime -> pp_leaks pd env fmt (leaks_es pd es) - | Normal -> () + | ConstantTime -> ec_leaks (List.map (toec_expr env) (leaks_es env.pd es)) + | Normal -> [] - let pp_leaks_if pd env fmt e = +let ec_leaks_opn env es = ec_leaks_es env es + +let ec_leaks_if env e = match env.model with | ConstantTime -> - let leaks = leaks_e pd e in - Format.fprintf fmt - "@[leakages <- ((LeakCond %a) :: ((LeakAddr @[[%a]@]) :: leakages));@]@ " - (pp_expr pd env) e (pp_list ";@ " (pp_expr pd env)) leaks - | Normal -> () + ec_addleaks [ + Eapp (ec_ident "LeakAddr", [Elist (ece_leaks_e env e)]); + Eapp (ec_ident "LeakCond", [toec_expr env e]) + ] + | Normal -> [] - let pp_leaks_for pd env fmt e1 e2 = +let ec_leaks_for env e1 e2 = match env.model with | ConstantTime -> - let leaks = leaks_es pd [e1;e2] in - Format.fprintf fmt - "@[leakages <- ((LeakFor (%a, %a)) :: ((LeakAddr @[[%a]@]) :: leakages));@]@ " - (pp_expr pd env) e1 (pp_expr pd env) e2 - (pp_list ";@ " (pp_expr pd env)) leaks - | Normal -> () - - let pp_leaks_lv pd env fmt lv = + let leaks = List.map (toec_expr env) (leaks_es env.pd [e1;e2]) in + ec_addleaks [ + Eapp (ec_ident "LeakAddr", [Elist leaks]); + Eapp (ec_ident "LeakFor", [Etuple [toec_expr env e1; toec_expr env e2]]) + ] + | Normal -> [] + +let ec_leaks_lv env lv = match env.model with | ConstantTime -> - let leaks = leaks_lval pd lv in - if leaks <> [] then pp_leaks pd env fmt leaks - | Normal -> () - - let rec init_aux_i pd asmOp env i = - match i.i_desc with - | Cassgn (lv, _, _, e) -> add_aux (add_aux env [ty_lval lv]) [ty_expr e] - | Copn (lvs, _, op, _) -> - let op = base_op op in - let tys = List.map Conv.ty_of_cty (Sopn.sopn_tout pd asmOp op) in - let env = add_aux env tys in - add_aux env (List.map ty_lval lvs) - | Csyscall(lvs, o, _)-> - let s = Syscall.syscall_sig_u o in - let otys = List.map Conv.ty_of_cty s.scs_tout in - let env = add_aux env otys in - add_aux env (List.map ty_lval lvs) - | Ccall(lvs, _, _) -> - if lvs = [] then env - else add_aux env (List.map ty_lval lvs) - | Cif(_, c1, c2) | Cwhile(_, c1, _, c2) -> init_aux pd asmOp (init_aux pd asmOp env c1) c2 - | Cfor(_,_,c) -> init_aux pd asmOp (add_aux env [tint]) c + let leaks = leaks_lval env.pd lv in + if leaks = [] then [] + else ec_leaks (List.map (toec_expr env) leaks) + | Normal -> [] - and init_aux pd asmOp env c = List.fold_left (init_aux_i pd asmOp) env c +let ec_assgn env lv (etyo, etyi) e = + let e = e |> ec_wzeroext (etyo, etyi) |> ec_cast env (ty_lval lv, etyo) in + (ec_leaks_lv env lv) @ [toec_lval1 env lv e] - let pp_assgn_i pd env fmt lv ((etyo, etyi), aux) = - Format.fprintf fmt "@ "; pp_leaks_lv pd env fmt lv; - let pp_e fmt aux = - pp_wzeroext pp_string fmt etyo etyi aux in - let pp_e = pp_cast env pp_e in - pp_lval1 pd env pp_e fmt (lv, (etyo,aux)) +let ec_assgn_i env lv ((etyo, etyi), aux) = ec_assgn env lv (etyo, etyi) (ec_ident aux) - let pp_call pd env fmt lvs etyso etysi pp a = +let ec_instr_aux env lvs etyso etysi instr = let auxs = get_aux env etysi in - Format.fprintf fmt "@[%a %a;@]" pp_aux_lvs auxs pp a; + let s2lv s = LvIdent [s] in + let call = instr (List.map s2lv auxs) in let tyauxs = List.combine (List.combine etyso etysi) auxs in - List.iter2 (pp_assgn_i pd env fmt) lvs tyauxs - - let rec pp_cmd pd asmOp env fmt c = - Format.fprintf fmt "@[%a@]" (pp_list "@ " (pp_instr pd asmOp env)) c - - and pp_instr pd asmOp env fmt i = - match i.i_desc with - | Cassgn(v, _, _, (Parr_init _ as e)) -> - pp_leaks_e pd env fmt e; - let pp_e fmt _ = Format.fprintf fmt "witness" in - pp_lval1 pd env pp_e fmt (v, ((), ())) - - | Cassgn (lv, _, _, e) -> - pp_leaks_e pd env fmt e; - let pp fmt e = Format.fprintf fmt "<- %a" (pp_expr pd env) e in - let tys = [ty_expr e] in - pp_call pd env fmt [lv] tys tys pp e - - | Copn([], _, op, es) -> - (* Erase opn without return values but keep their leakage *) - let op' = base_op op in - pp_leaks_opn pd asmOp env fmt op' es; - Format.fprintf fmt "(* Erased call to %a *)" (pp_opn pd asmOp) op - - | Copn(lvs, _, op, es) -> - let op' = base_op op in - (* Since we do not have merge for the moment only the output type can change *) - let otys,itys = ty_sopn pd asmOp op es in - let otys', _ = ty_sopn pd asmOp op' es in - let pp fmt (op, es) = - Format.fprintf fmt "<- (%a%a)" (pp_opn pd asmOp) op - (pp_list_pre "@ " (pp_wcast pd env)) (List.combine itys es) in - pp_leaks_opn pd asmOp env fmt op' es; - pp_call pd env fmt lvs otys otys' pp (op, es) - - | Ccall(lvs, f, es) -> - let otys, itys = get_funtype env f in - let pp_args fmt es = - pp_list ",@ " (pp_wcast pd env) fmt (List.combine itys es) in - pp_leaks_es pd env fmt es; - if lvs = [] then - Format.fprintf fmt "@[%a (%a);@]" (pp_fname env) f pp_args es - else - let pp fmt es = - Format.fprintf fmt "<%@ %a (%a)" (pp_fname env) f pp_args es in - pp_call pd env fmt lvs otys otys pp es - - | Csyscall(lvs, o, es) -> - let s = Syscall.syscall_sig_u o in - let otys = List.map Conv.ty_of_cty s.scs_tout in - let itys = List.map Conv.ty_of_cty s.scs_tin in - - let pp_args fmt es = - pp_list ",@ " (pp_wcast pd env) fmt (List.combine itys es) in - pp_leaks_es pd env fmt es; - if lvs = [] then - Format.fprintf fmt "@[%a (%a);@]" (pp_syscall env) o pp_args es - else - let pp fmt es = - Format.fprintf fmt "<%@ %a (%a)" (pp_syscall env) o pp_args es in - pp_call pd env fmt lvs otys otys pp es - - | Cif(e,c1,c2) -> - pp_leaks_if pd env fmt e; - Format.fprintf fmt "@[if (%a) {@ %a@ } else {@ %a@ }@]" - (pp_expr pd env) e (pp_cmd pd asmOp env) c1 (pp_cmd pd asmOp env) c2 - - | Cwhile(_, c1, e,c2) -> - let pp_leak fmt e = - Format.fprintf fmt "@ %a" (pp_leaks_if pd env) e in - Format.fprintf fmt "@[%a%a@ while (%a) {@ %a%a@ }@]" - (pp_cmd pd asmOp env) c1 pp_leak e (pp_expr pd env) e - (pp_cmd pd asmOp env) (c2@c1) pp_leak e - - | Cfor(i, (d,e1,e2), c) -> - (* decreasing for loops have bounds swaped *) - let e1, e2 = if d = UpTo then e1, e2 else e2, e1 in - pp_leaks_for pd env fmt e1 e2; - let aux, env1 = List.hd (get_aux env [tint]), env in - let pp_init, pp_e2 = - match e2 with - (* Can be generalized to the case where e2 is not modified by c and i *) - | Pconst _ -> (fun _fmt () -> ()), (fun fmt () -> pp_expr pd env fmt e2) - | _ -> - let pp_init fmt () = - Format.fprintf fmt "@[%s <-@ %a@];@ " aux (pp_expr pd env) e2 in - let pp_e2 fmt () = pp_string fmt aux in - pp_init, pp_e2 in - let pp_i fmt () = pp_var env1 fmt (L.unloc i) in - let pp_i1, pp_i2 = - if d = UpTo then pp_i , pp_e2 - else pp_e2, pp_i in - Format.fprintf fmt - "@[%a%a <- %a;@ while ((%a < %a)) {@ @[%a@ %a <- (%a %s 1);@]@ }@]" - pp_init () - pp_i () (pp_expr pd env) e1 - pp_i1 () pp_i2 () - (pp_cmd pd asmOp env1) c - pp_i () pp_i () (if d = UpTo then "+" else "-") - -end - -let pp_aux fmt env = - let pp ty aux = - Format.fprintf fmt "@[var %s:%a@];@ " aux (pp_ty env) ty in - Mty.iter (fun ty -> List.iter (pp ty)) env.auxv - -let pp_fun pd asmOp env fmt f = - let f = { f with f_body = remove_for f.f_body } in - let locals = Sv.elements (locals f) in - (* initialize the env *) - let env = List.fold_left add_var env f.f_args in - let env = List.fold_left add_var env locals in - (* init auxiliary variables *) - let env = - if env.model = Normal then Normal.init_aux pd asmOp env f.f_body - else Leak.init_aux pd asmOp env f.f_body in - - (* Print the function *) - (* FIXME ajouter les conditions d'initialisation - sur les variables de retour *) - let pp_cmd = - if env.model = Normal then Normal.pp_cmd - else Leak.pp_cmd in - Format.fprintf fmt - "@[@[proc %a (%a) : %a = {@]@ @[%a@ %a@ %a@ %a@]@ }@]" - (pp_fname env) f.f_name - (pp_params env) f.f_args - (pp_rty env) f.f_tyout - pp_aux env - (pp_locals env) locals - (pp_cmd pd asmOp env) f.f_body - (pp_ret env) f.f_ret - -let pp_glob_decl env fmt (x,d) = - match d with - | Global.Gword(ws, w) -> - Format.fprintf fmt "@[abbrev %a = (%a.of_int %a).@]@ " - (pp_var env) x pp_Tsz ws pp_print_i (Conv.z_of_word ws w) - | Global.Garr(p,t) -> - let wz, t = Conv.to_array x.v_ty p t in - let pp_elem fmt z = - Format.fprintf fmt "(%a.of_int %a)" pp_Tsz wz pp_print_i z in - Format.fprintf fmt "@[abbrev %a = (%a.of_list witness [%a]).@]@ " - (pp_var env) x (pp_Array env) (Array.length t) - (pp_list ";@ " pp_elem) (Array.to_list t) + let assgn_auxs = List.flatten (List.map2 (ec_assgn_i env) lvs tyauxs) in + call :: assgn_auxs + +let ec_pcall env lvs otys f args = + let ltys = List.map ty_lval lvs in + if lvs = [] || (env.model = Normal && check_lvals lvs && ltys = otys) then + [EScall (ec_lvals env lvs, f, args)] + else + ec_instr_aux env lvs otys otys (fun lvals -> EScall (lvals, f, args)) + +let ec_call env lvs etyso etysi e = + let ltys = List.map ty_lval lvs in + if lvs = [] || (env.model = Normal && check_lvals lvs && ltys = etyso && etyso = etysi) then + [ESasgn ((ec_lvals env lvs), e)] + else + ec_instr_aux env lvs etyso etysi (fun lvals -> ESasgn (lvals, e)) + +let rec toec_cmd asmOp env c = List.flatten (List.map (toec_instr asmOp env) c) + +and toec_instr asmOp env i = + match i.i_desc with + | Cassgn (lv, _, _, (Parr_init _ as e)) -> + (ec_leaks_e env e) @ + [toec_lval1 env lv (ec_ident "witness")] + | Cassgn (lv, _, _, e) -> ( + match env.model with + | Normal -> + let e = toec_cast env (ty_lval lv) e in + [toec_lval1 env lv e] + | ConstantTime -> + let tys = [ty_expr e] in + (ec_leaks_e env e) @ + ec_call env [lv] tys tys (toec_expr env e) + ) + | Copn ([], _, op, es) -> + (ec_leaks_opn env es) @ + [EScomment (Format.sprintf "Erased call to %s" (ec_opn env.pd asmOp op))] + | Copn (lvs, _, op, es) -> + let op' = base_op op in + (* Since we do not have merge for the moment only the output type can change *) + let otys,itys = ty_sopn env.pd asmOp op es in + let otys', _ = ty_sopn env.pd asmOp op' es in + let ec_op op = ec_ident (ec_opn env.pd asmOp op) in + let ec_e op = Eapp (ec_op op, List.map (ec_wcast env) (List.combine itys es)) in + if env.model = Normal && List.length lvs = 1 then + ec_assgn env (List.hd lvs) (List.hd otys, List.hd otys') (ec_e op') + else + (ec_leaks_opn env es) @ + (ec_call env lvs otys otys' (ec_e op)) + | Ccall (lvs, f, es) -> + let otys, itys = get_funtype env f in + let args = List.map (ec_wcast env) (List.combine itys es) in + (ec_leaks_es env es) @ + (ec_pcall env lvs otys [get_funname env f] args) + | Csyscall (lvs, o, es) -> + let s = Syscall.syscall_sig_u o in + let otys = List.map Conv.ty_of_cty s.scs_tout in + let itys = List.map Conv.ty_of_cty s.scs_tin in + let args = List.map (ec_wcast env) (List.combine itys es) in + (ec_leaks_es env es) @ + (ec_pcall env lvs otys [ec_syscall env o] args) + | Cif (e, c1, c2) -> + (ec_leaks_if env e) @ + [ESif (toec_expr env e, toec_cmd asmOp env c1, toec_cmd asmOp env c2)] + | Cwhile (_, c1, e, c2) -> + let leak_e = ec_leaks_if env e in + (toec_cmd asmOp env c1) @ leak_e @ + [ESwhile (toec_expr env e, (toec_cmd asmOp env (c2@c1)) @ leak_e)] + | Cfor (i, (d,e1,e2), c) -> + (* decreasing for loops have bounds swaped *) + let e1, e2 = if d = UpTo then e1, e2 else e2, e1 in + let init, ec_e2 = + match e2 with + (* Can be generalized to the case where e2 is not modified by c and i *) + | Pconst _ -> ([], toec_expr env e2) + | _ -> + let aux = List.hd (get_aux env [tint]) in + let init = ESasgn ([LvIdent [aux]], toec_expr env e2) in + let ec_e2 = ec_ident aux in + [init], ec_e2 in + let ec_i = [ec_vars env (L.unloc i)] in + let lv_i = [LvIdent ec_i] in + let ec_i1, ec_i2 = + if d = UpTo then Eident ec_i , ec_e2 + else ec_e2, Eident ec_i in + let i_upd_op = Infix (if d = UpTo then "+" else "-") in + let i_upd = ESasgn (lv_i, Eop2 (i_upd_op, Eident ec_i, Econst (Z.of_int 1))) in + (ec_leaks_for env e1 e2) @ init @ [ + ESasgn (lv_i, toec_expr env e1); + ESwhile (Eop2 (Infix "<", ec_i1, ec_i2), (toec_cmd asmOp env c) @ [i_upd]) + ] + +type ec_ty = string + +type ec_var = string * ec_ty + +type ec_fun_decl = { + fname: string; + args: (string * ec_ty) list; + rtys: ec_ty list; +} +type ec_fun = { + decl: ec_fun_decl; + locals: (string * ec_ty) list; + stmt: ec_stmt; +} + +let toec_ty ty = match ty with + | Bty Bool -> "bool" + | Bty Int -> "int" + | Bty (U ws) -> (pp_sz_t ws) + | Arr(ws,n) -> Format.sprintf "%s %s.t" (pp_sz_t ws) (fmt_Array n) + +let var2ec_var env x = (List.hd [ec_vars env x], toec_ty x.v_ty) + +let pp_ec_vdecl fmt (x, ty) = Format.fprintf fmt "%s:%a" x pp_string ty + +let pp_ec_fun_decl fmt fdecl = + let pp_ec_rty fmt rtys = + if rtys = [] then Format.fprintf fmt "unit" + else Format.fprintf fmt "@[%a@]" (pp_list " *@ " pp_string) rtys + in + Format.fprintf fmt + "@[proc %s (@[%a@]) : @[%a@]@]" + fdecl.fname + (pp_list ",@ " pp_ec_vdecl) fdecl.args + pp_ec_rty fdecl.rtys + +let pp_ec_fun fmt f = + let pp_decl_s fmt v = Format.fprintf fmt "var %a;" pp_ec_vdecl v in + Format.fprintf fmt + "@[@[%a = {@]@ @[%a@ %a@]@ }@]" + pp_ec_fun_decl f.decl + (pp_list "@ " pp_decl_s) f.locals + pp_ec_ast_stmt f.stmt + +let add_ty env = function + | Bty _ -> () + | Arr (_ws, n) -> add_Array env n + +let toec_fun asmOp env f = + let f = { f with f_body = remove_for f.f_body } in + let locals = Sv.elements (locals f) in + let env = List.fold_left add_var env (f.f_args @ locals) in + (* init auxiliary variables *) + let env = init_aux env.pd asmOp env f.f_body + in + List.iter (add_ty env) f.f_tyout; + List.iter (fun x -> add_ty env x.v_ty) (f.f_args @ locals); + Mty.iter (fun ty _ -> add_ty env ty) env.auxv; + let ec_locals = + let locs_ty (ty, vars) = List.map (fun v -> (v, toec_ty ty)) vars in + (List.flatten (List.map locs_ty (Mty.bindings env.auxv))) @ + (List.map (var2ec_var env) locals) + in + let aux_locals_init = locals + |> List.filter (fun x -> match x.v_ty with Arr _ -> true | _ -> false) + |> List.sort (fun x1 x2 -> compare x1.v_name x2.v_name) + |> List.map (fun x -> ESasgn ([LvIdent [ec_vars env x]], ec_ident "witness")) + in + let ret = + let ec_var x = ec_vari env (L.unloc x) in + match f.f_ret with + | [x] -> ESreturn (ec_var x) + | xs -> ESreturn (Etuple (List.map ec_var xs)) + in + { + decl = { + fname = (get_funname env f.f_name); + args = List.map (var2ec_var env) f.f_args; + rtys = List.map toec_ty f.f_tyout; + }; + locals = ec_locals; + stmt = aux_locals_init @ (toec_cmd asmOp env f.f_body) @ [ret]; + } let add_arrsz env f = let add_sz x sz = @@ -1300,82 +1212,169 @@ let add_glob_arrsz env (x,d) = env.warrsz := Sint.add (arr_size ws n) !(env.warrsz); env -let jmodel () = - let open Glob_options in - match !target_arch with +let jmodel () = match !Glob_options.target_arch with | X86_64 -> "JModel_x86" | ARM_M4 -> "JModel_m4" -let require_lib_slh () = - let s = - match !Glob_options.target_arch with +let lib_slh () = match !Glob_options.target_arch with | X86_64 -> "SLH64" | ARM_M4 -> "SLH32" - in - Format.sprintf "import %s." s -let pp_prog pd asmOp fmt model globs funcs arrsz warrsz randombytes = +type ec_modty = string + +type ec_module_type = { + name: ec_modty; + funs: ec_fun_decl list; +} + +type ec_module = { + name: string; + params: (string * ec_modty) list; + ty: ec_modty option; + vars: (string * string) list; + funs: ec_fun list; +} + +type ec_item = + | IrequireImport of string list + | Iimport of string list + | IfromImport of string * (string list) + | IfromRequireImport of string * (string list) + | Iabbrev of string * ec_expr + | ImoduleType of ec_module_type + | Imodule of ec_module + +type ec_prog = ec_item list + +let pp_ec_item fmt it = match it with + | IrequireImport is -> + Format.fprintf fmt "@[require import@ @[%a@].@]" (pp_list "@ " pp_string) is + | Iimport is -> + Format.fprintf fmt "@[import@ @[%a@].@]" (pp_list "@ " pp_string) is + | IfromImport (m, is) -> + Format.fprintf fmt "@[from %s import@ @[%a@].@]" m (pp_list "@ " pp_string) is + | IfromRequireImport (m, is) -> + Format.fprintf fmt "@[from %s require import@ @[%a@].@]" m (pp_list "@ " pp_string) is + | Iabbrev (a, e) -> + Format.fprintf fmt "@[abbrev %s =@ @[%a@].@]" a pp_ec_ast_expr e + | ImoduleType mt -> + Format.fprintf fmt "@[@[module type %s = {@]@ @[%a@]@ }.@]" + mt.name (pp_list "@ " pp_ec_fun_decl) mt.funs + | Imodule m -> + let pp_mp fmt (m, mt) = Format.fprintf fmt "%s:%s" m mt in + Format.fprintf fmt "@[@[module %s@[%a@]%a = {@]@ @[%a%a%a@]@ }.@]" + m.name + (pp_list_paren ",@ " pp_mp) m.params + (pp_option (fun fmt s -> Format.fprintf fmt " : %s" s)) m.ty + (pp_list "@ " (fun fmt (v, t) -> Format.fprintf fmt "@[var %s : %s@]" v t)) m.vars + (fun fmt _ -> if m.vars = [] then (Format.fprintf fmt "") else (Format.fprintf fmt "@ ")) () + (pp_list "@ " pp_ec_fun) m.funs + +let pp_ec_prog fmt prog = Format.fprintf fmt "@[%a@]" (pp_list "@ @ " pp_ec_item) prog + +let ec_glob_decl env (x,d) = + let w_of_z ws z = Eapp (Eident [pp_Tsz ws; "of_int"], [ec_ident (ec_print_i z)]) in + let mk_abbrev e = Iabbrev (ec_vars env x, e) in + match d with + | Global.Gword(ws, w) -> mk_abbrev (w_of_z ws (Conv.z_of_word ws w)) + | Global.Garr(p,t) -> + let ws, t = Conv.to_array x.v_ty p t in + mk_abbrev (Eapp ( + Eident [ec_Array env (Array.length t); "of_list"], + [ec_ident "witness"; Elist (List.map (w_of_z ws) (Array.to_list t))] + )) + +let ec_randombytes env = + let randombytes_decl a n = + let arr_ty = Format.sprintf "W8.t %s.t" (fmt_Array n) in + { + fname = Format.sprintf "randombytes_%i" n; + args = [(a, arr_ty)]; + rtys = [arr_ty]; + } + in + let randombytes_f n = + let dmap = + let wa = fmt_WArray n in + let initf = Efun1 ("a", Eapp (Eident [fmt_Array n; "init"], [ + Efun1 ("i", Eapp (Eident [wa; "get8"], [ec_ident "a"; ec_ident "i"])) + ])) in + Eapp (ec_ident "dmap", [Eident [wa; "darray"]; initf]) + in + { + decl = randombytes_decl "a" n; + locals = []; + stmt = [ESsample ([LvIdent ["a"]], dmap); ESreturn (ec_ident "a")]; + } + in + if Sint.is_empty !(env.randombytes) then [] + else [ + ImoduleType { + name = syscall_mod_sig; + funs = List.map (randombytes_decl "_") (Sint.elements !(env.randombytes)); + }; + Imodule { + name = syscall_mod; + params = []; + ty = Some syscall_mod_sig; + vars = []; + funs = List.map randombytes_f (Sint.elements !(env.randombytes)); + } + ] + +let toec_prog pd asmOp model globs funcs arrsz warrsz randombytes = + let add_glob_env env (x, d) = add_glob (add_glob_arrsz env (x, d)) x in + let env = empty_env pd model funcs arrsz warrsz randombytes + |> fun env -> List.fold_left add_glob_env env globs + |> fun env -> List.fold_left add_arrsz env funcs + in + + let funs = List.map (toec_fun asmOp env) funcs in + + let prefix = !Glob_options.ec_array_path in + Sint.iter (pp_array_decl ~prefix) !(env.arrsz); + Sint.iter (pp_warray_decl ~prefix) !(env.warrsz); + + let pp_arrays arr s = match Sint.elements s with + | [] -> [] + | l -> [IrequireImport (List.map (Format.sprintf "%s%i" arr) l)] + in + let pp_leakages = match model with + | ConstantTime -> [("leakages", "leakages_t")] + | Normal -> [] + in + let mod_arg = + if Sint.is_empty !(env.randombytes) then [] + else [(syscall_mod_arg, syscall_mod_sig)] + in + let import_jleakage = match model with + | Normal -> [] + | ConstantTime -> [IfromRequireImport ("Jasmin", ["JLeakage"])] + in + let glob_imports = [ + IrequireImport ["AllCore"; "IntDiv"; "CoreMap"; "List"; "Distr"]; + IfromRequireImport ("Jasmin", [jmodel ()]); + Iimport [lib_slh ()]; + ] in + let top_mod = Imodule { + name = "M"; + params = mod_arg; + ty = None; + vars = pp_leakages; + funs; + } in + glob_imports @ + import_jleakage @ + (pp_arrays "Array" !(env.arrsz)) @ + (pp_arrays "WArray" !(env.warrsz)) @ + (List.map (fun glob -> ec_glob_decl env glob) globs) @ + (ec_randombytes env) @ + [top_mod] - let env = empty_env model funcs arrsz warrsz randombytes in - - let env = - List.fold_left (fun env (x, d) -> let env = add_glob_arrsz env (x,d) in add_glob env x) - env globs in - let env = List.fold_left add_arrsz env funcs in - - let prefix = !Glob_options.ec_array_path in - Sint.iter (pp_array_decl ~prefix) !(env.arrsz); - Sint.iter (pp_warray_decl ~prefix) !(env.warrsz); - - let pp_arrays arr fmt s = - let l = Sint.elements s in - let pp_i fmt i = Format.fprintf fmt "%s%i" arr i in - if l <> [] then - Format.fprintf fmt "require import @[%a@].@ " (pp_list "@ " pp_i) l in - - let pp_leakages fmt env = - match env.model with - | ConstantTime -> - Format.fprintf fmt "var leakages : leakages_t@ @ " - | Normal -> () in - - let pp_mod_arg fmt env = - if not (Sint.is_empty !(env.randombytes)) then - Format.fprintf fmt "(%s:%s)" syscall_mod_arg syscall_mod_sig in - - let pp_mod_arg_sig fmt env = - if not (Sint.is_empty !(env.randombytes)) then - let pp_randombytes_decl fmt n = - Format.fprintf fmt "proc randombytes_%i (_:W8.t %a.t) : W8.t %a.t" n (pp_Array env) n (pp_Array env) n in - Format.fprintf fmt "module type %s = {@ @[%a@]@ }.@ @ " - syscall_mod_sig - (pp_list "@ " pp_randombytes_decl) (Sint.elements !(env.randombytes)); - let pp_randombytes_proc fmt n = - Format.fprintf fmt "proc randombytes_%i (a:W8.t %a.t) : W8.t %a.t = {@ a <$ @[(dmap %a.darray@ (fun a => (%a.init (fun i => (%a.get8 a i)))))@];@ return a;@ }" - n (pp_Array env) n (pp_Array env) n (pp_WArray env) n - (pp_Array env) n (pp_WArray env) n - in - Format.fprintf fmt - "module %s : %s = {@ @[%a@]@ }.@ @ " - syscall_mod syscall_mod_sig - (pp_list "@ @ " pp_randombytes_proc) (Sint.elements !(env.randombytes)) - in +let pp_prog pd asmOp fmt model globs funcs arrsz warrsz randombytes = + pp_ec_prog fmt (toec_prog pd asmOp model globs funcs arrsz warrsz randombytes); + Format.fprintf fmt "@." - Format.fprintf fmt - "@[%s.@ %s %s.@ %s@ @ %s@ %a%a@ %a@ @ %amodule M%a = {@ @[%a%a@]@ }.@ @]@." - "require import AllCore IntDiv CoreMap List Distr" - "from Jasmin require import" - (jmodel ()) - (require_lib_slh ()) - (if env.model = ConstantTime then "from Jasmin require import JLeakage." else "") - (pp_arrays "Array") !(env.arrsz) - (pp_arrays "WArray") !(env.warrsz) - (pp_list "@ @ " (pp_glob_decl env)) globs - pp_mod_arg_sig env - pp_mod_arg env - pp_leakages env - (pp_list "@ @ " (pp_fun pd asmOp env)) funcs - let rec used_func f = used_func_c Ss.empty f.f_body @@ -1401,8 +1400,5 @@ let extract pd asmOp fmt model ((globs,funcs):('info, 'asm) prog) tokeep = let arrsz = ref Sint.empty in let warrsz = ref Sint.empty in let randombytes = ref Sint.empty in - (* Do first a dummy printing to collect the Arrayi WArrayi RandomBytes ... *) - let dummy_fmt = Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ()) in - pp_prog pd asmOp dummy_fmt model globs funcs arrsz warrsz randombytes; - pp_prog pd asmOp fmt model globs funcs arrsz warrsz randombytes + pp_prog pd asmOp fmt model globs funcs arrsz warrsz randombytes diff --git a/compiler/src/toEC.mli b/compiler/src/toEC.mli index 49f82bff2..6f9438448 100644 --- a/compiler/src/toEC.mli +++ b/compiler/src/toEC.mli @@ -6,5 +6,3 @@ val extract : Format.formatter -> Utils.model -> ('info, ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op, 'extra_op) Arch_extra.extended_op) Prog.prog -> string list -> unit - -val init_use : ('info, 'asm) Prog.func list -> Prog.Sf.t * Prog.Sf.t