pietrobraione

From Coq Require Import Strings.String.
From Coq Require Import Init.Nat.
From Coq Require Import Bool.Bool.
From Coq Require Import Arith.Arith.
From Coq Require Import Lists.List.
From Coq Require Import Program.Wf.
From Hammer Require Import Tactics.

(* A simplified version of a symbolic interpreter for an o-o language.
   Expressions are evaluated against heaps. Values can be either 

pietrobraione

/* This gist shows how to build an almost zero-assembly template jit compiler from a
 * threaded interpreter.
 * See http://eli.thegreenplace.net/2012/07/12/computed-goto-for-efficient-dispatch-tables
 * for the original threaded code interpreter. To illustrate compilation of jumps I added 
 * a couple of jump bytecodes, and to illustrate compilation of primitives (with external
 * function invocations) I added a print bytecode.
 * Profiling is extremely rough: When a backjump is executed 1000 times the code between
 * the jump bytecode and the target of the jump is jitted, and nothing else.
 * Works with clang and gcc under macOS Sonoma (Apple silicon) and Ubuntu 22.04 (x86-64),
 * tried on the following versions: