Assembly Interoperation

This section describes the mechanisms that BRiCk uses to connect C++ concepts to the underlying generated machine code. These connections are generally necessary in low-level code that inter-operates with assembly. For example, accessing C++ memory from assembly, calling C++ functions from assembly, changing the address space that the C++ program is running in, etc.

While crucial for low-level programs these features are generally not used in high-level programs. Even for low-level programs, a relatively small amount of the program requires properties at this level.

Compiler Correctness

BRiCk’s strategy for connecting C++ programs to machine programs is to connect the weakest pre-condition of C++ functions to a weakest pre-condition for machine code. The relevant definitions can be found in bedrock.lang.cpp.compile.

  (** compilation of a function [f] is correct if the weakest pre-condition
      of the function ([wp_func]) implies the weakest pre-condition of the
      compiled code ([wp_fptr]).
   *)
  Axiom code_at_ok : forall (f : Func) p,
      code_at tu f p
      |-- Forall ls Q, wp_func tu f ls Q -*
                       wp_fptr (Σ:=Σ) tu.(types) (type_of_value (Ofunction f)) p ls Q.

  Axiom method_at_ok : forall (m : Method) p,
      method_at tu m p
      |-- Forall ls Q, wp_method tu m ls Q -*
                       wp_fptr (Σ:=Σ) tu.(types) (type_of_value (Omethod m)) p ls Q.

  Axiom ctor_at_ok : forall (c : Ctor) p,
      ctor_at tu c p
      |-- Forall ls Q, wp_ctor tu c ls Q -*
                       wp_fptr tu.(types) (type_of_value (Oconstructor c)) p ls Q.

  Axiom dtor_at_ok : forall (d : Dtor) p,
      dtor_at tu d p
      |-- Forall ls Q, wp_dtor tu d ls Q -*
                       wp_fptr tu.(types) (type_of_value (Odestructor d)) p ls Q.

This approach effectively casts C++ as a stylized way to write machine code; however, it is more than simply macros. When C++ code is running, the C++ abstract machines owns the underlying memory and can use that ownership to assert invariants over the memory (e.g. that code is not written, const objects do not change, etc). This characterization makes it possible (and even natural) to escape the abstract machine in limited circumstances and interact at a lower-level of abstraction. For example, a viable model of inline assembly is to borrow resources from the abstract machine, run the assembly, and then return the underlying resources back to the abstract machine. The Object representation, layout and padding section goes into more details regarding how this access to memory is coordinated within BRiCk.