CBMC: /home/runner/work/cbmc/cbmc/src/cprover/equality_propagation.cpp Source File

17 void equality_propagation(std::vector<exprt> &constraints)

18{

19 using valuest = std::map<irep_idt, exprt>;

20 valuest values;

21

22 std::vector<exprt> new_constraints;

23 new_constraints.reserve(constraints.size());

24

25 // forward-propagation of equalities

26 for(auto &expr : constraints)

27 {

28 bool retain_constraint = true;

29

30 // apply the map

31 auto substitution_result = substitute_symbols(values, expr);

32 if(substitution_result.has_value())

33 expr = std::move(substitution_result.value());

34

35 if(expr.id() == ID_equal)

36 {

37 const auto &equal_expr = to_equal_expr(expr);

38 if(equal_expr.lhs().id() == ID_symbol)

39 {

40 const auto &symbol_expr = to_symbol_expr(equal_expr.lhs());

41 // this is a (deliberate) no-op when the symbol is already in the map

42 auto insert_result =

43 values.insert({symbol_expr.identifier(), equal_expr.rhs()});

44 if(insert_result.second)

45 {

46 // insertion has happened

47 retain_constraint = false;

48 }

49 }

50 }

51

52 if(retain_constraint)

53 new_constraints.push_back(std::move(expr));

54 }

55

56 constraints = std::move(new_constraints);

57

58 // apply the map again, to catch any backwards definitions

59 for(auto &expr : constraints)

60 {

61 if(expr.id() == ID_equal && to_equal_expr(expr).lhs().id() == ID_symbol)

62 {

63 // it's a definition

64 }

65 else

66 {

67 // apply the map

68 auto substitution_result = substitute_symbols(values, expr);

69 if(substitution_result.has_value())

70 expr = std::move(substitution_result.value());

71 }

72 }

73}

ait

ait supplies three of the four components needed: an abstract interpreter (in this case handling func...

Definition ai.h:566

equality_propagation

void equality_propagation(std::vector< exprt > &constraints)

Definition equality_propagation.cpp:17

equality_propagation.h

Equality Propagation.

std_expr.h

API to expression classes.

to_symbol_expr

const symbol_exprt & to_symbol_expr(const exprt &expr)

Cast an exprt to a symbol_exprt.

Definition std_expr.h:221

to_equal_expr

const equal_exprt & to_equal_expr(const exprt &expr)

Cast an exprt to an equal_exprt.

Definition std_expr.h:1375

substitute_symbols

std::optional< exprt > substitute_symbols(const std::map< irep_idt, exprt > &substitutions, exprt src)

Substitute free occurrences of the variables given by their identifiers in the keys of the map in the...

Definition substitute_symbols.cpp:111

substitute_symbols.h

Symbol Substitution.