max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(library/vm/vm): serialization/deserialization of builtin cases_on instruction

Browse source 
We generate internal ids for builtin cases_on recursors.
These ids were being saved in the .olean files.
This was fine before commit 41e8a1712e because we had a separate
mapping for builtin cases_on recursors. Now, all ids are stored in the
same mapping. Thus, minor changes in the set of VM builtin operations
make lean crash when importing .olean files because they will change the
internal id for the builtin cases_on.
The problem can be reproduced in the following way:

0- Go to build/release

1- make clean-olean

2- make
Everything is fine after step 2

3- Comment the following line at tactic_state.cpp

    DECLARE_VM_BUILTIN(name({"tactic", "open_namespaces"}),      tactic_open_namespaces);

4- make

5- Lean will crash when executing the following command

   ../../bin/lean ../../library/init/meta/tactic.lean

I believe this bug is reponsible by the crash that @jroesch reported on Slack.

This commit fixes the problem by storing the name of the builtin
cases_on recursor in the .olean file.
This commit is contained in:
Leonardo de Moura 2016-12-22 18:35:30 -08:00
parent e5c4231248
commit 144d9096e2
1 changed files with 2 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/library/vm/vm.cpp
View file

@ -686,7 +686,7 @@ void vm_instr::serialize(serializer & s, std::function<name(unsigned)> const & i
s << m_pc[1];
break;
case opcode::BuiltinCases:
s << m_cases_idx;
s << idx2name(m_cases_idx);
// continue on CasesN
case opcode::CasesN:
s << m_npcs[0];
@ -759,7 +759,7 @@ static vm_instr read_vm_instr(deserializer & d) {
return mk_casesn_instr(pcs.size(), pcs.data());
}
case opcode::BuiltinCases: {
idx = d.read_unsigned();
idx = get_vm_index(read_name(d));
buffer<unsigned> pcs;
read_cases_pcs(d, pcs);
return mk_builtin_cases_instr(idx, pcs.size(), pcs.data());