CHC: add diagnostic for missing invariants

Author: sipma

CodeHawk/CHC/cchanalyze/cCHAnalysisTypes.mli

@@ -381,7 +381,7 @@ class type invariant_list_query_int =
   end
 
 
-(** Primary object that keeps track of invariants and can be queries *)
+(** Primary object that keeps track of invariants and can be queried *)
 class type po_query_int =
   object
     method env: c_environment_int

CodeHawk/CHC/cchanalyze/cCHPOCheckIndexLowerBound.ml

@@ -6,7 +6,7 @@
  
    Copyright (c) 2005-2019 Kestrel Technology LLC
    Copyright (c) 2020-2022 Henny Sipma
-   Copyright (c) 2023      Aarno Labs LLC
+   Copyright (c) 2023-2024 Aarno Labs LLC
 
    Permission is hereby granted, free of charge, to any person obtaining a copy
    of this software and associated documentation files (the "Software"), to deal
@@ -29,11 +29,9 @@
 
 (* chlib *)
 open CHNumerical
-open CHPretty
 
 (* chutil *)
 open CHPrettyUtil
-open CHUtil
 
 (* xprlib *)
 open Xprt
@@ -45,7 +43,6 @@ open Xsimplify
 open CCHBasicTypes
 open CCHLibTypes
 open CCHTypesToPretty
-open CCHTypesUtil
 
 (* cchpre *)
 open CCHPOPredicate
@@ -70,19 +67,20 @@ object (self)
 
   method private mk_predicate a = PIndexLowerBound a
 
-  method mk_safe_constraint x = XOp (XGe, [ x ; zero_constant_expr ])
+  method mk_safe_constraint x = XOp (XGe, [x; zero_constant_expr])
 
-  method mk_violation_constraint x = XOp (XLt, [ x ; zero_constant_expr ])
+  method mk_violation_constraint x = XOp (XLt, [x; zero_constant_expr])
 
   (* ----------------------------- safe ------------------------------------- *)
   method  private global_implies_safe invindex g =
     let pred = self#mk_predicate g in
     match poq#check_implied_by_assumptions pred with
     | Some pred ->
-       let deps = DEnvC ([ invindex ],[ GlobalApiAssumption pred ]) in
-       let msg = "index lower bound implied by global assumption: "
-                   ^ (p2s (po_predicate_to_pretty pred)) in
-       Some (deps,msg)
+       let deps = DEnvC ([invindex], [GlobalApiAssumption pred]) in
+       let msg =
+         "index lower bound implied by global assumption: "
+         ^ (p2s (po_predicate_to_pretty pred)) in
+       Some (deps, msg)
     | _ ->
        let xpred = po_predicate_to_xpredicate poq#fenv pred in
        begin
@@ -98,7 +96,7 @@ object (self)
       let r =
         match epcs with
         | [] ->
-           List.fold_left (fun acc (pc,_) ->
+           List.fold_left (fun acc (pc, _) ->
                match acc with
                | Some _ ->  acc
                | _ ->
@@ -131,13 +129,13 @@ object (self)
       let deps = DLocal [invindex] in
       let msg =
         "index: "  ^ (x2s x) ^ " satisfies constraint: " ^ (x2s xconstraint) in
-      Some (deps,msg)
+      Some (deps, msg)
     else if poq#is_global_expression x then
       match self#global_implies_safe invindex (poq#get_global_expression x) with
       | Some r -> Some r
       | _ ->
          begin
-           poq#set_diagnostic ("remaining constraint: " ^ (x2s sconstraint)) ;
+           poq#set_diagnostic ("remaining constraint: " ^ (x2s sconstraint));
            None
          end
     else
@@ -153,12 +151,16 @@ object (self)
 
   method check_safe =
     match invs with
-    | [] -> false
+    | [] ->
+       begin
+         poq#set_diagnostic ("no invariants for " ^ (e2s e));
+         false;
+       end
     | _ ->
        List.fold_left (fun acc inv ->
            acc ||
              match self#inv_implies_safe inv with
-             | Some (deps,msg) ->
+             | Some (deps, msg) ->
                 begin
                   poq#record_safe_result deps msg;
                   true
@@ -174,7 +176,7 @@ object (self)
       match poq#get_witness vconstraint v with
       | Some violationvalue -> 
          let (s, callee, pc) = poq#get_tainted_value_origin v in
-         let deps = DEnvC ([ invindex ],[ PostAssumption (callee.vid,pc) ]) in
+         let deps = DEnvC ([invindex],[PostAssumption (callee.vid,pc)]) in
          let msg =
            s
            ^ " choose value: "
@@ -190,12 +192,12 @@ object (self)
     | XConst (IntConst n) when n#lt numerical_zero ->
        let deps = DLocal [invindex] in
        let msg  = "upper bound on index value is negative: " ^ n#toString in
-       Some (deps,msg)
+       Some (deps, msg)
     | XVar v ->
        self#var_implies_violation invindex v zero_constant_expr
-    | XOp (XPlus, [ XVar v ; xincr ]) ->
+    | XOp (XPlus, [XVar v; xincr]) ->
        self#var_implies_violation invindex v xincr
-    | XOp (XMinus, [ XVar v ; xdecr ]) ->
+    | XOp (XMinus, [XVar v; xdecr]) ->
        let xincr = simplify_xpr (XOp (XMinus, [zero_constant_expr; xdecr])) in
        self#var_implies_violation invindex v xincr
     | _ -> None
@@ -221,7 +223,7 @@ object (self)
                List.fold_left (fun acc x ->
                    match acc with
                    | None -> None
-                   | Some (deps,msg) ->
+                   | Some (deps, msg) ->
                       match self#xpr_implies_violation inv#index x with
                       | Some (d, m) ->
                          let deps = join_dependencies deps d in
@@ -245,7 +247,7 @@ object (self)
                          | Some (d, m) ->
                             let deps = join_dependencies deps d in
                             let msg = msg ^ "; " ^ m in
-                            Some (deps,msg)
+                            Some (deps, msg)
                          | _ -> None) (Some r) tl
                | _ -> None
              end
@@ -264,9 +266,9 @@ object (self)
         List.fold_left (fun acc inv ->
             acc ||
               match self#inv_implies_violation inv with
-              | Some (deps,msg) ->
+              | Some (deps, msg) ->
                  begin
-                   poq#record_violation_result deps msg ;
+                   poq#record_violation_result deps msg;
                    true
                  end
               | _ -> false) false invs
@@ -281,13 +283,13 @@ object (self)
         "condition "
         ^ (p2s (po_predicate_to_pretty pred))
         ^ " delegated to the api" in
-      Some (deps,msg)
+      Some (deps, msg)
     else
       None
 
   method private inv_implies_delegation inv =
     match inv#lower_bound_xpr with
-    | Some  x -> self#xpr_implies_delegation inv#index x
+    | Some x -> self#xpr_implies_delegation inv#index x
     | _ -> None
 
   method check_delegation =
@@ -297,7 +299,7 @@ object (self)
        List.fold_left (fun acc inv ->
            acc ||
              match self#inv_implies_delegation inv with
-             | Some (deps,msg) ->
+             | Some (deps, msg) ->
                 begin
                   poq#record_safe_result deps msg;
                   true