@@ -639,13 +639,45 @@ object (self)
639639 (var : variable_t )
640640 (numoffset : numerical_t ): variable_t traceresult =
641641 let inv = self#inv in
642+ let mk_memvar memref_r memoffset_r =
643+ TR. tbind
644+ ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__))
645+ (fun memref ->
646+ if memref#is_global_reference then
647+ TR. tbind
648+ ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__)
649+ ^ " : memref:global" )
650+ (fun memoff ->
651+ TR. tbind
652+ ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__))
653+ self#env#mk_global_variable
654+ (get_total_constant_offset memoff))
655+ memoffset_r
656+ else
657+ TR. tmap
658+ ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__))
659+ (fun memoff ->
660+ (self#env#mk_offset_memory_variable memref memoff))
661+ memoffset_r)
662+ memref_r in
663+
642664 if inv#is_base_offset_constant var then
643665 let (base, offset) = inv#get_base_offset_constant var in
644666 let memoffset = numoffset#add offset in
645- TR. tmap
646- ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__))
647- (fun memref -> self#env#mk_memory_variable ~size memref memoffset)
648- (self#env#mk_base_sym_reference base)
667+ let memref_r = self#env#mk_base_sym_reference base in
668+ let memoff_r =
669+ TR. tbind
670+ ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__))
671+ (fun basevar ->
672+ let optbasetype = self#env#get_variable_type basevar in
673+ let basetype =
674+ match optbasetype with
675+ | Some t when is_pointer t -> ptr_deref t
676+ | _ -> t_unknown in
677+ address_memory_offset basetype (num_constant_expr memoffset))
678+ (self#env#get_variable base#getSeqNumber) in
679+ mk_memvar memref_r memoff_r
680+
649681 else
650682 let varx =
651683 if align > 1 then
@@ -670,27 +702,7 @@ object (self)
670702 ^ " )" ]
671703 | _ ->
672704 let (memref_r, memoffset_r) = self#decompose_memaddr address in
673- TR. tbind
674- ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__))
675- (fun memref ->
676- if memref#is_global_reference then
677- TR. tbind
678- ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__)
679- ^ " : memref:global" )
680- (fun memoff ->
681- TR. tbind
682- self#env#mk_global_variable
683- (get_total_constant_offset memoff))
684- memoffset_r
685- else
686- TR. tbind
687- ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__))
688- (fun memoff ->
689- TR. tmap
690- (self#env#mk_memory_variable memref)
691- (get_total_constant_offset memoff))
692- memoffset_r)
693- memref_r
705+ mk_memvar memref_r memoffset_r
694706
695707 method get_memory_variable_1
696708 ?(align =1 ) (* alignment of var value *)
@@ -753,6 +765,7 @@ object (self)
753765 (fun v -> v)
754766 (default () )
755767 (TR. tbind
768+ ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__))
756769 self#env#mk_global_variable
757770 (get_total_constant_offset memoffset))
758771 else
@@ -797,6 +810,7 @@ object (self)
797810 ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__))
798811 (fun memoff ->
799812 TR. tmap
813+ ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__))
800814 (self#env#mk_memory_variable memref)
801815 (get_total_constant_offset memoff))
802816 memoff_r)
@@ -849,6 +863,7 @@ object (self)
849863 ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__) ^ " : memref:global" )
850864 (fun memoff ->
851865 TR. tbind
866+ ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__))
852867 (self#env#mk_global_variable ~size )
853868 (get_total_constant_offset memoff))
854869 memoff_r
@@ -857,6 +872,7 @@ object (self)
857872 ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__))
858873 (fun memoff ->
859874 TR. tmap
875+ ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__))
860876 (self#env#mk_memory_variable memref)
861877 (get_total_constant_offset memoff))
862878 memoff_r)
@@ -893,6 +909,7 @@ object (self)
893909 (fun v -> v)
894910 (default () )
895911 (TR. tbind
912+ ~msg: (__FILE__ ^ " :" ^ (string_of_int __LINE__))
896913 self#env#mk_global_variable
897914 (get_total_constant_offset memoffset))
898915 else
@@ -1254,7 +1271,10 @@ object (self)
12541271 | [base] ->
12551272 let offset = simplify_xpr (XOp (XMinus , [x; XVar base])) in
12561273 let memref_r = self#env#mk_base_variable_reference base in
1257- let memoff_r =
1274+ let vartype = self#f#env#get_variable_type base in
1275+ let vartype = match vartype with None -> t_unknown | Some t -> t in
1276+ let memoff_r = address_memory_offset vartype offset in
1277+ (*
12581278 (match offset with
12591279 | XConst (IntConst n) -> Ok (ConstantOffset (n, NoOffset))
12601280 | XOp (XMult, [XConst (IntConst n); XVar v]) ->
@@ -1263,7 +1283,7 @@ object (self)
12631283 Error [__FILE__ ^ ":" ^ (string_of_int __LINE__) ^ ": "
12641284 ^ "Offset from base "
12651285 ^ (x2s (XVar base))
1266- ^ " not recognized: " ^ (x2s offset)]) in
1286+ ^ " not recognized: " ^ (x2s offset)]) in *)
12671287 (memref_r, memoff_r)
12681288
12691289 (* no known pointers, have to find a base *)
@@ -1681,7 +1701,31 @@ object (self)
16811701 let reqN () = self#env#mk_num_temp in
16821702 let reqC = self#env#request_num_constant in
16831703 let (rhscmds, rhs_c) = xpr_to_numexpr reqN reqC rhs in
1684- rhscmds @ [ASSIGN_NUM (lhs, rhs_c)]
1704+ let cmds = rhscmds @ [ASSIGN_NUM (lhs, rhs_c)] in
1705+ let fndata = self#f#get_function_data in
1706+ match fndata#get_regvar_intro self#ia with
1707+ | Some rvi when rvi.rvi_cast && Option. is_some rvi.rvi_vartype ->
1708+ TR. tfold
1709+ ~ok: (fun reg ->
1710+ let ty = Option. get rvi.rvi_vartype in
1711+ let tcvar =
1712+ self#f#env#mk_typecast_value self#cia rvi.rvi_name ty reg in
1713+ begin
1714+ log_result __FILE__ __LINE__
1715+ [" Create typecast var for "
1716+ ^ (register_to_string reg)
1717+ ^ " at "
1718+ ^ self#cia];
1719+ cmds @ [ASSIGN_NUM (lhs, NUM_VAR tcvar)]
1720+ end )
1721+ ~error: (fun e ->
1722+ begin
1723+ log_error_result __FILE__ __LINE__
1724+ (" expected a register variable" :: e);
1725+ cmds
1726+ end )
1727+ (self#f#env#get_register lhs)
1728+ | _ -> cmds
16851729
16861730 (* Note: recording of loads and stores is performed by the different
16871731 architectures directly in FnXXXDictionary.*)
0 commit comments