@@ -49,6 +49,8 @@ open BCHLibTypes
4949open BCHARMTypes
5050open BCHARMOpcodeRecords
5151
52+ module TR = CHTraceResult
53+
5254
5355(* Conditional execution: conditions
5456
@@ -110,56 +112,63 @@ let freeze_variables
110112 (add :variable_t -> variable_t -> unit )
111113 (testloc :location_int )
112114 (condloc :location_int )
113- (op :arm_operand_int ) =
115+ (op :arm_operand_int ): xpr_t =
114116 let testfloc = get_floc testloc in
115117 let condfloc = get_floc condloc in
116118 let env = testfloc#f#env in
117- let opXpr = op#to_expr ~unsigned testfloc in
118119 let frozenVars = new VariableCollections. table_t in
119- let vars = (variables_in_expr opXpr) in
120- let varsKnown = ref true in
121- let _ =
122- List. iter (
123- fun v ->
124- if v#isTmp then
125- varsKnown := false
126- else if env#is_function_initial_value v then
127- ()
128- else if env#is_local_variable v then
129- let _ =
130- track_location
131- testloc#ci
132- (LBLOCK [
133- v#toPretty; NL ;
134- testfloc#inv#toPretty; NL ;
135- condfloc#inv#toPretty]) in
136- if condfloc#inv#test_var_is_equal v testloc#ci condloc#ci then
137- let _ =
138- track_location
139- condloc#ci
140- (LBLOCK [
141- v#toPretty; NL ;
142- STR " test_var_is_equal" ]) in
143- ()
144- else
145- let fv = env#mk_frozen_test_value v testloc#ci condloc#ci in
146- frozenVars#set v fv
147- else if env#is_unknown_memory_variable v then
148- varsKnown := false ) vars in
149- let subst v =
150- if frozenVars#has v then
151- match testfloc#inv#get_external_exprs v with
152- | x ::_ -> x
153- | _ -> XVar (Option. get (frozenVars#get v))
154- else
155- XVar v in
156- if ! varsKnown then
157- begin
158- List. iter (fun (v , fv ) -> add v fv) frozenVars#listOfPairs ;
159- substitute_expr subst opXpr
160- end
161- else
162- random_constant_expr
120+ TR. tfold
121+ ~error: (fun e ->
122+ begin
123+ log_error_result __FILE__ __LINE__ e;
124+ random_constant_expr
125+ end )
126+ ~ok: (fun opXpr ->
127+ let vars = (variables_in_expr opXpr) in
128+ let varsKnown = ref true in
129+ let _ =
130+ List. iter (
131+ fun v ->
132+ if v#isTmp then
133+ varsKnown := false
134+ else if env#is_function_initial_value v then
135+ ()
136+ else if env#is_local_variable v then
137+ let _ =
138+ track_location
139+ testloc#ci
140+ (LBLOCK [
141+ v#toPretty; NL ;
142+ testfloc#inv#toPretty; NL ;
143+ condfloc#inv#toPretty]) in
144+ if condfloc#inv#test_var_is_equal v testloc#ci condloc#ci then
145+ let _ =
146+ track_location
147+ condloc#ci
148+ (LBLOCK [
149+ v#toPretty; NL ;
150+ STR " test_var_is_equal" ]) in
151+ ()
152+ else
153+ let fv = env#mk_frozen_test_value v testloc#ci condloc#ci in
154+ frozenVars#set v fv
155+ else if env#is_unknown_memory_variable v then
156+ varsKnown := false ) vars in
157+ let subst v =
158+ if frozenVars#has v then
159+ match testfloc#inv#get_external_exprs v with
160+ | x ::_ -> x
161+ | _ -> XVar (Option. get (frozenVars#get v))
162+ else
163+ XVar v in
164+ if ! varsKnown then
165+ begin
166+ List. iter (fun (v , fv ) -> add v fv) frozenVars#listOfPairs ;
167+ substitute_expr subst opXpr
168+ end
169+ else
170+ random_constant_expr)
171+ (op#to_expr ~unsigned testfloc)
163172
164173
165174let cc_expr
0 commit comments