Skip to content

Commit 8ed461a

Browse files
committed
CHB:ARM: result reporting for BX-call
1 parent 398a301 commit 8ed461a

File tree

1 file changed

+33
-36
lines changed

1 file changed

+33
-36
lines changed

CodeHawk/CHB/bchlibarm32/bCHFnARMDictionary.ml

Lines changed: 33 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -785,6 +785,39 @@ object (self)
785785
let (tags, args) = add_optional_instr_condition tagstring args c in
786786
(tags, args)
787787

788+
| BranchExchange (_, tgt) when instr#is_aggregate_anchor ->
789+
let iaddr = instr#get_address in
790+
let agg = (!arm_assembly_instructions)#get_aggregate iaddr in
791+
if agg#is_jumptable then
792+
let jt = agg#jumptable in
793+
let indexregop = jt#index_operand in
794+
let xrn = indexregop#to_expr floc in
795+
let xxrn = rewrite_expr xrn in
796+
let rdefs = (get_rdef xrn) :: (get_all_rdefs xxrn) in
797+
let (tagstring, args) =
798+
mk_instrx_data
799+
~xprs:[xrn; xxrn]
800+
~rdefs:rdefs
801+
() in
802+
let tags = tagstring :: ["agg-jt"] in
803+
let tags = add_subsumption_dependents agg tags in
804+
(tags, args)
805+
else if agg#is_bx_call then
806+
let (tags, args) = callinstr_key() in
807+
let xtgt = tgt#to_expr floc in
808+
let xxtgt = rewrite_expr xtgt in
809+
let rdefs = (get_rdef xtgt) :: (get_all_rdefs xxtgt) in
810+
let (tags, args) =
811+
add_bx_call_defs ~xprs:[xtgt; xxtgt] ~rdefs tags args in
812+
let tags = add_subsumption_dependents agg tags in
813+
(tags, args)
814+
else
815+
raise
816+
(BCH_failure
817+
(LBLOCK [
818+
STR "Aggregate for BranchExchange not recognized at ";
819+
iaddr#toPretty]))
820+
788821
| Branch _
789822
| BranchExchange _ when floc#has_call_target ->
790823
callinstr_key ()
@@ -858,42 +891,6 @@ object (self)
858891
let tags = add_optional_subsumption [tagstring] in
859892
(tags, args)
860893

861-
| BranchExchange (_, tgt) when instr#is_aggregate_anchor ->
862-
let iaddr = instr#get_address in
863-
let agg = (!arm_assembly_instructions)#get_aggregate iaddr in
864-
if agg#is_jumptable then
865-
let jt = agg#jumptable in
866-
let indexregop = jt#index_operand in
867-
let xrn = indexregop#to_expr floc in
868-
let xxrn = rewrite_expr xrn in
869-
let rdefs = (get_rdef xrn) :: (get_all_rdefs xxrn) in
870-
let (tagstring, args) =
871-
mk_instrx_data
872-
~xprs:[xrn; xxrn]
873-
~rdefs:rdefs
874-
() in
875-
let tags = tagstring :: ["agg-jt"] in
876-
let tags = add_subsumption_dependents agg tags in
877-
(tags, args)
878-
else if agg#is_bx_call then
879-
let (tags, args) = callinstr_key() in
880-
let xtgt = tgt#to_expr floc in
881-
let xxtgt = rewrite_expr xtgt in
882-
let rdefs = (get_rdef xtgt) :: (get_all_rdefs xxtgt) in
883-
let (tags, args) =
884-
add_bx_call_defs ~xprs:[xtgt; xxtgt] ~rdefs tags args in
885-
(* let (tagstring, args) =
886-
mk_instrx_data ~xprs:[xtgt; xxtgt] ~rdefs () in
887-
let tags = tagstring :: ["agg-bxcall"] in *)
888-
let tags = add_subsumption_dependents agg tags in
889-
(tags, args)
890-
else
891-
raise
892-
(BCH_failure
893-
(LBLOCK [
894-
STR "Aggregate for BranchExchange not recognized at ";
895-
iaddr#toPretty]))
896-
897894
| BranchExchange (c, tgt)
898895
when tgt#is_register && tgt#get_register = ARLR ->
899896
let r0_op = arm_register_op AR0 RD in

0 commit comments

Comments
 (0)