Perform a loop transformation that eliminate back-edges in a loop and flatten the function CFG into a directed acyclic graph (DAG). The general procedure works as following (assuming the loop invariant expression is L): - At the beginning of the loop header (identified by the label bytecode), insert the following statements: - assert L; - havoc T; - assume L; - Create a new dummy block (say, blo
(
func_env: &FunctionEnv<'_>,
data: FunctionData,
loop_annotation: &LoopAnnotation,
)
| 108 | /// - In the source block of the back edge, replace the last statement (must be a jump or |
| 109 | /// branch) with the new label of X. |
| 110 | fn transform( |
| 111 | func_env: &FunctionEnv<'_>, |
| 112 | data: FunctionData, |
| 113 | loop_annotation: &LoopAnnotation, |
| 114 | ) -> FunctionData { |
| 115 | let options = ProverOptions::get(func_env.module_env.env); |
| 116 | |
| 117 | let back_edge_locs = loop_annotation.back_edges_locations(); |
| 118 | let invariant_locs = loop_annotation.invariants_locations(); |
| 119 | let mut builder = FunctionDataBuilder::new_with_options( |
| 120 | func_env, |
| 121 | data, |
| 122 | FunctionDataBuilderOptions { |
| 123 | no_fallthrough_jump_removal: true, |
| 124 | }, |
| 125 | ); |
| 126 | let mut goto_fixes = vec![]; |
| 127 | let code = std::mem::take(&mut builder.data.code); |
| 128 | for (offset, bytecode) in code.into_iter().enumerate() { |
| 129 | match bytecode { |
| 130 | Bytecode::Label(attr_id, label) => { |
| 131 | builder.emit(bytecode); |
| 132 | builder.set_loc_from_attr(attr_id); |
| 133 | if let Some(loop_info) = loop_annotation.fat_loops.get(&label) { |
| 134 | // assert loop invariants -> this is the base case |
| 135 | for (attr_id, exp) in loop_info.invariants.values() { |
| 136 | builder.set_loc_and_vc_info( |
| 137 | builder.get_loc(*attr_id), |
| 138 | LOOP_INVARIANT_BASE_FAILED, |
| 139 | ); |
| 140 | builder.emit_with(|attr_id| { |
| 141 | Bytecode::Prop(attr_id, PropKind::Assert, exp.clone()) |
| 142 | }); |
| 143 | } |
| 144 | |
| 145 | // havoc all loop targets |
| 146 | for idx in &loop_info.val_targets { |
| 147 | builder.emit_with(|attr_id| { |
| 148 | Bytecode::Call( |
| 149 | attr_id, |
| 150 | vec![], |
| 151 | Operation::Havoc(HavocKind::Value), |
| 152 | vec![*idx], |
| 153 | None, |
| 154 | ) |
| 155 | }); |
| 156 | } |
| 157 | for (idx, havoc_all) in &loop_info.mut_targets { |
| 158 | let havoc_kind = if *havoc_all { |
| 159 | HavocKind::MutationAll |
| 160 | } else { |
| 161 | HavocKind::MutationValue |
| 162 | }; |
| 163 | builder.emit_with(|attr_id| { |
| 164 | Bytecode::Call( |
| 165 | attr_id, |
| 166 | vec![], |
| 167 | Operation::Havoc(havoc_kind), |
nothing calls this directly
no test coverage detected