CHB:ARM: analyze with loop counters

Author: sipma

CodeHawk/CHB/bchanalyze/bCHAnalyzeProcedure.ml

@@ -91,7 +91,7 @@ let analyze_procedure_with_linear_equalities
   begin
     analysis_setup#addLinearEqualities;
     analysis_setup#setOpSemantics (default_opsemantics "karr");
-    analysis_setup#analyze_procedure system proc
+    analysis_setup#analyze_procedure system ~do_loop_counters:true proc
   end
 
 let analyze_procedure_with_intervals (proc:procedure_int) (system:system_int) =

CodeHawk/CHB/bchanalyze/bCHExtractInvariants.ml

@@ -232,6 +232,16 @@ let extract_external_value_equalities
 
 
 let extract_relational_facts finfo iaddr domain =
+  let vars = domain#observer#getObservedVariables in
+  let lcs =
+    List.filter (fun v -> match v#getType with NUM_LOOP_COUNTER_TYPE -> true | _ -> false)
+      vars in
+  let _ =
+    ch_diagnostics_log#add
+      "project out loopcounters"
+      (LBLOCK [STR iaddr; STR ": ";
+               pretty_print_list lcs (fun v -> v#toPretty) "[" ", " "]"]) in
+  let domain = domain#projectOut lcs in
   let constraints = domain#observer#getNumericalConstraints ~variables:None () in
   List.iter (finfo#finv#add_lineq iaddr) constraints
 

CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml

@@ -726,7 +726,7 @@ object (self:'a)
     | ARMImmediate _ ->
        let num = self#to_numerical in
        (try
-          num#toInt >= 0 && num#toInt < 5
+          num#toInt >= 0 && num#toInt < 7
         with
         | _ -> false)
     | _ -> false

CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml

@@ -159,7 +159,7 @@ object (self)
         () in
     let rewrite_expr ?(restrict:int option) (x: xpr_t): xpr_t =
       try
-        let xpr = floc#inv#rewrite_expr x in
+        let xpr = floc#inv#rewrite_expr ~loopcounter:true x in
         let xpr = simplify_xpr xpr in
         let xpr =
           let vars = variables_in_expr xpr in

CodeHawk/CHB/bchlibarm32/bCHTranslateARMToCHIF.ml

@@ -1987,6 +1987,8 @@ let translate_arm_instruction
        | 2 -> 4
        | 3 -> 8
        | 4 -> 16
+       | 5 -> 32
+       | 6 -> 64
        | _ -> 1 in  (* not reachable by small immediate *)
      let usevars = get_register_vars [rn] in
      let usehigh = get_use_high_vars_r [xxrn_r] in

CodeHawk/CHB/bchlibmips32/bCHTranslateMIPSToCHIF.ml

@@ -268,7 +268,7 @@ let translate_mips_instruction
   let frozenasserts =
     List.map (fun (v, fv) -> ASSERT (EQ (v, fv)))
       (finfo#get_test_variables ctxtiaddr) in
-  let rewrite_expr floc x:xpr_t =
+  let rewrite_expr (floc: floc_int) (x: xpr_t):xpr_t =
     let rec expand x =
       match x with
       | XVar v