CHB:ARM: record presence of instruction predicates in analysis results

Author: sipma

CodeHawk/CHB/bchlib/bCHVersion.ml

@@ -95,8 +95,8 @@ end
 
 
 let version = new version_info_t 
-  ~version:"0.6.0_20250623"
-  ~date:"2025-06-23"
+  ~version:"0.6.0_20250625"
+  ~date:"2025-06-25"
   ~licensee: None
   ~maxfilesize: None
   ()

CodeHawk/CHB/bchlibarm32/bCHARMAnalysisResults.ml

@@ -72,12 +72,32 @@ object (self)
     let loc = ctxt_string_to_location faddr ctxtiaddr in
     let floc = get_floc loc in
     let espoffset = floc#get_stackpointer_offset "arm" in
+    let has_control_flow =
+      instr#has_opcode_condition
+      && (match instr#get_opcode with
+          | Branch _ | BranchExchange _ -> false
+          | _ -> true)
+      && (Option.is_none instr#is_in_aggregate) in
     begin
       arm_dictionary#write_xml_arm_opcode node instr#get_opcode;
       id#write_xml_instr node instr floc;
       id#write_xml_sp_offset node espoffset;
       arm_dictionary#write_xml_arm_bytestring
-        node (byte_string_to_printed_string instr#get_instruction_bytes)
+        node (byte_string_to_printed_string instr#get_instruction_bytes);
+      (if has_control_flow then
+         let optcc = instr#get_opcode_condition in
+         match optcc with
+         | Some cc ->
+            let pcc = BCHARMOpcodeRecords.get_cond_mnemonic_extension cc in
+            let _ = node#setAttribute "brcc" pcc in
+            if floc#has_test_expr then
+              let csetter = floc#f#get_associated_cc_setter floc#cia in
+              node#setAttribute "brsetter" csetter
+            else
+              ()
+         | _ -> ()
+       else
+         ())
     end
 
   method private write_xml_instructions (node:xml_element_int) =

CodeHawk/CHB/bchlibarm32/bCHARMAssemblyInstruction.ml

@@ -4,7 +4,7 @@
    ------------------------------------------------------------------------------
    The MIT License (MIT)
 
-   Copyright (c) 2021-2024  Aarno Labs, LLC
+   Copyright (c) 2021-2025  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
@@ -87,8 +87,16 @@ object (self)
 
   method is_in_aggregate = in_aggregate
 
+  method has_opcode_condition =
+    BCHARMOpcodeRecords.is_opcode_conditional opcode
+
+  method get_opcode_condition =
+    BCHARMOpcodeRecords.get_arm_opcode_condition opcode
+
+  (* applies only to Thumb IT instruction *)
   method set_block_condition = blockcondition <- true
 
+  (* applies only to Thumb IT instruction *)
   method is_block_condition = blockcondition
 
   method set_condition_covered_by (iaddr: doubleword_int) =

CodeHawk/CHB/bchlibarm32/bCHARMOpcodeRecords.ml

@@ -198,7 +198,7 @@ let get_record (opc:arm_opcode_t): 'a opcode_record_t =
       operands = [ rd; rn; imm ];
       flags_set = if s then [APSR_N; APSR_Z; APSR_C] else [];
       ccode = Some c;
-      ida_asm = (fun f -> f#opscc ~thumbw:tw "AND" c [rd; rn; imm])
+      ida_asm = (fun f -> f#opscc ~thumbw:tw "AND" ~writeback:s c [rd; rn; imm])
     }
   | BitwiseBitClear (s, c, rd, rn, rm, tw) -> {
       mnemonic = "BIC";

CodeHawk/CHB/bchlibarm32/bCHARMTypes.mli

@@ -1423,6 +1423,7 @@ class type arm_assembly_instruction_int =
     method get_instruction_bytes: string
     method get_bytes_ashexstring: string
     method get_non_code_block: not_code_t
+    method get_opcode_condition: arm_opcode_cc_t option
     method condition_covered_by: doubleword_int
 
     (* predicates *)
@@ -1438,6 +1439,7 @@ class type arm_assembly_instruction_int =
     method is_aggregate_entry: bool
     method is_aggregate_exit: bool
     method is_aggregate_anchor: bool
+    method has_opcode_condition: bool
 
     (* i/o *)
     method write_xml: xml_element_int -> unit

CodeHawk/CHB/bchlibarm32/bCHFnARMTypeConstraints.ml

@@ -393,6 +393,23 @@ object (self)
 
        end
 
+    | BitwiseNot (_, _, rd, rm, _) ->
+       let rdreg = rd#to_register in
+       let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in
+       let rmdefs = get_variable_rdefs_r (rm#to_variable floc) in
+       let rmreg = rm#to_register in
+       begin
+         List.iter (fun rmsym ->
+             let rmaddr = rmsym#getBaseName in
+             let rmtypevar = mk_reglhs_typevar rmreg faddr rmaddr in
+             let rmtypeterm = mk_vty_term rmtypevar in
+             let lhstypeterm = mk_vty_term lhstypevar in
+             begin
+               log_subtype_constraint __LINE__ "MVN-rdef" rmtypeterm lhstypeterm;
+               store#add_subtype_constraint rmtypeterm lhstypeterm
+             end) rmdefs
+       end
+
     | BitwiseOr (_, _, rd, rn, _, _) ->
        let rdreg = rd#to_register in
        let lhstypevar = mk_reglhs_typevar rdreg faddr iaddr in