open Pretty
open Cil

let isSignedType (t: typ): bool =
        match (unrollType t) with
        | TInt(ik,_) -> isSigned ik;
        |_ -> true;

class chkIntVisitor = object
  inherit nopCilVisitor

  method vexpr (e: exp) : exp visitAction =
                (* only check if result is a signed type (which would be
                 * able to hold the correct signed result) *)
    match e with
    | CastE( castedType, BinOp(_, e1, e2, binOpType) ) when (isSignedType castedType) -> begin
            let bitsCasted = bitsSizeOf castedType and bitsOp = bitsSizeOf binOpType in
            if (bitsCasted < bitsOp) then begin
                    ignore(warn "cast looses significant bits %a(%d) ->  %a(%d) in expr: %a\n"
                    d_type binOpType bitsOp
                    d_type castedType bitsCasted
                    d_exp e);
                    DoChildren;
            end
            else
                    let t1 = typeOf (stripCasts e1) and t2 = typeOf (stripCasts e2) in
                    match t1,t2 with
                    |TInt(ik1,_),TInt(ik2,_) -> begin
                            (* one of the operands is signed, but the binop result
                             * is an unsigned type, while the castedType is a
                             * signed type capable of holding the signed result *)
                            if (isSigned ik1) != (isSigned ik2) &&
                            not (isSignedType binOpType) && (not (isIntegralType castedType) ||
                            (bitsCasted > bitsOp)) then
                                    ignore(warn "conversion looses sign in expression: %a  ;
                                    operands:%a,%a -> op-result: %a(%d) -> casted: %a(%d)\n"
                                    d_exp e
                                    d_ikind ik1
                                    d_ikind ik2
                                    d_type binOpType
                                    bitsOp
                                    d_type castedType
                                    bitsCasted
                                    );

                            DoChildren;
                    end
                    | _ -> DoChildren;
    end
    | BinOp( (Lt|Le|Gt|Ge) , _, CastE( castedType, (SizeOf(_) | SizeOfE(_) | SizeOfStr(_)) ), _) | BinOp((Lt|Le|Gt|Ge), CastE( castedType, (SizeOf(_) | SizeOfE(_) | SizeOfStr(_)) ), _, _)  when (isSignedType castedType) ->
        ignore(warn "sizeof expression is cast to signed type in expression: %a; type: %a
                                                                 if this is a bounds test, make sure you also test the lower bound!"
                 d_exp e d_type castedType);
        DoChildren;
    |_ -> DoChildren
end

let feature : featureDescr =
  { fd_name = "chkints";
    fd_enabled = ref false;
    fd_description = "check compatibilty of integer types";
    fd_extraopt = [];
    fd_doit =
    (function (f: file) ->
      let ciVisitor = new chkIntVisitor in
      visitCilFileSameGlobals ciVisitor f);
    fd_post_check = true;
  }