GCC Jump Table Project
A retroactive analysis of verified Deos software components containing multi-way branches implemented as jump-tables.
Introduction
During recent Deos kernel structural coverage analysis, it was observed that the GCC compiler will sometimes implement a C/C++ multi-way branch statement (switch) as a jump table. This undermines our Assembly Branch Coverage (ABC) structural coverage technique's claim that ABC results in a Test Case population at least as great as Modified Condition Decision Coverage (MCDC). In short, by building a jump-table, the compiler is violating the ABC compiler restriction described in DDC-I Additional Considerations Document, DDCIDOC1b, section 3.2.2.3.5 "The Compiler Restriction", that states:
The compiler must generate at least one branch instruction for the evaluation of each condition in a Boolean expression
If any ABC compliant assembly language files, that come from Source Code destined to make up the Executable Object Code, contain jump-tables, the implications are that there could be an insufficient number of Test Cases. If discovered, an analysis needs to be retroactively added to the affected software component's certification archive showing that sufficient Test Cases do exist. Failing this, Test Cases would need to be created, or some sort of justification rendered. Here are the possible analysis implementations. Choose the one that is the most practical for the affected software component:
- Rebuild the ABC compliant (instrumented) variant with -fno-jump-tables compiler option, and re-execute the requirements based tests. Perform structural coverage analysis on the relevant object code and ensure there are sufficient tests to cover each conditional.
- Perform a manual structural coverage analysis over the jump-table present assembly code showing that there are indeed sufficient Test Cases.
- Pretend that the instrumented_optimized structural coverage analysis for the jump-table area revealed a coverage issue, and that the creation of a Test Case, or change to the Executable Object Code has been deferred. In short, perform an Executable Object Code analysis which shows that the compiler's jump-table optimization is corrected (i.e., the resulting executable object code is correct).
Note on 3: This choice may seem a strange one. The root problem is that we've discovered that our "ABC is equivalent to MCDC" claim has been rendered bogus thanks to the compiler's use of a jump-table. In many of the software components where a jump-table was discovered, the resulting code had complete structural coverage, but that's irrelevant to the issue: Did you achieve that coverage using sufficient Test Cases? For some components, especially older ones where resurrecting the structural coverage test infrastructure would be difficult, it may be more practical to assume that structural coverage of the jump-table was not achieved, and proceed accordingly.
The Compiler Assessment has been updated along with the common makefiles to prevent jump-tables in future efforts.
Candidate Software Components
The following lists all components with a certification archive entry, and that meet the following criteria:
- Distribution Server contains a latest-verified link
- Design Assurance Level is A or B
- SAS contains a DDC-I copyright
For the Deos kernel, the following additonal criteria was used:
- Only versions greater than 7.2.4.
afdx-driver 6.0.1 afdx-library 4.6.0 ansi 4.1.4 arinc653-runtime 3.1.3 arinc664-library 1.1.1 cffs-server 6.1.0 cffsi7sata 3.0.1 cffsNORFlash 3.5.0 startup-gcc 7.1.2 dart 1.2.1 ioi-api 4.0.2 ioi-ring-buffer 4.0.3 kernel 7.6.1 kernel 7.6.2 kernel 7.10.6 math 1.0.2 math-x86 2.1.0 mtl 2.2.2 emac-prl 2.0.0 pro1000enet 2.2.0 rtl81xx-prl 1.1.0 tsec-durant-prl 2.0.0 sal 2.3.2 tdl-integrity 4.0.3
These are the relevant Board Support Packages (BSP):
ccpdf-boot 1.3.0 ccpdf-pal 1.3.0 hosmer-boot 2.1.6 hosmer-pal 2.1.2 hotdish-aid-boot 3.0.0 hotdish-aid-pal 3.0.0 lutefisk-aid-boot 4.0.0 lutefisk-aid-pal 4.0.0
The remaining components listed below are assumed to only be in use by Honeywell. The current DDC-I internal conjecture is that Honeywell engineers will take the responsibility for these:
afgs-boot afgs-pal agm-pal cdsr-pal cmu cmu-mkii-plus-boot cmu-mkii-plus-pal cffs-malahci cffsECL dcp-boot dcp-pal du-pal dhm-library fcc-enet fhm-library internet-api kernel (all prior to 7.6.1) mcdu-pal nexcom-pal pdmc-pal pro100enet produce (all baselines) sccenet sfs-library (all baselines)
Impact Assessment
To determine the set of verified components that may suffer from the "jump-table" problem, the following procedure was used.
- From the relevant certification archive, retrieve each component's structural coverage report.
- Scan each component structural coverage reports' Instrumented inter-mixed source/assembly .html for switch statements implemented as jump-tables.
The following table lists those components where a switch was present.
Legend:
- JT - Jump Table implementation found
- OK - No Jump-Table
- N/A - Not Applicable, i.e. architecture not supported.
| Component | Assignee | MIPS | PPC | X86 | Remarks |
|---|---|---|---|---|---|
| afdx-library-4.6.0 | N/A | JT | N/A | Legacy | |
| afdx-driver-6.0.1 | N/A | JT | N/A | Legacy | |
| ansi-4.1.4 | TR | Done | Done | Done | |
| arinc664-library-1.1.1.1 | TR | N/A | Done | N/A | Hosmer |
| cffsi7sata-3.0.1 | N/A | N/A | OK | ||
| cffsnorflash-3.5.0 | TR | N/A | Done | N/A | Hosmer |
| cffs-server-6.1.0 | TR | N/A | Done | Done | |
| deos653p1-runtime-3.1.3 | TR | Done | Done | Done | |
| emac-prl-2.0.0 | N/A | OK | N/A | ||
| kernel-7.6.1 | N/A | JT | JT | Legacy | |
| kernel-7.6.2 | N/A | JT | JT | Legacy | |
| kernel-7.10.6 | TR | N/A | Done | Done | Hosmer |
| math-1.0.2 | OK | OK | N/A | ||
| math-x86-2.1.0 | N/A | N/A | OK | ||
| pro1000-process-2.2.0 | N/A | N/A | OK | ||
| rtl81xx-platform-resource-library-1.1.0 | N/A | N/A | OK | ||
| tdl-integrity-library-4.0.3 | N/A | OK | OK | ||
| tsec-durant-prl-2.0.0 | N/A | OK | N/A |
Jump-Table Rendition
So, what does the assembly language look like when GCC decides to implement a switch as a jump-table?
This is an x86 assembly language example:
switch (x)
120: 83 7d 08 08 cmpl $0x8,0x8(%ebp)
124: 77 56 ja 17c <_Z11testCase1_8i+0x69>
126: 8b 45 08 mov 0x8(%ebp),%eax
129: c1 e0 02 shl $0x2,%eax
12c: 05 00 00 00 00 add $0x0,%eax
131: 8b 00 mov (%eax),%eax
133: ff e0 jmp *%eax
{
case 1 :
a = 1;
135: c7 45 fc 01 00 00 00 movl $0x1,-0x4(%ebp)
break;
13c: eb 3e jmp 17c <_Z11testCase1_8i+0x69>
case 2 :
a = 2;
13e: c7 45 fc 02 00 00 00 movl $0x2,-0x4(%ebp)
break;
145: eb 35 jmp 17c <_Z11testCase1_8i+0x69>
case 3 :
a = 4;
147: c7 45 fc 04 00 00 00 movl $0x4,-0x4(%ebp)
break;
14e: eb 2c jmp 17c <_Z11testCase1_8i+0x69>
case 4 :
a = 8;
150: c7 45 fc 08 00 00 00 movl $0x8,-0x4(%ebp)
break;
157: eb 23 jmp 17c <_Z11testCase1_8i+0x69>
case 5 :
a = 16;
159: c7 45 fc 10 00 00 00 movl $0x10,-0x4(%ebp)
break;
160: eb 1a jmp 17c <_Z11testCase1_8i+0x69>
case 6 :
a = 32;
162: c7 45 fc 20 00 00 00 movl $0x20,-0x4(%ebp)
break;
169: eb 11 jmp 17c <_Z11testCase1_8i+0x69>
case 7 :
a = 64;
16b: c7 45 fc 40 00 00 00 movl $0x40,-0x4(%ebp)
break;
172: eb 08 jmp 17c <_Z11testCase1_8i+0x69>
case 8 :
a = 128;
174: c7 45 fc 80 00 00 00 movl $0x80,-0x4(%ebp)
break;
17b: 90 nop
} // switch
Boo. Notice the jmp *%eax at 133?
Now, here is how it should be rendered, with one conditional per possible outcome:
switch (x)
11d: 8b 45 08 mov 0x8(%ebp),%eax
120: 83 f8 04 cmp $0x4,%eax
123: 74 47 je 16c <_Z11testCase1_8i+0x5c> // conditional 1
125: 83 f8 04 cmp $0x4,%eax
128: 7f 11 jg 13b <_Z11testCase1_8i+0x2b> // conditional 2
12a: 83 f8 02 cmp $0x2,%eax
12d: 74 2b je 15a <_Z11testCase1_8i+0x4a> // conditional 3
12f: 83 f8 02 cmp $0x2,%eax
132: 7f 2f jg 163 <_Z11testCase1_8i+0x53> // conditional 4
134: 83 f8 01 cmp $0x1,%eax
137: 74 18 je 151 <_Z11testCase1_8i+0x41> // conditional 5
139: eb 5d jmp 198 <_Z11testCase1_8i+0x88>
13b: 83 f8 06 cmp $0x6,%eax
13e: 74 3e je 17e <_Z11testCase1_8i+0x6e> // conditional 6
140: 83 f8 06 cmp $0x6,%eax
143: 7c 30 jl 175 <_Z11testCase1_8i+0x65> // conditional 7
145: 83 f8 07 cmp $0x7,%eax
148: 74 3d je 187 <_Z11testCase1_8i+0x77> // conditional 8
14a: 83 f8 08 cmp $0x8,%eax
14d: 74 41 je 190 <_Z11testCase1_8i+0x80> // conditional 9
14f: eb 47 jmp 198 <_Z11testCase1_8i+0x88>
{
case 1 :
a = 1;
151: c7 45 fc 01 00 00 00 movl $0x1,-0x4(%ebp)
break;
158: eb 3e jmp 198 <_Z11testCase1_8i+0x88>
case 2 :
a = 2;
15a: c7 45 fc 02 00 00 00 movl $0x2,-0x4(%ebp)
break;
161: eb 35 jmp 198 <_Z11testCase1_8i+0x88>
case 3 :
a = 4;
163: c7 45 fc 04 00 00 00 movl $0x4,-0x4(%ebp)
break;
16a: eb 2c jmp 198 <_Z11testCase1_8i+0x88>
case 4 :
a = 8;
16c: c7 45 fc 08 00 00 00 movl $0x8,-0x4(%ebp)
break;
173: eb 23 jmp 198 <_Z11testCase1_8i+0x88>
case 5 :
a = 16;
175: c7 45 fc 10 00 00 00 movl $0x10,-0x4(%ebp)
break;
17c: eb 1a jmp 198 <_Z11testCase1_8i+0x88>
case 6 :
a = 32;
17e: c7 45 fc 20 00 00 00 movl $0x20,-0x4(%ebp)
break;
185: eb 11 jmp 198 <_Z11testCase1_8i+0x88>
case 7 :
a = 64;
187: c7 45 fc 40 00 00 00 movl $0x40,-0x4(%ebp)
break;
18e: eb 08 jmp 198 <_Z11testCase1_8i+0x88>
case 8 :
a = 128;
190: c7 45 fc 80 00 00 00 movl $0x80,-0x4(%ebp)
break;
197: 90 nop
} // switch
Recognizing code leading up to a jump table usage for various architectures can be difficult. It depends on whether the jump table is used in an executable or in a shared object.
At the time of writing several GCC Jump Table analyses have been carried out, and the results documented in the respective cert archives at 11-14-verf-results/analysis/executable-object-code/... There is an .htm file with the analysis, and a .bz2 file with its data.
This link describes all current architectures for the ANSI shared object and contains a description of the procedures used for the various architectures, as well its application for ANSI:
Later analysis reports have extended the procedure descriptions to also cover the executables when these
needed handling as this for Hosmer kernel-7.10.6:
