[logic] better typed expr_to_term conversion

argument of ACSL `!` is supposed to be a boolean, not an int

src/kernel_services/ast_queries/logic_utils.ml

@@ -334,39 +334,42 @@ let is_zero_comparable t =
   | Ltype _ -> false
   | Lvar _ | Larrow _ -> false
 
-let scalar_term_to_predicate t =
+let scalar_term_conversion conversion t =
   let loc = t.term_loc in
-  let conversion zero = prel ~loc (Cil_types.Rneq, t, zero) in
-  let arith_conversion () = conversion (Cil.lzero ~loc ()) in
-  let ptr_conversion () = conversion (Logic_const.term ~loc Tnull t.term_type)
+  let arith_conversion () = conversion ~loc (Cil.lzero ~loc ()) t in
+  let ptr_conversion () =
+    conversion ~loc (Logic_const.term ~loc Tnull t.term_type) t
   in
   match unroll_type t.term_type with
   | Ctype (TInt _) -> arith_conversion ()
   | Ctype (TFloat _) ->
-    conversion
-      (Logic_const.treal_zero ~loc ~ltyp:t.term_type ())
+    conversion ~loc (Logic_const.treal_zero ~loc ~ltyp:t.term_type ()) t
   | Ctype (TPtr _) -> ptr_conversion ()
   | Ctype (TArray _) -> ptr_conversion ()
   (* Could be transformed to \true: an array is never \null *)
   | Ctype (TFun _) -> ptr_conversion ()
   (* decay as pointer *)
   | Linteger -> arith_conversion ()
-  | Lreal -> conversion (Logic_const.treal_zero ~loc ())
+  | Lreal -> conversion ~loc (Logic_const.treal_zero ~loc ()) t
   | Ltype ({lt_name = name},[]) when name = Utf8_logic.boolean ->
-    let ctrue = Logic_env.Logic_ctor_info.find "\\true" in
-    prel ~loc
-      (Cil_types.Req,t,
-       { term_node = TDataCons(ctrue,[]);
-         term_loc = loc;
-         term_type = Ltype(ctrue.ctor_type,[]);
-         term_name = [];
-       })
+    let ctrue = Logic_env.Logic_ctor_info.find "\\false" in
+    conversion ~loc (term ~loc (TDataCons(ctrue,[])) boolean_type) t
   | Ltype _ | Lvar _ | Larrow _
   | Ctype (TVoid _ | TNamed _ | TComp _ | TEnum _ | TBuiltin_va_list _)
     -> Kernel.fatal
-         "Cannot convert to predicate a term of type %a"
+         "Cannot convert a term of type %a"
          Cil_printer.pp_logic_type t.term_type
 
+let scalar_term_to_predicate =
+  let conversion ~loc zero t = prel ~loc (Cil_types.Rneq, t, zero) in
+  scalar_term_conversion conversion
+
+let scalar_term_to_boolean =
+  let conversion ~loc zero t =
+    term ~loc (TBinOp(Ne,t,zero)) Logic_const.boolean_type
+  in
+  scalar_term_conversion conversion
+
 let rec expr_to_term ~cast e =
   let e_typ = unrollType (Cil.typeOf e) in
   let loc = e.eloc in
@@ -403,6 +406,21 @@ let rec expr_to_term ~cast e =
       end
     | UnOp (op, u, _) ->
       let u' = expr_to_term_coerce ~cast u in
+      let u' =
+        match op with
+        | Cil_types.LNot ->
+          (match u'.term_node with
+           | TCastE(_, t) when is_boolean_type t.term_type -> t
+           | _ when is_boolean_type u'.term_type -> u'
+           | _ when is_zero_comparable u' ->
+             scalar_term_to_boolean u'
+           | _ ->
+             Kernel.fatal
+               "expr_to_term: unexpected argument of ! operator %a, \
+                converted to %a"
+               Cil_printer.pp_exp u Cil_printer.pp_term u')
+        | _ -> u'
+      in
       (* See comments for binop case above. *)
       let tcast = match op, cast with
         | Cil_types.LNot, _ -> Some Logic_const.boolean_type