-
Notifications
You must be signed in to change notification settings - Fork 9
/
sparknacl.gpr
170 lines (146 loc) · 6.64 KB
/
sparknacl.gpr
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
library project Sparknacl is
for Library_Name use "Sparknacl";
for Library_Version use "0.0.0";
for Source_Dirs use ("src");
for Object_Dir use "obj";
for Create_Missing_Dirs use "True";
for Library_Dir use "lib";
type Library_Type_Type is ("relocatable", "static", "static-pic");
Library_Type : Library_Type_Type :=
external ("SPARKNACL_LIBRARY_TYPE", external ("LIBRARY_TYPE", "static"));
for Library_Kind use Library_Type;
type Enabled_Kind is ("enabled", "disabled");
Compile_Checks : Enabled_Kind := External ("SPARKNACL_COMPILE_CHECKS", "enabled");
Runtime_Checks : Enabled_Kind := External ("SPARKNACL_RUNTIME_CHECKS", "disabled");
Style_Checks : Enabled_Kind := External ("SPARKNACL_STYLE_CHECKS", "enabled");
Contracts_Checks : Enabled_Kind := External ("SPARKNACL_CONTRACTS", "disabled");
type Build_Kind is ("debug", "O1", "O2", "O3", "Os", "Og");
Build_Mode : Build_Kind := External ("SPARKNACL_BUILD_MODE", "O2");
type Runtime_Kind is ("full", "zfp");
Runtime_Mode : Runtime_Kind := External ("SPARKNACL_RUNTIME_MODE", "full");
-- Extend this list to add any options for specific targets and see below
type Target_Arch_Kind is ("unspecified", "rv32im", "rv32imc", "rv32imc_a4");
Target_Arch : Target_Arch_Kind := External ("SPARKNACL_TARGET_ARCH", "unspecified");
Callgraph_Switch := ("-fcallgraph-info=su,da");
Compile_Checks_Switches := ();
case Compile_Checks is
when "enabled" =>
Compile_Checks_Switches :=
("-gnatwaC", -- All warnings except redundant checks
"-gnatwe"); -- Warnings as errors
when others => null;
end case;
Runtime_Checks_Switches := ();
case Runtime_Checks is
when "enabled" => null;
when others =>
Runtime_Checks_Switches :=
("-gnatp"); -- Supress checks
end case;
Style_Checks_Switches := ();
case Style_Checks is
when "enabled" => null;
Style_Checks_Switches :=
("-gnaty"); -- style checks on
when others => null;
end case;
Contracts_Switches := ();
case Contracts_Checks is
when "enabled" =>
Contracts_Switches :=
("-gnata"); -- Enable assertions and contracts
when "disabled" =>
null;
end case;
Build_Switches := ();
case Build_Mode is
when "debug" =>
Build_Switches := ("-g", -- Debug info
"-O0"); -- No optimization
when "O1" =>
Build_Switches := ("-O1", -- Optimization
"-gnatn"); -- Enable inlining
when "O2" =>
Build_Switches := ("-O2", -- Optimization
"-gnatn"); -- Enable inlining
when "O3" =>
Build_Switches := ("-O3", -- Optimization
"-gnatn"); -- Enable inlining
when "Os" =>
Build_Switches := ("-Os"); -- Optimize for small code size, no inlining
when "Og" =>
Build_Switches := ("-g",
"-Og");
end case;
-- Extend this case choice for any other target/architecture specific switches
case Target_Arch is
when "rv32im" =>
Build_Switches := Build_Switches &
("-march=rv32im"); -- RV32IM but NO Compressed instructions
when "rv32imc" =>
Build_Switches := Build_Switches &
("-march=rv32imc"); -- RV32IM with Compressed instructions
when "rv32imc_a4" =>
Build_Switches := Build_Switches &
("-march=rv32imc") & -- Compressed instructions but all BBs on 4-byte alignment
("-falign-functions=4") &
("-falign-jumps=4") &
("-falign-loops=4") &
("-falign-labels=4");
when others => null;
end case;
case Runtime_Mode is
when "zfp" =>
for Runtime ("Ada") use "zfp";
for Excluded_Source_Files use ("sparknacl-debug.ads", "sparknacl-debug.adb", "sparknacl-pdebug.ads", "sparknacl-pdebug.adb");
when others =>
null;
end case;
package Compiler is
for Default_Switches ("Ada") use
Compile_Checks_Switches &
Callgraph_Switch &
Build_Switches &
Runtime_Checks_Switches &
Style_Checks_Switches &
Contracts_Switches &
("-ffunction-sections") & -- Create a linker section for each function
("-fdata-sections") & -- Create a linker section for each data area
("-gnatw.X") & -- Disable warnings for No_Exception_Propagation
("-gnatQ"); -- Don't quit. Generate ALI and tree files even if illegalities
case Runtime_Mode is
when "zfp" =>
case Contracts_Checks is
when "enabled" =>
for Local_Configuration_Pragmas use "src/sparknacl.adc";
when "disabled" =>
for Local_Configuration_Pragmas use "src/sparknacl_no_elab.adc";
end case;
when others =>
null; -- No Restrictions when compiling with full runtime
end case;
end Compiler;
package Binder is
for Switches ("Ada") use ("-Es"); -- Symbolic traceback
end Binder;
package Prove is
for Proof_Switches ("Ada") use ("--proof=per_path",
"-j6",
"--no-global-generation",
"--no-inlining",
"--no-loop-unrolling",
"--level=1",
"--prover=z3,cvc4,altergo",
"--timeout=60",
"--memlimit=0",
"--steps=200000",
"--report=statistics");
for Proof_Switches ("sparknacl-car.adb") use ("--prover=altergo,z3,cvc4");
for Proof_Switches ("sparknacl-utils.adb") use ("--prover=altergo,z3,cvc4"); -- ok with CE 2021
end Prove;
-- All the main NaCl entry points
Stack_Entry_Points := ("-esparknacl.sign.open,sparknacl.sign.sign,sparknacl.sign.keypair,sparknacl.cryptobox.create,sparknacl.cryptobox.open,sparknacl.cryptobox.keypair,sparknacl.secretbox.create,sparknacl.secretbox.open,sparknacl.core.salsa20,sparknacl.core.hsalsa20,sparknacl.stream.salsa20,sparknacl.stream.salsa20_xor,sparknacl.stream.hsalsa20,sparknacl.stream.hsalsa20_xor,sparknacl.mac.onetimeauth,sparknacl.mac.onetimeauth_verify,sparknacl.hashing.sha512.hash,sparknacl.hashing.sha256.hash,sparknacl.scalar.mult,sparknacl.scalar.mult_base,sparknacl.equal,sparknacl.random_bytes");
package Stack is
for Switches use ("-Wa", "-u 128", "-np", "-v") & Stack_Entry_Points;
end Stack;
end Sparknacl;