@@ -699,17 +699,23 @@ object (self)
699699 let memoffset = numoffset#add offset in
700700 let memref_r = self#env#mk_base_sym_reference base in
701701 let memoff_r =
702+ address_memory_offset
703+ t_unknown ~tgtsize: (Some size) (num_constant_expr memoffset) in
704+ (*
705+ To keep representation unifor (i.e., to avoid aliasing) the creation
706+ of variable representation against the type of the variable must be
707+ delayed until reporting time.
702708 TR.tbind
703709 ~msg:(__FILE__ ^ ":" ^ (string_of_int __LINE__))
704710 (fun basevar ->
705711 let optbasetype = self#env#get_variable_type basevar in
706- let basetype =
712+ let basetype = t_unknown in
707713 match optbasetype with
708714 | Some t when is_pointer t -> ptr_deref t
709715 | _ -> t_unknown in
710- address_memory_offset basetype
716+ address_memory_offset t_unknown
711717 ~tgtsize:(Some size) (num_constant_expr memoffset))
712- (self#env#get_variable base#getSeqNumber) in
718+ (self#env#get_variable base#getSeqNumber) in *)
713719 mk_memvar memref_r memoff_r
714720
715721 else
@@ -1527,9 +1533,16 @@ object (self)
15271533 ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__))
15281534 (fun v -> XVar v) (self#convert_variable_offsets ~size v)
15291535 | XOp ((Xf "addressofvar" ), [XVar v ]) ->
1536+ let newx_r =
1537+ TR. tmap
1538+ ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__))
1539+ (fun v -> XVar v) (self#convert_variable_offsets ~size v) in
15301540 TR. tmap
1531- ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__))
1532- (fun v -> XVar v) (self#convert_variable_offsets ~size v)
1541+ (fun newx ->
1542+ match newx with
1543+ | XVar v -> XOp ((Xf " addressofvar" ), [(XVar v)])
1544+ | _ -> exp)
1545+ newx_r
15331546 | XOp (op , [xx ]) -> TR. tmap (fun x -> XOp (op, [x])) (aux xx)
15341547 | XOp (op , [x1 ; x2 ]) ->
15351548 TR. tmap2 (fun x1 x2 -> XOp (op, [x1; x2])) (aux x1) (aux x2)
@@ -1550,12 +1563,15 @@ object (self)
15501563 let knownpointers = List. filter self#f#is_base_pointer vars in
15511564 match knownpointers with
15521565 (* one known pointer, must be the base *)
1553- | [base] when self#f#env#is_initial_stackpointer_value base ->
1566+ | [base] (* when self#f#env#is_initial_stackpointer_value base *) ->
15541567 let offset = simplify_xpr (XOp (XMinus , [x; XVar base])) in
15551568 let memref_r = self#env#mk_base_variable_reference base in
15561569 let memoff_r = address_memory_offset t_unknown offset in
15571570 (memref_r, memoff_r)
15581571
1572+ (* resolving to type-based representations at this point may give
1573+ rise to aliasing; for example __ptr_deref_R[0]_in.field_4 may be aliased
1574+ with R[0]_in[4]_in
15591575 | [base] ->
15601576 let offset = simplify_xpr (XOp (XMinus, [x; XVar base])) in
15611577 let memref_r = self#env#mk_base_variable_reference base in
@@ -1582,6 +1598,7 @@ object (self)
15821598 ^ "base pointer: " ^ (x2s (XVar base)))
15831599 (fun basetype -> address_memory_offset basetype offset)
15841600 basetype_r in
1601+ *)
15851602
15861603 (*
15871604 (match offset with
@@ -1593,7 +1610,7 @@ object (self)
15931610 ^ "Offset from base "
15941611 ^ (x2s (XVar base))
15951612 ^ " not recognized: " ^ (x2s offset)]) in *)
1596- (memref_r, memoff_r)
1613+ (* (memref_r, memoff_r) * )
15971614
15981615 (* no known pointers, have to find a base *)
15991616 | [] ->
0 commit comments