Skip to content

Commit 5e6b593

Browse files
author
Daniel Kroening
authored
Merge pull request #957 from karkhaz/kk
[goto-cc] Add support for ARM-enabling flags
2 parents fedc90b + 21d0610 commit 5e6b593

File tree

20 files changed

+281
-1
lines changed

20 files changed

+281
-1
lines changed

‎appveyor.yml

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,10 @@ test_script:
7575
cat goto-instrument-typedef/chain.sh || true
7676
7777
rem HACK disable failing tests
78+
rmdir /s /q ansi-c\arch_flags_mcpu_bad
79+
rmdir /s /q ansi-c\arch_flags_mcpu_good
80+
rmdir /s /q ansi-c\arch_flags_mthumb_bad
81+
rmdir /s /q ansi-c\arch_flags_mthumb_good
7882
rmdir /s /q ansi-c\Forward_Declaration2
7983
rmdir /s /q ansi-c\Incomplete_Type1
8084
rmdir /s /q ansi-c\Union_Padding1

‎regression/ansi-c/arch_flags_mcpu_bad/object.intel

4.29 KB
Binary file not shown.

‎regression/ansi-c/arch_flags_mcpu_bad/preproc.i

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
int foo() { return 3; }

‎regression/ansi-c/arch_flags_mcpu_bad/source.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
int bar(){ return 9; }

‎regression/ansi-c/arch_flags_mcpu_bad/test.desc

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
CORE
2+
preproc.i
3+
-mcpu=cortex-a15 -o linked-object.gb object.intel
4+
^EXIT=(64|1)$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
^CONVERSION ERROR$
9+
--
10+
This tests the -mcpu=cortex=a15 flag that should activate ARM-32 mode.
11+
The object file 'object.intel' was compiled from 'source.c' with goto-cc
12+
on a 64-bit platform:
13+
14+
goto-cc -c source.c
15+
16+
preproc.i is already pre-processed so that it can be linked in without
17+
needing to invoke a pre-processor from a cross-compile toolchain on your
18+
local machine. Linking it together with the Intel object file, while
19+
passing -mcpu=cortex-a15 on the command line, should fail because
20+
-mcpu=cortex-a15 implies that we're trying to make an ARM executable.

‎regression/ansi-c/arch_flags_mcpu_good/object.arm

4.08 KB
Binary file not shown.

‎regression/ansi-c/arch_flags_mcpu_good/preproc.i

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
int foo() { return 3; }

‎regression/ansi-c/arch_flags_mcpu_good/source.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
int bar(){ return 9; }

‎regression/ansi-c/arch_flags_mcpu_good/test.desc

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
CORE
2+
preproc.i
3+
-mcpu=cortex-a15 -o linked-object.gb object.arm
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
^CONVERSION ERROR$
9+
--
10+
This tests the -mcpu=cortex-a15 flag that should activate ARM-32 mode.
11+
The object file 'object.arm' was compiled from 'source.c' with goto-cc
12+
along with an ARM cross-compiler on a 64-bit platform with the following
13+
command line:
14+
15+
goto-cc --native-compiler=arm-none-eabi-gcc -mcpu=cortex-a15 -c source.c
16+
17+
preproc.i is already pre-processed so that it can be linked in without
18+
needing to invoke a pre-processor from a cross-compile toolchain on your
19+
local machine. Linking it together with the ARM object file, while
20+
passing -mcpu=cortex-a15 on the command line, should succeed.

‎regression/ansi-c/arch_flags_mthumb_bad/object.intel

4.29 KB
Binary file not shown.

‎regression/ansi-c/arch_flags_mthumb_bad/preproc.i

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
int foo() { return 3; }

‎regression/ansi-c/arch_flags_mthumb_bad/source.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
int bar(){ return 9; }

‎regression/ansi-c/arch_flags_mthumb_bad/test.desc

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
CORE
2+
preproc.i
3+
-mthumb -o linked-object.gb object.intel
4+
^EXIT=(64|1)$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
^CONVERSION ERROR$
9+
--
10+
This tests the -mthumb flag that should activate ARM-32 mode. The object
11+
file 'object.intel' was compiled from 'source.c' with goto-cc on a
12+
64-bit platform:
13+
14+
goto-cc -c source.c
15+
16+
preproc.i is already pre-processed so that it can be linked in without
17+
needing to invoke a pre-processor from a cross-compile toolchain on your
18+
local machine. Linking it together with the Intel object file, while
19+
passing -mthumb on the command line, should fail because -mthumb implies
20+
that we're trying to make an ARM executable.

‎regression/ansi-c/arch_flags_mthumb_good/object.arm

4.08 KB
Binary file not shown.

‎regression/ansi-c/arch_flags_mthumb_good/preproc.i

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
int foo() { return 3; }

‎regression/ansi-c/arch_flags_mthumb_good/source.c

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
int bar(){ return 9; }

‎regression/ansi-c/arch_flags_mthumb_good/test.desc

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
CORE
2+
preproc.i
3+
-mthumb -o linked-object.gb object.arm
4+
^EXIT=0$
5+
^SIGNAL=0$
6+
--
7+
^warning: ignoring
8+
^CONVERSION ERROR$
9+
--
10+
This tests the -mthumb flag that should activate ARM-32 mode. The object
11+
file 'object.arm' was compiled from 'source.c' with goto-cc along with
12+
an ARM cross-compiler on a 64-bit platform with the following command
13+
line:
14+
15+
goto-cc --native-compiler=arm-none-eabi-gcc -mthumb -c source.c
16+
17+
preproc.i is already pre-processed so that it can be linked in without
18+
needing to invoke a pre-processor from a cross-compile toolchain on your
19+
local machine. Linking it together with the ARM object file, while
20+
passing -mthumb on the command line, should succeed.

‎src/goto-cc/gcc_cmdline.cpp

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -96,6 +96,9 @@ const char *gcc_options_with_separated_argument[]=
9696
"-isysroot",
9797
"-imultilib",
9898
"-imultiarch",
99+
"-mcpu",
100+
"-mtune",
101+
"-march",
99102
"-Xpreprocessor",
100103
"-Xassembler",
101104
"-Xlinker",
@@ -188,6 +191,9 @@ const char *gcc_options_without_argument[]=
188191
"-MP",
189192
"-MD",
190193
"-MMD",
194+
"-mno-unaligned-access",
195+
"-mthumb",
196+
"-mthumb-interwork",
191197
"-nostdinc",
192198
"-P",
193199
"-remap",

‎src/goto-cc/gcc_mode.cpp

Lines changed: 181 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -124,7 +124,142 @@ gcc_modet::gcc_modet(
124124
goto_cc_modet(_cmdline, _base_name, gcc_message_handler),
125125
produce_hybrid_binary(_produce_hybrid_binary),
126126
act_as_ld(base_name=="ld" ||
127-
base_name.find("goto-ld")!=std::string::npos)
127+
base_name.find("goto-ld")!=std::string::npos),
128+
129+
// Keys are architectures specified in configt::set_arch().
130+
// Values are lists of GCC architectures that can be supplied as
131+
// arguments to the -march, -mcpu, and -mtune flags (see the GCC
132+
// manual https://gcc.gnu.org/onlinedocs/).
133+
arch_map(
134+
{
135+
// ARM information taken from the following:
136+
//
137+
// the "ARM core timeline" table on this page:
138+
// https://en.wikipedia.org/wiki/List_of_ARM_microarchitectures
139+
//
140+
// articles on particular core groups, e.g.
141+
// https://en.wikipedia.org/wiki/ARM9
142+
//
143+
// The "Cores" table on this page:
144+
// https://en.wikipedia.org/wiki/ARM_architecture
145+
// NOLINTNEXTLINE(whitespace/braces)
146+
{"arm", {
147+
"strongarm", "strongarm110", "strongarm1100", "strongarm1110",
148+
"arm2", "arm250", "arm3", "arm6", "arm60", "arm600", "arm610",
149+
"arm620", "fa526", "fa626", "fa606te", "fa626te", "fmp626",
150+
"xscale", "iwmmxt", "iwmmxt2", "xgene1"
151+
}}, // NOLINTNEXTLINE(whitespace/braces)
152+
{"armhf", {
153+
"armv7", "arm7m", "arm7d", "arm7dm", "arm7di", "arm7dmi",
154+
"arm70", "arm700", "arm700i", "arm710", "arm710c", "arm7100",
155+
"arm720", "arm7500", "arm7500fe", "arm7tdmi", "arm7tdmi-s",
156+
"arm710t", "arm720t", "arm740t", "mpcore", "mpcorenovfp",
157+
"arm8", "arm810", "arm9", "arm9e", "arm920", "arm920t",
158+
"arm922t", "arm946e-s", "arm966e-s", "arm968e-s", "arm926ej-s",
159+
"arm940t", "arm9tdmi", "arm10tdmi", "arm1020t", "arm1026ej-s",
160+
"arm10e", "arm1020e", "arm1022e", "arm1136j-s", "arm1136jf-s",
161+
"arm1156t2-s", "arm1156t2f-s", "arm1176jz-s", "arm1176jzf-s",
162+
"cortex-a5", "cortex-a7", "cortex-a8", "cortex-a9",
163+
"cortex-a12", "cortex-a15", "cortex-a53", "cortex-r4",
164+
"cortex-r4f", "cortex-r5", "cortex-r7", "cortex-m7",
165+
"cortex-m4", "cortex-m3", "cortex-m1", "cortex-m0",
166+
"cortex-m0plus", "cortex-m1.small-multiply",
167+
"cortex-m0.small-multiply", "cortex-m0plus.small-multiply",
168+
"marvell-pj4", "ep9312", "fa726te",
169+
}}, // NOLINTNEXTLINE(whitespace/braces)
170+
{"arm64", {
171+
"cortex-a57", "cortex-a72", "exynos-m1"
172+
}},
173+
// There are two MIPS architecture series. The 'old' one comprises
174+
// MIPS I - MIPS V (where MIPS I and MIPS II are 32-bit
175+
// architectures, and the III, IV and V are 64-bit). The 'new'
176+
// architecture series comprises MIPS32 and MIPS64. Source: [0].
177+
//
178+
// CPROVER's names for these are in configt::this_architecture(),
179+
// in particular note the preprocessor variable names. MIPS
180+
// processors can run in little-endian or big-endian mode; [1]
181+
// gives more information on particular processors. Particular
182+
// processors and their architectures are at [2]. This means that
183+
// we cannot use the processor flags alone to decide which CPROVER
184+
// name to use; we also need to check for the -EB or -EL flags to
185+
// decide whether little- or big-endian code should be generated.
186+
// Therefore, the keys in this part of the map don't directly map
187+
// to CPROVER architectures.
188+
//
189+
// [0] https://en.wikipedia.org/wiki/MIPS_architecture
190+
// [1] https://www.debian.org/ports/mips/
191+
// [2] https://en.wikipedia.org/wiki/List_of_MIPS_architecture_processors
192+
// NOLINTNEXTLINE(whitespace/braces)
193+
{"mips64n", {
194+
"loongson2e", "loongson2f", "loongson3a", "mips64", "mips64r2",
195+
"mips64r3", "mips64r5", "mips64r6 4kc", "5kc", "5kf", "20kc",
196+
"octeon", "octeon+", "octeon2", "octeon3", "sb1", "vr4100",
197+
"vr4111", "vr4120", "vr4130", "vr4300", "vr5000", "vr5400",
198+
"vr5500", "sr71000", "xlp",
199+
}}, // NOLINTNEXTLINE(whitespace/braces)
200+
{"mips32n", {
201+
"mips32", "mips32r2", "mips32r3", "mips32r5", "mips32r6",
202+
// https://www.imgtec.com/mips/classic/
203+
"4km", "4kp", "4ksc", "4kec", "4kem", "4kep", "4ksd", "24kc",
204+
"24kf2_1", "24kf1_1", "24kec", "24kef2_1", "24kef1_1", "34kc",
205+
"34kf2_1", "34kf1_1", "34kn", "74kc", "74kf2_1", "74kf1_1",
206+
"74kf3_2", "1004kc", "1004kf2_1", "1004kf1_1", "m4k", "m14k",
207+
"m14kc", "m14ke", "m14kec",
208+
// https://en.wikipedia.org/wiki/List_of_MIPS_architecture_processors
209+
"p5600", "xlr",
210+
}}, // NOLINTNEXTLINE(whitespace/braces)
211+
{"mips32o", {
212+
"mips1", "mips2", "r2000", "r3000",
213+
"r6000", // Not a mistake, r4000 came out _after_ this
214+
}}, // NOLINTNEXTLINE(whitespace/braces)
215+
{"mips64o", {
216+
"mips3", "mips4", "r4000", "r4400", "r4600", "r4650", "r4700",
217+
"r8000", "rm7000", "rm9000", "r10000", "r12000", "r14000",
218+
"r16000",
219+
}},
220+
// These are IBM mainframes. s390 is 32-bit; s390x is 64-bit [0].
221+
// Search that page for s390x and note that 32-bit refers to
222+
// everything "prior to 2000's z900 model". The list of model
223+
// numbers is at [1].
224+
// [0] https://en.wikipedia.org/wiki/Linux_on_z_Systems
225+
// [1] https://en.wikipedia.org/wiki/IBM_System_z
226+
// NOLINTNEXTLINE(whitespace/braces)
227+
{"s390", {
228+
"z900", "z990", "g5", "g6",
229+
}}, // NOLINTNEXTLINE(whitespace/braces)
230+
{"s390x", {
231+
"z9-109", "z9-ec", "z10", "z196", "zEC12", "z13"
232+
}},
233+
// SPARC
234+
// In the "Implementations" table of [0], everything with an arch
235+
// version up to V8 is 32-bit. V9 and onward are 64-bit.
236+
// [0] https://en.wikipedia.org/wiki/SPARC
237+
// NOLINTNEXTLINE(whitespace/braces)
238+
{"sparc", {
239+
"v7", "v8", "leon", "leon3", "leon3v7", "cypress", "supersparc",
240+
"hypersparc", "sparclite", "f930", "f934", "sparclite86x",
241+
"tsc701",
242+
}}, // NOLINTNEXTLINE(whitespace/braces)
243+
{"sparc64", {
244+
"v9", "ultrasparc", "ultrasparc3", "niagara", "niagara2",
245+
"niagara3", "niagara4",
246+
}}, // NOLINTNEXTLINE(whitespace/braces)
247+
{"ia64", {
248+
"itanium", "itanium1", "merced", "itanium2", "mckinley"
249+
}}, // NOLINTNEXTLINE(whitespace/braces)
250+
{"i386", {
251+
"i386", "i486", "i586", "pentium", "pentium-mmx", "pentiumpro",
252+
"i686", "pentium2", "pentium3", "pentium3m", "pentium-m",
253+
"pentium4", "pentium4m", "prescott", "nocona", "core2", "nehalem",
254+
"westmere", "sandybridge", "ivybridge", "haswell", "broadwell",
255+
"bonnell", "silvermont", "k6", "k6-2", "k6-3", "athlon",
256+
"athlon-tbird", "athlon-4", "athlon-xp", "athlon-mp", "k8",
257+
"opteron", "athlon64", "athlon-fx", "k8-sse3", "opteron-sse3",
258+
"athlon64-sse3", "amdfam10", "barcelona", "bdver1", "bdver2",
259+
"bdver3", "bdver4", "btver1", "btver2", "winchip-c6", "winchip2",
260+
"c3", "c3-2", "geode",
261+
}},
262+
})
128263
{
129264
}
130265

@@ -286,6 +421,51 @@ int gcc_modet::doit()
286421
else if(cmdline.isset("little-endian") || cmdline.isset("mlittle"))
287422
config.ansi_c.endianness=configt::ansi_ct::endiannesst::IS_LITTLE_ENDIAN;
288423

424+
if(cmdline.isset("mthumb") || cmdline.isset("mthumb-interwork"))
425+
config.ansi_c.set_arch_spec_arm("armhf");
426+
427+
// -mcpu sets both the arch and tune, but should only be used if
428+
// neither -march nor -mtune are passed on the command line.
429+
std::string target_cpu=
430+
cmdline.isset("march") ? cmdline.get_value("march") :
431+
cmdline.isset("mtune") ? cmdline.get_value("mtune") :
432+
cmdline.isset("mcpu") ? cmdline.get_value("mcpu") : "";
433+
434+
if(target_cpu!="")
435+
{
436+
// Work out what CPROVER architecture we should target.
437+
for(auto &pair : arch_map)
438+
for(auto &processor : pair.second)
439+
if(processor==target_cpu)
440+
{
441+
if(pair.first.find("mips")==std::string::npos)
442+
config.set_arch(pair.first);
443+
else
444+
{
445+
// Targeting a MIPS processor. MIPS is special; we also need
446+
// to know the endianness. -EB (big-endian) is the default.
447+
if(cmdline.isset("EL"))
448+
{
449+
if(pair.first=="mips32o")
450+
config.set_arch("mipsel");
451+
else if(pair.first=="mips32n")
452+
config.set_arch("mipsn32el");
453+
else
454+
config.set_arch("mips64el");
455+
}
456+
else
457+
{
458+
if(pair.first=="mips32o")
459+
config.set_arch("mips");
460+
else if(pair.first=="mips32n")
461+
config.set_arch("mipsn32");
462+
else
463+
config.set_arch("mips64");
464+
}
465+
}
466+
}
467+
}
468+
289469
// -fshort-wchar makes wchar_t "short unsigned int"
290470
if(cmdline.isset("fshort-wchar"))
291471
{

‎src/goto-cc/gcc_mode.h

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -34,6 +34,8 @@ class gcc_modet:public goto_cc_modet
3434
const bool act_as_ld;
3535
std::string native_tool_name;
3636

37+
const std::map<std::string, std::set<std::string>> arch_map;
38+
3739
int preprocess(
3840
const std::string &language,
3941
const std::string &src,

0 commit comments

Comments
 (0)