CHB:ARM: add documentation for conditional expressions

Author: sipma

CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.ml

@@ -433,7 +433,11 @@ let arm_conditional_expr
        else
 	 begin
            (if collect_diagnostics () then
-              ch_diagnostics_log#add "condition" (x2p expr));
+              ch_diagnostics_log#add
+                "condition"
+                (LBLOCK [condloc#toPretty; STR ": "; (x2p expr); STR ". ";
+                         pretty_print_list frozenVars#listOfValues
+                           (fun v -> v#toPretty) "[" ", " "]" ]));
 	   condfloc#set_test_expr expr;
 	   testfloc#set_test_variables frozenVars#listOfPairs;
 	   (frozenVars#listOfValues, (Some expr), opsused)
@@ -504,7 +508,8 @@ let arm_conditional_conditional_expr
                 STR "; cond3: ";
                 x2p cond3]) in
 
-     let xpr = XOp (XLOr, [XOp (XLAnd, [XOp (XLNot, [cond1]); cond3]); cond2]) in
+     let xpr = XOp (XLOr, [XOp (XLAnd, [XOp (XLNot, [cond1]); cond3]);
+                           XOp (XLAnd, [cond1; cond2])]) in
      begin
        (if collect_diagnostics () then
           ch_diagnostics_log#add "condition" (x2p xpr));

CodeHawk/CHB/bchlibarm32/bCHARMConditionalExpr.mli

@@ -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
@@ -37,6 +37,21 @@ open BCHLibTypes
 (* bchlibarm32 *)
 open BCHARMTypes
 
+
+(** Returns the predicate condition and associated info for a condidional,
+    in particular it returns a tuple consisting of:
+    - a list of temporary variables created to preserve the (frozen) values at
+      the test location (testloc) for the location of the conditional (condloc)
+    - the predicate that expresses the joint condition of test and condition
+      code (cc, e.g., EQ), and
+    - a list of the operands used in the creation of the predicate.
+
+    The arguments to the function are:
+    - [condopc]: the opcode of the conditional instruction (e.g., Branch)
+    - [testopc]: the opcode of the test instruction (e.g., Compare)
+    - [condloc]: the location of conditional instruction
+    - [testloc]: the location of the test instruction.
+ *)
 val arm_conditional_expr:
   condopc: arm_opcode_t
   -> testopc:arm_opcode_t
@@ -45,6 +60,34 @@ val arm_conditional_expr:
   -> (variable_t list * xpr_t option * arm_operand_int list)
 
 
+(** Returns the predicate condition and associated info as above for a composite
+    condtitional of the form
+{v
+    I1: <test1>            CMP    x, #0
+    I2: <test2-cc1>        CMPEQ  y, z
+    I3: <cond-cc2>         BGT
+v}
+    where the ultimate predicate condition depends is a composite of potentially
+    three test - cc combinations:
+    - if test1-cc1 is true, I2 is executed and the branch predicate is test2-cc2
+    - if test2-cc1 is false I2 is not executed and branch predicate is test2-cc1
+    leading to the composite expression
+{v
+     (test1-cc1 /\ test2-cc2) \/ ((not test1-cc1) /\ test1-cc2)
+v}
+    or, in the case of the example above:
+{v
+     (x = 0 /\ y > z) \/ (x != 0 /\ x > 0)
+or
+     (x = 0 /\ y > z) \/ (x > 0)
+v}
+    - [condopc]: the opcode of the conditional instruction (above: BGT)
+    - [testopc] the opcode of the second test instruction (above: CMPEQ)
+    - [testtestopc]: the opcode of the first test instruction (above: CMP)
+    - [condloc]: the location of [condopc]
+    - [testloc]: the location of [testopc]
+    - [testtestloc]: the location of [testtestopc]
+ *)
 val arm_conditional_conditional_expr:
   condopc: arm_opcode_t
   -> testopc: arm_opcode_t