Planes Without Heaps

I ran across something interesting while reading up on abstract interpretation. I was prompted by a redditor comment that the approach in "Symbolic Disassembly" was an abstract interpretation technique. Patrick Cousot's team has a static analyzer for C code that they've applied to software in the Airbus A340 and A380:

The development of ASTRÉE started from scratch in Nov. 2001. Two years later, the main applications have been the static analysis of synchronous, time-triggered, real-time, safety critical, embedded software written or automatically generated in the C programming language. ASTRÉE has achieved the following two unprecedented results:

• A340-300 In Nov. 2003, ASTRÉE was able to prove completely automatically the absence of any RTE in the primary flight control software of the Airbus A340 fly-by-wire system, a program of 132,000 lines of C analyzed in 1h20 on a 2.8 GHz 32-bit PC using 300 Mb of memory (and 50mn on a 64-bit AMD Athlon™ 64 using 580 Mb of memory).


• A380 From Jan. 2004 on, ASTRÉE was extended to analyze the electric flight control codes then in development and test for the A380 series. The operational application by Airbus France at the end of 2004 was just in time before the A380 maiden flight on Wednesday, 27 April, 2005.

The analyzer has its limits, so by extension does the tested code: "ASTRÉE analyzes structured C programs, with complex memory usages, but without dynamic memory allocation and recursion." Of course we don't know from this whether there is other code run in the Airbus 340 or 380 that does use dynamic memory allocation, but presumably the 132,000 lines of C are an important and interesting part of the system. So, it's a largish useful program that doesn't use the heap.

Do you remember the last time you wrote a program with no dynamic memory allocation (in a language that doesn't do it as a matter of course)?

Symbolic Disassembly

In looking at OCaml-generated x86 assembly last week, I noticed that having a language which keeps undefined identifiers in symbolic form can be handy. I started making notes in a Mathematica notebook to keep track of some heap shuffling code I was trying to understand. To explain the technique, let's use this OCaml snippet:

((1.0 -. alpha) *. (Array.get y i))

where the floating-point arithmetic becomes this x86 code:

fld1
fsub REAL8 PTR [eax]
fmul REAL8 PTR [esi]

In Mathematica, I translated lines of assembly into real assignments, using the literal register names for my variable names, except at the very beginning of the assembly fragement. For example, when starting the above fragment, eax points to the alpha value, so I would write the read reference to eax as alpha, without defining alpha. Similarly esi points to Array.get y i, so I was able to write this sequence:


It was interesting, a little startling actually, to see the original expression re-emerge by simulating running the code. I didn't get very far into it, but you can also do things like simulate writes to memory with a register transfer definition:

Mem[eax] = 2301

In a traditional language, eax has to be bound to a value. But in a symbolic language, eax can be a symbolic expression like _caml_young_ptr + 4.

Do my partial-evaluation readers have any remarks about this?