@@ -686,8 +686,8 @@ object (self)
686686 match address with
687687 | XConst (IntConst n ) ->
688688 log_tfold_default
689- (mk_tracelog_spec
690- ~tag: " get_memory_variable_1"
689+ (log_error
690+ " get_memory_variable_1"
691691 (self#cia ^ " : constant: " ^ n#toString))
692692 (fun base ->
693693 if system_info#get_image_base#le base then
@@ -697,9 +697,24 @@ object (self)
697697 (default () )
698698 (numerical_to_doubleword n)
699699 | XVar v when self#f#env#is_memory_address_variable v ->
700- self#f#env#mk_memory_address_deref_variable v
700+ log_tfold_default
701+ (log_error
702+ " get_memory_variable_1"
703+ (self#cia ^ " : memory address variable: " ^ (p2s var#toPretty)))
704+ (fun v -> v)
705+ (default () )
706+ (self#env#mk_memory_address_deref_variable v)
707+ | XOp (XPlus , [XVar v; XConst (IntConst n)])
708+ when self#f#env#is_memory_address_variable v ->
709+ log_tfold_default
710+ (log_error
711+ " get_memory_variable_1"
712+ (self#cia ^ " : memory address variable: " ^ (p2s var#toPretty)))
713+ (fun v -> v)
714+ (default () )
715+ (self#env#mk_memory_address_deref_variable ~offset: n#toInt v)
701716 | _ ->
702- let (memref, memoffset) = self#decompose_address address in
717+ let (memref, memoffset) = self#decompose_address address in
703718 if is_constant_offset memoffset then
704719 let memvar =
705720 if memref#is_global_reference then
@@ -1069,7 +1084,7 @@ object (self)
10691084
10701085 method get_fts_parameter_expr (_p : fts_parameter_t ) = None
10711086
1072- method decompose_array_address
1087+ method decompose_memvar_address
10731088 (x : xpr_t ): (memory_reference_int * memory_offset_t) option =
10741089 let _ = chlog#add " decompose_array_address" (LBLOCK [STR " xpr: " ; x2p x]) in
10751090 let vars = vars_as_positive_terms x in
@@ -1078,15 +1093,15 @@ object (self)
10781093 match memaddrs with
10791094 | [base] ->
10801095 let (_, _, _, optty) =
1081- self#f#env#varmgr#get_memory_address_meminfo base in
1096+ TR. tget_ok ( self#f#env#varmgr#get_memory_address_meminfo base) in
10821097 let offset = simplify_xpr (XOp (XMinus , [x; XVar base])) in
10831098 Some (XVar base, offset, optty)
10841099 | _ ->
10851100 None in
10861101 match optbase with
10871102 | None -> None
10881103 | Some (_ , _ , None) -> None
1089- | Some (XVar base , xoffset , Some ty ) ->
1104+ | Some (XVar base , xoffset , Some ty ) when is_array_type ty ->
10901105 let _ =
10911106 chlog#add
10921107 " decompose_array_address" (LBLOCK [STR " xoffset: " ; x2p xoffset]) in
@@ -1112,6 +1127,25 @@ object (self)
11121127 (match (optmemref, memoffset) with
11131128 | (_ , UnknownOffset) -> None
11141129 | (Some memref , memoffset ) -> Some (memref, memoffset)
1130+ | _ ->
1131+ None )
1132+ | Some (XVar base , xoffset , Some ty ) when is_struct_type ty ->
1133+ let _ =
1134+ chlog#add
1135+ " decompose_struct_address" (LBLOCK [STR " xoffset: " ; x2p xoffset]) in
1136+ let optmemref = TR. to_option (self#env#mk_base_variable_reference base) in
1137+ let cinfo = get_struct_type_compinfo ty in
1138+ (match xoffset with
1139+ | XConst (IntConst n ) ->
1140+ let optfinfo = get_struct_field_at_offset cinfo n#toInt in
1141+ (match optfinfo with
1142+ | None -> None
1143+ | Some (finfo , rem ) when rem = 0 ->
1144+ let memoffset = FieldOffset ((finfo.bfname, cinfo.bckey), NoOffset ) in
1145+ (match optmemref with
1146+ | Some memref -> Some (memref, memoffset)
1147+ | _ -> None )
1148+ | _ -> None )
11151149 | _ -> None )
11161150 | _ -> None
11171151
0 commit comments