Added new diagnostic for non-linear conditionals

The new diagnostics is triggered if a conditional is used that
may not be transformed into linear code by the later by the
if conversion.

The new diagnostic is emitted if a conditional may contain an
unsafe expression or is contained within another conditional,
logical and or logical or expression. An expression is unsafe if
it contains a call, changes memory or if its evaluation leads to
undefined behavior, for example division and modulo.

Also fixes a small typo in a comment in Cutil.

6 files changed, 179 insertions, 1 deletions

diff --git a/cparser/Checks.ml b/cparser/Checks.ml
index 94570f4e..e79e3ccf 100644
--- a/cparser/Checks.ml
+++ b/cparser/Checks.ml
@@ -212,3 +212,166 @@ let unused_variables p =
   traverse_program
     ~fundef:fundef
     p
+
+(* Warning for conditionals that cannot be transformed into linear code *)
+
+(* Compute the set of local variables that do not have their address taken *)
+
+let rec non_stack_locals_expr vars e =
+  match e.edesc with
+  | ECast (_,e) -> non_stack_locals_expr vars e
+  | EUnop (Oaddrof,e) ->
+    begin match e.edesc with
+    | EVar id ->
+      IdentSet.remove id vars
+    | _ -> vars
+    end
+  | EUnop (Oderef, e) ->
+    (* Special optimization *(& ...) is removed in SimplExpr *)
+    begin match e.edesc with
+      | EUnop (Oaddrof,e) -> non_stack_locals_expr vars e
+      | _ -> non_stack_locals_expr vars e
+    end
+  | EUnop (_, e) ->
+    non_stack_locals_expr vars e
+  | EBinop (_,e1,e2,_) ->
+    let vars = non_stack_locals_expr vars e1 in
+    non_stack_locals_expr vars e2
+  | EConditional (e1,e2,e3) ->
+    let vars = non_stack_locals_expr vars e1 in
+    let vars = non_stack_locals_expr vars e2 in
+    non_stack_locals_expr vars e3
+  | ECompound (_,init) -> non_stack_locals_init vars init
+  | ECall (e,p) ->
+    let vars = non_stack_locals_expr vars e in
+    List.fold_left non_stack_locals_expr vars p
+  | _ -> vars
+
+and non_stack_locals_init vars init =
+  fold_over_init ~expr:non_stack_locals_expr vars init
+
+let add_vars env vars (id,ty) =
+  let volatile = List.mem AVolatile (attributes_of_type env ty) in
+  if not volatile then
+    IdentSet.add id vars
+  else
+    vars
+
+let non_stack_locals_stmt env vars s =
+  let decl vars loc (sto, id, ty, init) =
+    let vars = match init with
+      | Some init -> non_stack_locals_init vars init
+      | None -> vars in
+    add_vars env vars (id,ty) in
+  fold_over_stmt ~expr:non_stack_locals_expr ~decl:decl
+    vars s
+
+(* Check whether an expression is safe and can be always evaluated *)
+
+let safe_cast env tfrom tto =
+  match unroll env tfrom, unroll env tto with
+  | (TInt _ | TPtr _ | TArray _ | TFun _ | TEnum _),
+    (TInt _ | TPtr _ | TEnum _) -> true
+  | TFloat _, TFloat _ -> true
+  | _, _ -> equal_types env tfrom tto
+
+let safe_expr vars env e =
+  let rec expr e =
+    match e.edesc with
+    | EConst _ | ESizeof _ | EAlignof _   | ECompound _  -> true
+    | EVar id -> (IdentSet.mem id vars) || not (is_scalar_type env e.etyp)
+    | ECast (ty, e) ->
+      safe_cast env e.etyp ty && expr e
+    | EUnop (op, e) ->
+      unop op  e
+    | EBinop (op, e1, e2, ty) ->
+      binop op e1  e2
+    | EConditional _  -> false
+    | ECall _ -> false
+  and binop op e1 e2 =
+    let is_long_long_type ty =
+      match unroll env ty with
+      | TInt (ILongLong, _)
+      | TInt (IULongLong, _) -> true
+      | _ -> false in
+    match op with
+    | Oadd | Osub | Omul | Oand | Oor | Oxor | Oshl | Oshr ->
+      expr e1 && expr e2
+    | Oeq | One | Olt | Ogt | Ole | Oge ->
+      let not_long_long = not (is_long_long_type e1.etyp) && not (is_long_long_type e2.etyp) in
+      not_long_long && expr e1 && expr e2
+    | _ -> false
+  (* x.f if f has array or struct or union type *)
+  and unop  op e =
+    match op with
+    | Ominus | Onot | Olognot | Oplus -> expr e
+    | Oaddrof ->
+      begin match e.edesc with
+        (* skip &*e *)
+        | EUnop (Oderef, e) -> expr e
+        (* skip &(e.f) *)
+        | EUnop (Odot f, e) -> expr e
+        | _ -> expr e
+      end
+    (* skip *&e *)
+    | Oderef ->
+      begin match e.edesc with
+        | EUnop (Oaddrof,e) -> expr e
+        | _ -> expr e
+      end
+    (* e.f is okay if f has array or composite type *)
+    | Odot m ->
+      let fld = field_of_dot_access env e.etyp m in
+      (is_array_type env fld.fld_typ || is_composite_type env fld.fld_typ) && expr e
+    | _ -> false in
+  expr e
+
+(* Check expressions if they contain conditionals that cannot be transformed in
+   linear code. The inner_cond parameter is used to mimic the translation of short
+   circuit logical or and logical and as well as conditional to if statements in
+   SimplExpr. *)
+
+let rec non_linear_cond_expr inner_cond vars env loc e =
+  match e.edesc with
+  | EConst _ | ESizeof _ | EAlignof _ | EVar _ -> ()
+  | ECast (_ , e) | EUnop (_, e)-> non_linear_cond_expr false vars env loc e
+  | EBinop (op, e1, e2, ty) ->
+    let inner_cond = match op with
+      | Ocomma -> inner_cond
+      | Ologand | Ologor -> true
+      | _ -> false
+    in
+    non_linear_cond_expr false vars env loc e1;
+    non_linear_cond_expr inner_cond vars env loc e2
+  | EConditional (c, e1, e2) ->
+    let can_cast = safe_cast env e1.etyp e.etyp && safe_cast env e2.etyp e.etyp in
+    if not can_cast || inner_cond || not (safe_expr vars env e1) || not (safe_expr vars env e2) then
+      warning loc Non_linear_cond_expr "conditional expression may not be linearized";
+    non_linear_cond_expr true vars env loc e1;
+    non_linear_cond_expr true vars env loc e2;
+  | ECompound (ty, init) -> non_linear_cond_init vars env loc init
+  | ECall (e, params) ->
+    non_linear_cond_expr false vars env loc e;
+    List.iter (non_linear_cond_expr false vars env loc) params
+
+and non_linear_cond_init vars env loc init =
+  iter_over_init ~expr:(non_linear_cond_expr false vars env loc) init
+
+let non_linear_cond_stmt vars env s =
+  let decl loc (sto, id, ty, init) =
+    match init with
+    | None -> ()
+    | Some init -> non_linear_cond_init vars env loc init in
+  iter_over_stmt_loc ~expr:(non_linear_cond_expr false vars env) ~decl:decl s
+
+let non_linear_conditional p =
+  if active_warning Non_linear_cond_expr then begin
+    let fundef env loc fd =
+      let vars = List.fold_left (add_vars env) IdentSet.empty fd.fd_params in
+      let vars = non_stack_locals_stmt env vars fd.fd_body in
+      non_linear_cond_stmt vars env fd.fd_body;
+    in
+    traverse_program
+      ~fundef:fundef
+      p
+  end
diff --git a/cparser/Checks.mli b/cparser/Checks.mli
index 4d61a5b8..cfd7b04d 100644
--- a/cparser/Checks.mli
+++ b/cparser/Checks.mli
@@ -16,3 +16,5 @@
 val unknown_attrs_program: C.program -> unit
 
 val unused_variables: C.program -> unit
+
+val non_linear_conditional : C.program -> unit
diff --git a/cparser/Cutil.mli b/cparser/Cutil.mli
index 3777c321..f6c4627d 100644
--- a/cparser/Cutil.mli
+++ b/cparser/Cutil.mli
@@ -167,7 +167,7 @@ val is_scalar_type : Env.t -> typ -> bool
 val is_composite_type : Env.t -> typ -> bool
   (* Is type a struct or union? *)
 val is_array_type : Env.t -> typ -> bool
-  (* Is type a array type? *)
+  (* Is type an array type? *)
 val is_function_type : Env.t -> typ -> bool
   (* Is type a function type? (not pointer to function) *)
 val is_function_pointer_type : Env.t -> typ -> bool
diff --git a/cparser/Diagnostics.ml b/cparser/Diagnostics.ml
index 51dcab47..012e4b66 100644
--- a/cparser/Diagnostics.ml
+++ b/cparser/Diagnostics.ml
@@ -102,6 +102,7 @@ type warning_type =
   | Flexible_array_extensions
   | Tentative_incomplete_static
   | Reduced_alignment
+  | Non_linear_cond_expr
 
 (* List of active warnings *)
 let active_warnings: warning_type list ref = ref [
@@ -163,6 +164,7 @@ let string_of_warning = function
   | Flexible_array_extensions -> "flexible-array-extensions"
   | Tentative_incomplete_static -> "tentative-incomplete-static"
   | Reduced_alignment -> "reduced-alignment"
+  | Non_linear_cond_expr -> "non-linear-cond-expr"
 
 (* Activate the given warning *)
 let activate_warning w () =
@@ -216,6 +218,7 @@ let wall () =
     Flexible_array_extensions;
     Tentative_incomplete_static;
     Reduced_alignment;
+    Non_linear_cond_expr;
   ]
 
 let wnothing () =
@@ -253,6 +256,7 @@ let werror () =
     Flexible_array_extensions;
     Tentative_incomplete_static;
     Reduced_alignment;
+    Non_linear_cond_expr;
   ]
 
 (* Generate the warning key for the message *)
@@ -437,6 +441,7 @@ let warning_options =
   error_option Flexible_array_extensions @
   error_option Tentative_incomplete_static @
   error_option Reduced_alignment @
+  error_option Non_linear_cond_expr @
   [Exact ("-Wfatal-errors"), Set error_fatal;
    Exact ("-fdiagnostics-color"), Ignore; (* Either output supports it or no color *)
    Exact ("-fno-diagnostics-color"), Unset color_diagnostics;
@@ -492,3 +497,6 @@ let crash exn =
 let no_loc = ("", -1)
 
 let file_loc file = (file,-10)
+
+let active_warning ty =
+  fst (classify_warning ty) <> SuppressedMsg
diff --git a/cparser/Diagnostics.mli b/cparser/Diagnostics.mli
index 6a3c11c8..0f0a0ea5 100644
--- a/cparser/Diagnostics.mli
+++ b/cparser/Diagnostics.mli
@@ -55,6 +55,7 @@ type warning_type =
   | Flexible_array_extensions      (** usange of structs with flexible arrays in structs and arrays *)
   | Tentative_incomplete_static    (** static tentative definition with incomplete type *)
   | Reduced_alignment              (** alignment reduction *)
+  | Non_linear_cond_expr           (** condition that cannot be linearized *)
 
 val warning  : (string * int) -> warning_type -> ('a, Format.formatter, unit, unit, unit, unit) format6 -> 'a
 (** [warning (f,c) w fmt arg1 ... argN] formats the arguments [arg1] to [argN] as warining according to
@@ -95,3 +96,6 @@ val file_loc : string -> string * int
 
 val error_summary : unit -> unit
 (** Print a summary containing the numbers of errors encountered *)
+
+val active_warning : warning_type -> bool
+(** Test whether a warning is active to avoid costly checks *)
diff --git a/cparser/Elab.ml b/cparser/Elab.ml
index 10380152..4d27598f 100644
--- a/cparser/Elab.ml
+++ b/cparser/Elab.ml
@@ -3095,4 +3095,5 @@ let elab_file prog =
   let p = elaborated_program () in
   Checks.unused_variables p;
   Checks.unknown_attrs_program p;
+  Checks.non_linear_conditional p;
   p