include "Clight/Csyntax.ma". include "Clight/TypeComparison.ma". (* Attempt to remove unnecessary integer casts in Clight programs. This differs from the OCaml prototype by attempting to recursively determine whether subexpressions can be changed rather than using a fixed size pattern. As a result more complex expressions such as (char)((int)x + (int)y + (int)z) where x,y and z are chars can be simplified. A possible improvement that doesn't quite fit into this scheme would be to spot that casts can be removed in expressions like (int)x == (int)y where x and y have some smaller integer type. *) (* Attempt to squeeze integer constant into a given type. This might be too conservative --- if we're going to cast it anyway, can't I just ignore the fact that the integer doesn't fit? *) let rec reduce_bits (n,m:nat) (exp:bool) (v:BitVector (plus n (S m))) on n : option (BitVector (S m)) ≝ match n return λn. BitVector (n+S m) → option (BitVector (S m)) with [ O ⇒ λv. Some ? v | S n' ⇒ λv. if eq_b (head' ?? v) exp then reduce_bits ?? exp (tail ?? v) else None ? ] v. definition pred_bitsize_of_intsize : intsize → nat ≝ λsz. pred (bitsize_of_intsize sz). definition signed : signedness → bool ≝ λsg. match sg with [ Unsigned ⇒ false | Signed ⇒ true ]. let rec simplify_int (sz,sz':intsize) (sg,sg':signedness) (i:bvint sz) : option (bvint sz') ≝ let bit ≝ signed sg ∧ head' … i in match nat_compare (pred_bitsize_of_intsize sz) (pred_bitsize_of_intsize sz') return λn,m,x.BitVector (S n) → option (BitVector (S m)) with [ nat_lt _ _ ⇒ λi. None ? (* refuse to make constants larger *) | nat_eq _ ⇒ λi. Some ? i | nat_gt x y ⇒ λi. match reduce_bits ?? bit (i⌈BitVector (S (y+S x))↦BitVector ((S x) + (S y))⌉) with [ Some i' ⇒ if signed sg' then if eq_b bit (head' … i') then Some ? i' else None ? else Some ? i' | None ⇒ None ? ] ] i. >(commutative_plus_faster (S x)) @refl qed. (* Compare integer types to decide if we can omit casts. *) inductive inttype_cmp : Type[0] ≝ | itc_le : inttype_cmp | itc_no : inttype_cmp. definition inttype_compare ≝ λt1,t2. match t1 with [ Tint sz sg ⇒ match t2 with [ Tint sz' sg' ⇒ match sz with [ I8 ⇒ itc_le | I16 ⇒ match sz' with [ I8 ⇒ itc_no | _ ⇒ itc_le ] | I32 ⇒ match sz' with [ I32 ⇒ itc_le | _ ⇒ itc_no ] ] | _ ⇒ itc_no ] | _ ⇒ itc_no ]. (* Operations where it is safe to use a smaller integer type on the assumption that we would cast it down afterwards anyway. *) definition binop_simplifiable ≝ λop. match op with [ Oadd ⇒ true | Osub ⇒ true | _ ⇒ false ]. (* simplify_expr [e] [ty'] takes an expression e and a desired type ty', and returns a flag stating whether the desired type was achieved and a simplified version of e. *) let rec simplify_expr (e:expr) (ty':type) : bool × expr ≝ match e with [ Expr ed ty ⇒ match ed with [ Econst_int sz i ⇒ match ty with [ Tint _ sg ⇒ match ty' with [ Tint sz' sg' ⇒ match simplify_int sz sz' sg sg' i with [ Some i' ⇒ 〈true, Expr (Econst_int sz' i') ty'〉 | None ⇒ 〈false, e〉 ] | _ ⇒ 〈false, e〉 ] | _ ⇒ 〈false, e〉 ] | Ederef e1 ⇒ let ty1 ≝ typeof e1 in 〈type_eq ty ty',Expr (Ederef (\snd (simplify_expr e1 ty1))) ty〉 | Eaddrof e1 ⇒ let ty1 ≝ typeof e1 in 〈type_eq ty ty',Expr (Eaddrof (\snd (simplify_expr e1 ty1))) ty〉 | Eunop op e1 ⇒ let ty1 ≝ typeof e1 in 〈type_eq ty ty',Expr (Eunop op (\snd (simplify_expr e1 ty1))) ty〉 | Ebinop op e1 e2 ⇒ if binop_simplifiable op then let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty' in let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty' in if desired_type1 ∧ desired_type2 then 〈true, Expr (Ebinop op e1' e2') ty'〉 else let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty in let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in 〈false, Expr (Ebinop op e1' e2') ty〉 else let 〈desired_type1, e1'〉 ≝ simplify_expr e1 (typeof e1) in let 〈desired_type2, e2'〉 ≝ simplify_expr e2 (typeof e2) in 〈type_eq ty ty', Expr (Ebinop op e1' e2') ty〉 | Ecast ty e1 ⇒ match inttype_compare ty' ty with [ itc_le ⇒ let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty' in if desired_type then 〈true, e1'〉 else let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty in if desired_type then 〈false, e1'〉 else 〈false, Expr (Ecast ty e1') ty〉 | itc_no ⇒ let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty in if desired_type then 〈false, e1'〉 else 〈false, Expr (Ecast ty e1') ty〉 ] | Econdition e1 e2 e3 ⇒ let 〈irrelevant, e1'〉 ≝ simplify_expr e1 (typeof e1) in (* TODO try to reduce size *) let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty' in let 〈desired_type3, e3'〉 ≝ simplify_expr e3 ty' in if desired_type2 ∧ desired_type3 then 〈true, Expr (Econdition e1' e2' e3') ty'〉 else let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in let 〈desired_type3, e3'〉 ≝ simplify_expr e3 ty in 〈false, Expr (Econdition e1' e2' e3') ty〉 (* Could probably do better with these, too. *) | Eandbool e1 e2 ⇒ let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty in let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in 〈type_eq ty ty', Expr (Eandbool e1' e2') ty〉 | Eorbool e1 e2 ⇒ let 〈desired_type1, e1'〉 ≝ simplify_expr e1 ty in let 〈desired_type2, e2'〉 ≝ simplify_expr e2 ty in 〈type_eq ty ty', Expr (Eorbool e1' e2') ty〉 (* Could also improve Esizeof *) | Efield e1 f ⇒ let ty1 ≝ typeof e1 in 〈type_eq ty ty',Expr (Efield (\snd (simplify_expr e1 ty1)) f) ty〉 | Ecost l e1 ⇒ let 〈desired_type, e1'〉 ≝ simplify_expr e1 ty' in 〈desired_type, Expr (Ecost l e1') (typeof e1')〉 | _ ⇒ 〈type_eq ty ty',e〉 ] ]. definition simplify_e ≝ λe. \snd (simplify_expr e (typeof e)). let rec simplify_statement (s:statement) : statement ≝ match s with [ Sskip ⇒ Sskip | Sassign e1 e2 ⇒ Sassign (simplify_e e1) (simplify_e e2) | Scall eo e es ⇒ Scall (option_map ?? simplify_e eo) (simplify_e e) (map ?? simplify_e es) | Ssequence s1 s2 ⇒ Ssequence (simplify_statement s1) (simplify_statement s2) | Sifthenelse e s1 s2 ⇒ Sifthenelse (simplify_e e) (simplify_statement s1) (simplify_statement s2) (* TODO: try to reduce size of e *) | Swhile e s1 ⇒ Swhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *) | Sdowhile e s1 ⇒ Sdowhile (simplify_e e) (simplify_statement s1) (* TODO: try to reduce size of e *) | Sfor s1 e s2 s3 ⇒ Sfor (simplify_statement s1) (simplify_e e) (simplify_statement s2) (simplify_statement s3) (* TODO: reduce size of e *) | Sbreak ⇒ Sbreak | Scontinue ⇒ Scontinue | Sreturn eo ⇒ Sreturn (option_map ?? simplify_e eo) | Sswitch e ls ⇒ Sswitch (simplify_e e) (simplify_ls ls) | Slabel l s1 ⇒ Slabel l (simplify_statement s1) | Sgoto l ⇒ Sgoto l | Scost l s1 ⇒ Scost l (simplify_statement s1) ] and simplify_ls ls ≝ match ls with [ LSdefault s ⇒ LSdefault (simplify_statement s) | LScase sz i s ls' ⇒ LScase sz i (simplify_statement s) (simplify_ls ls') ]. definition simplify_function : function → function ≝ λf. mk_function (fn_return f) (fn_params f) (fn_vars f) (simplify_statement (fn_body f)). definition simplify_fundef : clight_fundef → clight_fundef ≝ λf. match f with [ CL_Internal f ⇒ CL_Internal (simplify_function f) | _ ⇒ f ]. definition simplify_program : clight_program → clight_program ≝ λp. transform_program … p simplify_fundef.