CHB:ARM: add predicate assignment instruction

Author: sipma

CodeHawk/CHB/bchlibarm32/bCHARMDisassemblyUtils.ml

@@ -139,6 +139,28 @@ let get_it_condition_list (firstcond:int) (mask:int) =
   thencc::xyz
 
 
+let get_inverse_cc (cc: arm_opcode_cc_t): arm_opcode_cc_t option =
+  match cc with
+  | ACCEqual -> Some ACCNotEqual
+  | ACCNotEqual -> Some ACCEqual
+  | ACCCarrySet -> Some ACCCarryClear
+  | ACCCarryClear -> Some ACCCarrySet
+  | ACCNegative -> Some ACCNonNegative
+  | ACCNonNegative -> Some ACCNegative
+  | ACCOverflow -> Some ACCNoOverflow
+  | ACCNoOverflow -> Some ACCOverflow
+  | ACCUnsignedHigher -> Some ACCNotUnsignedHigher
+  | ACCNotUnsignedHigher -> Some ACCUnsignedHigher
+  | ACCSignedGE -> Some ACCSignedLT
+  | ACCSignedLT -> Some ACCSignedGE
+  | ACCSignedGT -> Some ACCSignedLE
+  | ACCSignedLE -> Some ACCSignedGT
+  | _ -> None
+
+
+let has_inverse_cc (cc: arm_opcode_cc_t): bool =  Option.is_some (get_inverse_cc cc)
+
+
 let get_string_reference (floc:floc_int) (xpr:xpr_t) =
   try
     match xpr with

CodeHawk/CHB/bchlibarm32/bCHARMDisassemblyUtils.mli

@@ -39,4 +39,8 @@ val get_interrupt_flags: int -> interrupt_flags_t
 
 val get_it_condition_list: int -> int -> (string * arm_opcode_cc_t) list
 
+val get_inverse_cc: arm_opcode_cc_t -> arm_opcode_cc_t option
+
+val has_inverse_cc: arm_opcode_cc_t -> bool
+
 val get_string_reference: floc_int -> xpr_t -> string option

CodeHawk/CHB/bchlibarm32/bCHARMInstructionAggregate.ml

@@ -26,6 +26,7 @@
    ============================================================================= *)
 
 (* chlib *)
+open CHNumerical
 open CHPretty
 
 (* chutil *)
@@ -39,6 +40,7 @@ open BCHLibTypes
 (* bchlibarm32 *)
 open BCHARMAssemblyInstruction
 open BCHARMAssemblyInstructions
+open BCHARMDisassemblyUtils
 open BCHARMJumptable
 open BCHARMTypes
 open BCHDisassembleARMInstruction
@@ -61,6 +63,9 @@ let arm_aggregate_kind_to_string (k: arm_aggregate_kind_t) =
   | LDMSTMSequence s -> s#toString
   | PseudoLDRSB (i1, _, _) -> "Pseudo LDRSB at " ^ i1#get_address#to_hex_string
   | PseudoLDRSH (i1, _, _) -> "Pseudo LDRSH at " ^ i1#get_address#to_hex_string
+  | ARMPredicateAssignment (inverse, op) ->
+     let inv = if inverse then " (inverse)" else "" in
+     "predicate assignment to " ^ op#toString ^ inv
   | BXCall (_, i2) -> "BXCall at " ^ i2#get_address#to_hex_string
 
 
@@ -130,6 +135,11 @@ object (self)
     | PseudoLDRSH _ -> true
     | _ -> false
 
+  method is_predicate_assign =
+    match self#kind with
+    | ARMPredicateAssignment _ -> true
+    | _ -> false
+
   method write_xml (_node: xml_element_int) = ()
 
   method toCHIF (_faddr: doubleword_int) = []
@@ -232,6 +242,20 @@ let make_pseudo_ldrsb_aggregate
     ~anchor:asrinstr
 
 
+let make_predassign_aggregate
+      (inverse: bool)
+      (mov1: arm_assembly_instruction_int)
+      (mov2: arm_assembly_instruction_int)
+      (dstop: arm_operand_int): arm_instruction_aggregate_int =
+  let kind = ARMPredicateAssignment (inverse, dstop) in
+  make_arm_instruction_aggregate
+    ~kind
+    ~instrs:[mov1; mov2]
+    ~entry:mov1
+    ~exitinstr:mov2
+    ~anchor:mov2
+
+
 let disassemble_arm_instructions
       (ch: pushback_stream_int) (iaddr: doubleword_int) (n: int) =
   for _i = 1 to n do
@@ -393,7 +417,7 @@ let identify_pseudo_ldrsh
    ASR  Rx, Rx, #0x18
  *)
 let identify_pseudo_ldrsb
-      (ch: pushback_stream_int)
+      (_ch: pushback_stream_int)
       (instr: arm_assembly_instruction_int):
       (arm_assembly_instruction_int
        * arm_assembly_instruction_int
@@ -422,13 +446,51 @@ let identify_pseudo_ldrsb
                     when rd2#get_register = rd#get_register -> true
                | _ -> false)
          then
-           Some (TR.tget_ok ldrbinstr_r, TR.tget_ok lslinstr_r, instr)
+           Some (ldrbinstr, lslinstr, instr)
          else
            None
       | _ -> None)
   | _ -> None
 
 
+(* format of predicate assignment (in ARM): assigns the result of a test as a
+   0/1 value to a register
+
+   MOVNE  Rx, #0
+   MOVEQ  Rx, #1
+ *)
+let identify_predicate_assignment
+      (_ch: pushback_stream_int)
+      (instr: arm_assembly_instruction_int):
+      (bool
+       * arm_assembly_instruction_int
+       * arm_assembly_instruction_int
+       * arm_operand_int) option =
+  let is_zero imm = imm#to_numerical#equal numerical_zero in
+  let is_one imm = imm#to_numerical#equal numerical_one in
+  let is_zero_or_one imm = (is_zero imm) || (is_one imm) in
+  match instr#get_opcode with
+  | Move (false, c2, rd, imm2, _, _)
+       when imm2#is_immediate && (is_zero_or_one imm2) && (has_inverse_cc c2) ->
+     let rdreg = rd#get_register in
+     let addr = instr#get_address in
+     let movinstr_r = get_arm_assembly_instruction (addr#add_int (-4)) in
+     (match TR.to_option movinstr_r with
+      | Some movinstr ->
+         (match movinstr#get_opcode with
+          | Move (false, c1, rd, imm1, _, _)
+               when imm1#is_immediate
+                  && (is_zero_or_one imm1)
+                  && (rd#get_register = rdreg)
+                  && (not (imm1#to_numerical#equal imm2#to_numerical))
+                  && (has_inverse_cc c1)
+                  && ((Option.get (get_inverse_cc c1)) = c2) ->
+             let inverse = is_zero imm2 in
+             Some (inverse, movinstr, instr, rd)
+          | _ -> None)
+      | _ -> None)
+  | _ -> None
+
 
 let identify_arm_aggregate
       (ch: pushback_stream_int)
@@ -486,4 +548,12 @@ let identify_arm_aggregate
        | Some (ldrbinstr, lslinstr, asrinstr) ->
           Some (make_pseudo_ldrsb_aggregate ldrbinstr lslinstr asrinstr)
        | _ -> None in
+  let result =
+    match result with
+    | Some _ -> result
+    | _ ->
+       match identify_predicate_assignment ch instr with
+       | Some (inverse, mov1, mov2, dstop) ->
+          Some (make_predassign_aggregate inverse mov1 mov2 dstop)
+       | _ -> None in
   result

CodeHawk/CHB/bchlibarm32/bCHARMOperand.ml

@@ -44,7 +44,6 @@ open Xsimplify
 open BCHBasicTypes
 open BCHBCTypes
 open BCHBCTypeUtil
-open BCHConstantDefinitions
 open BCHCPURegisters
 open BCHDoubleword
 open BCHImmediate
@@ -64,6 +63,8 @@ module TR = CHTraceResult
 let x2p = xpr_formatter#pr_expr
 let p2s = pretty_to_string
 
+let memmap = BCHGlobalMemoryMap.global_memory_map
+
 
 let log_error (tag: string) (msg: string): tracelogspec_t =
   mk_tracelog_spec ~tag:("arm_operand:" ^ tag) msg
@@ -617,8 +618,8 @@ object (self:'a)
        let imm = if unsigned then imm#to_unsigned else imm in
        (match imm#to_doubleword with
         | Some dw ->
-           if has_symbolic_address_name dw then
-             let name = get_symbolic_address_name dw in
+           if memmap#has_location dw then
+             let name = memmap#get_location_name dw in
              let var =
                floc#f#env#mk_global_memory_address
                  ~optname:(Some name) imm#to_numerical in
@@ -637,11 +638,11 @@ object (self:'a)
     | ARMAbsolute a when elf_header#is_program_address a ->
        num_constant_expr a#to_numerical
     | ARMLiteralAddress a ->
-       if elf_header#is_program_address a then
+       if elf_header#is_readonly_address a then
          let dw = elf_header#get_program_value a in
-         if has_symbolic_address_name dw then
-           let name = get_symbolic_address_name dw in
-           let ty = get_symbolic_address_type_by_name name in
+         if memmap#has_location dw then
+           let name = memmap#get_location_name dw in
+           let ty = memmap#get_location_type dw in
            if is_struct_type ty || is_array_type ty then
              let var =
                floc#f#env#mk_global_memory_address

CodeHawk/CHB/bchlibarm32/bCHARMTypes.mli

@@ -1531,6 +1531,7 @@ type arm_aggregate_kind_t =
       arm_assembly_instruction_int
       * arm_assembly_instruction_int
       * arm_assembly_instruction_int
+  | ARMPredicateAssignment of bool * arm_operand_int
   | BXCall of arm_assembly_instruction_int * arm_assembly_instruction_int
 
 
@@ -1556,6 +1557,7 @@ class type arm_instruction_aggregate_int =
     method is_bx_call: bool
     method is_pseudo_ldrsh: bool
     method is_pseudo_ldrsb: bool
+    method is_predicate_assign: bool
 
     (* i/o *)
     method write_xml: xml_element_int -> unit

CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml

@@ -1546,6 +1546,56 @@ object (self)
          let (tags, args) = add_optional_instr_condition tagstring args c in
          (tags, args)
 
+      | Move _ when instr#is_aggregate_anchor ->
+         let finfo = floc#f in
+         let ctxtiaddr = floc#l#ci in
+         if finfo#has_associated_cc_setter ctxtiaddr then
+           let testiaddr = finfo#get_associated_cc_setter ctxtiaddr in
+           let testloc = ctxt_string_to_location faddr testiaddr in
+           let testaddr = testloc#i in
+           let testinstr =
+             fail_tvalue
+               (trerror_record
+                  (LBLOCK [
+                       STR "FnDictionary: predicate assignment"; floc#ia#toPretty]))
+               (get_arm_assembly_instruction testaddr) in
+           let agg = get_aggregate floc#ia in
+           (match agg#kind with
+            | ARMPredicateAssignment (inverse, dstop) ->
+               let (_, optpredicate, _) =
+                 arm_conditional_expr
+                   ~condopc:instr#get_opcode
+                   ~testopc:testinstr#get_opcode
+                   ~condloc:floc#l
+                   ~testloc:testloc in
+               let (tags, args) =
+                 (match optpredicate with
+                  | Some p ->
+                     let p = if inverse then XOp (XLNot, [p]) else p in
+                     let lhs = dstop#to_variable floc in
+                     let rdefs = get_all_rdefs p in
+                     let xp = rewrite_expr p in
+                     let (tagstring, args) =
+                       mk_instrx_data
+                         ~vars:[lhs]
+                         ~xprs:[p; xp]
+                         ~rdefs
+                         ~uses:[get_def_use lhs]
+                         ~useshigh:[get_def_use_high lhs]
+                         () in
+                     ([tagstring], args)
+                  | _ ->
+                     ([], [])) in
+               let dependents =
+                 List.map (fun d ->
+                     (make_i_location floc#l d#get_address)#ci) agg#instrs in
+               let tags = tags @ ["subsumes"] @ dependents in
+               (tags, args)
+            | _ ->
+               ([], []))
+         else
+           ([], [])
+
       | Move _ when (Option.is_some instr#is_in_aggregate) ->
          (match instr#is_in_aggregate with
           | Some va ->

CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml

@@ -42,7 +42,6 @@ open BCHBCFiles
 open BCHBCTypePretty
 open BCHBCTypes
 open BCHBCTypeUtil
-open BCHConstantDefinitions
 open BCHCPURegisters
 open BCHDoubleword
 open BCHFloc
@@ -228,8 +227,8 @@ object (self)
 
          (match getopt_global_address (rn#to_expr floc) with
           | Some gaddr ->
-             if is_in_global_arrayvar gaddr then
-               (match (get_arrayvar_base_offset gaddr) with
+             if BCHConstantDefinitions.is_in_global_arrayvar gaddr then
+               (match (BCHConstantDefinitions.get_arrayvar_base_offset gaddr) with
                 | Some _ ->
                    let rmdefs = get_variable_rdefs (rm#to_variable floc) in
                    let rmreg = rm#to_register in
@@ -544,8 +543,8 @@ object (self)
             assign the type of that field to the destination register. *)
          (match getopt_global_address (memop#to_address floc) with
           | Some gaddr ->
-             if is_in_global_structvar gaddr then
-               match (get_structvar_base_offset gaddr) with
+             if BCHConstantDefinitions.is_in_global_structvar gaddr then
+               match (BCHConstantDefinitions.get_structvar_base_offset gaddr) with
                | Some (_, Field ((fname, fckey), NoOffset)) ->
                   let compinfo = bcfiles#get_compinfo fckey in
                   let finfo = get_compinfo_field compinfo fname in
@@ -598,8 +597,8 @@ object (self)
             assign that array type to the destination register. *)
          (match getopt_global_address (memop#to_expr floc) with
           | Some gaddr ->
-             if is_in_global_arrayvar gaddr then
-               (match (get_arrayvar_base_offset gaddr) with
+             if BCHConstantDefinitions.is_in_global_arrayvar gaddr then
+               (match (BCHConstantDefinitions.get_arrayvar_base_offset gaddr) with
                 | Some (_, offset, bty) ->
                    (match offset with
                     | Index (Const (CInt (i64, _, _)), NoOffset) ->