@@ -244,9 +244,6 @@ def complete_instruction_connections(self) -> None:
244244 self .astinterface .add_instr_mapping (hl_instr , ll_instr )
245245
246246 def set_invariants (self ) -> None :
247- pass
248-
249- '''
250247 invariants = self .function .invariants
251248 aexprs : Dict [str , Dict [str , Tuple [int , int , str ]]] = {}
252249 for loc in sorted (invariants ):
@@ -263,47 +260,72 @@ def set_invariants(self) -> None:
263260 # Exclude auxiliary analysis variables
264261 continue
265262
266- var = XU.xvariable_to_ast_lvals(
263+ if fact .variable .is_constant_value_variable :
264+ # Exclude invariants that equate symbolic constants
265+ # with constant values
266+ continue
267+
268+ var = XU .xvariable_to_ast_lval (
267269 fact .variable ,
268270 instr .xdata ,
271+ instr .iaddr ,
269272 self .astinterface ,
270- anonymous=True)[0]
273+ anonymous = True )
274+
271275 varindex = var .index (self .astinterface .serializer )
272276 value = fact .value
273277 if value .is_singleton_value :
274278 aexpr : ASTExpr = self .astinterface .mk_integer_constant (
275279 value .singleton_value )
276280 aexprindex = aexpr .index (self .astinterface .serializer )
281+
277282 elif value .is_symbolic_expression :
278- aexpr = XU.xxpr_to_ast_exprs (
283+ aexpr = XU .xxpr_to_ast_def_expr (
279284 fact .value .expr ,
280285 instr .xdata ,
281286 instr .iaddr ,
282287 self .astinterface ,
283- anonymous=True)[0]
288+ anonymous = True )
284289 aexprindex = aexpr .index (self .astinterface .serializer )
285290 else :
286291 continue
287292 aexprs .setdefault (loc , {})
288293 aexprs [loc ][str (var )] = (varindex , aexprindex , str (aexpr ))
294+
289295 if fact .is_initial_var_equality :
290296 fact = cast ("InitialVarEqualityFact" , fact )
291- var = XU.xvariable_to_ast_lvals(
297+
298+ if fact .variable .is_constant_value_variable :
299+ continue
300+
301+ if fact .variable .is_global_variable :
302+ continue
303+
304+ # Filter out initial-value equalities on return values
305+ if "rtn_" in str (fact .variable ):
306+ continue
307+
308+ var = XU .xvariable_to_ast_lval (
292309 fact .variable ,
293310 instr .xdata ,
311+ instr .iaddr ,
294312 self .astinterface ,
295- anonymous=True)[0]
313+ anonymous = True )
314+
296315 varindex = var .index (self .astinterface .serializer )
297- aelval = XU.xvariable_to_ast_lvals (
316+ aexpr = XU .xvariable_to_ast_def_lval_expression (
298317 fact .initial_value ,
299318 instr .xdata ,
300- self.astinterface)[0]
301- aexpr = self.astinterface.mk_lval_expr(aelval)
319+ instr .iaddr ,
320+ self .astinterface )
321+
302322 aexprindex = aexpr .index (self .astinterface .serializer )
303323 aexprs .setdefault (loc , {})
304324 aexprs [loc ][str (var )] = (varindex , aexprindex , str (aexpr ))
325+
326+ num_aexprs = sum (len (aexprs [a ]) for a in aexprs )
327+ chklogger .logger .info ("Set %d available expressions" , num_aexprs )
305328 self .astinterface .set_available_expressions (aexprs )
306- '''
307329
308330 def set_return_sequences (self ) -> None :
309331 """Currently only supports Thumb-2 stack-adjustment, pop return sequence."""
0 commit comments