Skip to content

Commit

Permalink
fix code generation bug when inline spec is involved
Browse files Browse the repository at this point in the history
  • Loading branch information
rahxephon89 committed Oct 8, 2024
1 parent 2deaf9f commit ff29628
Show file tree
Hide file tree
Showing 2 changed files with 39 additions and 1 deletion.
Original file line number Diff line number Diff line change
Expand Up @@ -887,6 +887,16 @@ impl<'a> FunctionGenerator<'a> {
/// translation. In the actual Move bytecode, a `Nop` is inserted
/// at the current code offset.
fn gen_spec_block(&mut self, ctx: &BytecodeContext, spec: &Spec) {
let used_temps = self.collect_temps_from_spec(spec);
for temp in used_temps {
let live_after = ctx.is_alive_after(temp, &[], false);
let local = self.temps.get(&temp).expect("temp has mapping").local;
if !live_after && temp >= ctx.fun_ctx.fun.get_parameter_count() {
self.emit(FF::Bytecode::MoveLoc(local));
self.emit(FF::Bytecode::Pop);
}
}

let mut replacer = |id: NodeId, target: RewriteTarget| {
if let RewriteTarget::Temporary(temp) = target {
Some(
Expand All @@ -906,6 +916,31 @@ impl<'a> FunctionGenerator<'a> {
self.emit(FF::Bytecode::Nop)
}

fn collect_temps_from_spec(&mut self, spec: &Spec) -> BTreeSet<TempIndex> {
let mut temps = BTreeSet::new();
for cond in spec.conditions.iter() {
for exp in cond.all_exps() {
exp.visit_pre_order(&mut |inner: &ExpData| {
if let ExpData::Temporary(_, temp_index) = inner {
temps.insert(*temp_index);
}
true
})
}
}
for (_, cond) in spec.update_map.iter() {
for exp in cond.all_exps() {
exp.visit_pre_order(&mut |inner: &ExpData| {
if let ExpData::Temporary(_, temp_index) = inner {
temps.insert(*temp_index);
}
true
})
}
}
temps
}

/// Emits a file-format bytecode.
fn emit(&mut self, bc: FF::Bytecode) {
self.code.push(bc)
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -851,7 +851,10 @@ impl<'env> SpecTranslator<'env> {
},
Operation::Pack(mid, sid, None) => self.translate_pack(node_id, *mid, *sid, args),
Operation::Tuple if args.len() == 1 => self.translate_exp(&args[0]),
Operation::Tuple => self.error(&loc, "Tuple not yet supported"),
Operation::Tuple => {
println!("args:{:?}", args);
self.error(&loc, "Tuple not yet supported")
},
Operation::Select(module_id, struct_id, field_id) => {
self.translate_select(node_id, *module_id, *struct_id, *field_id, args)
},
Expand Down

0 comments on commit ff29628

Please sign in to comment.