CHC: fix memory variable creation

Author: sipma

CodeHawk/CHC/cchanalyze/cCHAssignmentTranslator.ml

@@ -81,11 +81,26 @@ object (self)
         let assign =
 	  if chifVar#isTmp then
             let memoryvars = env#get_memory_variables in
+            let _ =
+              chlog#add
+                "abstract memory variables"
+                (LBLOCK [
+                     pretty_print_list
+                       memoryvars (fun v -> v#toPretty) "" ", " ""]) in
             CCMD (ABSTRACT_VARS memoryvars)
 	  else if env#has_constant_offset chifVar then
 	    make_c_cmd (ASSIGN_NUM (chifVar, numExp))
           else
             let memoryvars = env#get_memory_variables_with_base chifVar in
+            let _ =
+              chlog#add
+                "abstract memory variables with base"
+                (LBLOCK [
+                     STR "base: ";
+                     chifVar#toPretty;
+                     STR "; ";
+                     pretty_print_list
+                       memoryvars (fun v -> v#toPretty) "[" ", " "]"]) in
             CCMD (ABSTRACT_VARS memoryvars) in
         [rhsCode; assign]
       with

CodeHawk/CHC/cchanalyze/cCHEnvironment.ml

@@ -522,7 +522,7 @@ object(self)
 
   method get_memory_variables_with_base (v:variable_t) =
     let memvars = self#get_memory_variables in
-    if self#is_memory_address v then
+    if self#is_memory_address v || self#is_memory_variable v then
       let memref = self#get_memory_reference v in
       List.filter (fun mv ->
           memref#index = (self#get_memory_reference mv)#index) memvars

CodeHawk/CHC/cchanalyze/cCHExpTranslator.ml

@@ -33,6 +33,9 @@ open CHLanguage
 open CHNumerical
 open CHPretty
 
+(* chutil *)
+open CHLogger
+
 (* xprlib *)
 open Xprt
 open XprTypes
@@ -157,16 +160,16 @@ object (self)
        else
          env#mk_program_var vinfo eoffset NUM_VAR_TYPE
     | (Var _, _) -> env#mk_temp NUM_VAR_TYPE
-    | (Mem e,offset) ->
+    | (Mem e, offset) ->
        match self#translate_exp context e with
        | XVar v when env#is_memory_address v ->
-          let (memref,moffset) = env#get_memory_address v in
+          let (memref, moffset) = env#get_memory_address v in
           env#mk_memory_variable
             memref#index (add_offset moffset offset) NUM_VAR_TYPE
        | XVar v when env#is_initial_value v ->
           let memref =
             env#get_variable_manager#memrefmgr#mk_external_reference
-              v (type_of_lval fdecls lval) in
+              v (type_of_exp fdecls e) in
           env#mk_memory_variable memref#index offset NUM_VAR_TYPE
        | XVar _ -> env#mk_temp NUM_VAR_TYPE
        | _ -> env#mk_temp NUM_VAR_TYPE
@@ -193,7 +196,8 @@ object (self)
        begin
          match memxpr with
          | XVar v when env#is_initial_value v || env#is_function_return_value v ->
-            let memref = vmgr#memrefmgr#mk_external_reference v ftype in
+            let memtype = type_of_exp fdecls e in
+            let memref = vmgr#memrefmgr#mk_external_reference v memtype in
             XVar (env#mk_memory_address_value memref#index offset)
          | XVar v when env#is_memory_address v ->
             let (memref, moffset) = env#get_memory_address v in
@@ -435,7 +439,8 @@ object (self)
        begin
          match memxpr with
          | XVar v when env#is_initial_value v || env#is_function_return_value v ->
-            let memref = vmgr#memrefmgr#mk_external_reference v ftype in
+            let memtype = type_of_exp fdecls e in
+            let memref = vmgr#memrefmgr#mk_external_reference v memtype in
             XVar (env#mk_memory_address_value memref#index offset)
          | XVar v when env#is_memory_address v -> XVar v
          | _ ->
@@ -693,7 +698,8 @@ object (self)
        begin
          match memxpr with
          | XVar v when env#is_initial_value v || env#is_function_return_value v ->
-            let memref = vmgr#memrefmgr#mk_external_reference v ftype in
+            let memtype = type_of_exp fdecls e in
+            let memref = vmgr#memrefmgr#mk_external_reference v memtype in
             XVar (env#mk_memory_address_value memref#index offset)
          | XVar v when env#is_memory_address v -> XVar v
          | _ ->
@@ -765,7 +771,7 @@ object (self)
        | XVar v when env#is_initial_value v ->
           let memref =
             env#get_variable_manager#memrefmgr#mk_external_reference
-              v (type_of_lval fdecls lval) in
+              v (type_of_exp fdecls e) in
           env#mk_memory_variable memref#index offset SYM_VAR_TYPE
        | _ ->
           env#mk_temp SYM_VAR_TYPE

CodeHawk/CHC/cchanalyze/cCHGenerateAndCheck.ml

@@ -31,30 +31,20 @@
 open CHAtlas
 open CHCommon
 open CHLanguage
-open CHPEPRDictionary
 open CHPretty
 
 (* chutil *)
 open CHLogger
-open CHPrettyUtil
-open CHTiming
 open CHTimingLog
-open CHXmlDocument
-open CHXmlReader
 
 (* cchlib *)
 open CCHBasicTypes
-open CCHContext
-open CCHFileEnvironment
 open CCHSettings
 open CCHUtilities
 
 (* cchpre *)
-open CCHCallsite
-open CCHPPO
 open CCHPreFileIO
 open CCHPreTypes
-open CCHProofObligation
 open CCHProofScaffolding
 
 (* cchanalyze *)
@@ -75,7 +65,6 @@ module H = Hashtbl
 
 let fenv = CCHFileEnvironment.file_environment
 
-let prr p l = fixed_length_pretty ~alignment:StrRight p l
 let function_to_be_analyzed = ref ""
 
 let max_callcount = 100
@@ -210,6 +199,7 @@ let process_function gspecs fname =
 	          let functionTranslator =
                     gspec.ig_get_function_translator env orakel opsProvider in
 	          let (optSem, sys) = functionTranslator#translate fundec in
+                  (* let _ = pr_debug [sys#toPretty] in *)
 	          let semantics =
                     match optSem with
                     | Some sem -> sem | _ -> default_opsemantics in

CodeHawk/CHC/cchanalyze/cCHPOCheckIndexUpperBound.ml

@@ -183,6 +183,12 @@ object (self)
   method private xpr1_implies_existential_violation invindices x1 x2 =
     match x1 with
     | XVar v -> self#var1_implies_existential_violation invindices v x2
+    | XOp (XPlus, [XVar v; xincr]) ->
+       let xincr = simplify_xpr (XOp (XPlus, [x2; xincr])) in
+       self#var1_implies_existential_violation invindices v xincr
+    | XOp (XMinus, [XVar v; xdecr]) ->
+       let xincr = simplify_xpr (XOp (XMinus, [x2; xdecr])) in
+       self#var1_implies_existential_violation invindices v xincr
     | _ -> None
 
   method private xprlist_implies_existential_violation invindices xl x2 =

CodeHawk/CHC/cchanalyze/cCHPOQuery.ml

@@ -420,24 +420,52 @@ object (self)
     let id = po#index in
     let locinvio = invio#get_location_invariant cfgcontext in
     let facts = locinvio#get_invariants in
-    let vars = List.fold_left (fun acc f ->
-        match f#get_fact with
-        | NonRelationalFact (v, _i) ->
-           if env#check_variable_applies_to_po v ~argindex po#is_ppo id then
-             if List.exists (fun vv -> v#equal vv) acc then
-               acc
-             else
-               v :: acc
-           else
-             acc
-        | _ -> acc) [] facts in
-    List.fold_left (fun acc v ->
-        let invs = locinvio#get_var_invariants v in
-        List.fold_left (fun acc1 inv ->
-            if List.exists (fun inv' -> inv#index = inv'#index) acc1 then
-              acc1
-            else
-              inv :: acc1) acc invs) [] vars
+    match facts with
+    | [] ->
+       begin
+         self#set_diagnostic
+           ("no invariant facts in proof obligation context");
+         []
+       end
+    | _ ->
+       let vars =
+         List.fold_left (fun acc f ->
+             match f#get_fact with
+             | NonRelationalFact (v, _i) ->
+                if env#check_variable_applies_to_po v ~argindex po#is_ppo id then
+                  if List.exists (fun vv -> v#equal vv) acc then
+                    acc
+                  else
+                    v :: acc
+                else
+                  acc
+             | _ -> acc) [] facts in
+       match vars with
+       | [] ->
+          begin
+            self#set_diagnostic
+              ("no invariants found on variables that apply to proof obligation");
+            []
+          end
+       | _ ->
+          let invs =
+            List.fold_left (fun acc v ->
+                let invs = locinvio#get_var_invariants v in
+                List.fold_left (fun acc1 inv ->
+                    if List.exists (fun inv' -> inv#index = inv'#index) acc1 then
+                      acc1
+                    else
+                      inv :: acc1) acc invs) [] vars in
+          match invs with
+          | [] ->
+             begin
+               self#set_diagnostic
+                 ("none of the variables has associated invariants: "
+                  ^ (p2s
+                       (pretty_print_list vars (fun v -> v#toPretty) "[" "," "]")));
+               []
+             end
+          | _ -> invs
 
   method get_invariants_lb (argindex:int) =
     List.sort (fun i1 i2 -> i1#compare_lb i2) (self#get_invariants argindex)