overall shape of main loop

- there are many holes
- translatejimple/classverification now returns Core.ast_procedure,
  then the main loop (in Jstar) instruments them with topl stuff,
  and then the symbolic execution is called (from Jstar rather than
  Translatejimple)
Merge remote-tracking branch 'origin/alt-abd' into alt-abd