-
Notifications
You must be signed in to change notification settings - Fork 2
/
hotfix.patch
265 lines (240 loc) · 10.3 KB
/
hotfix.patch
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
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
# Missing includes
diff -u a/dios/CMakeLists.txt b/dios/CMakeLists.txt
--- a/dios/CMakeLists.txt 2019-11-01 15:57:40.145739566 +0100
+++ b/dios/CMakeLists.txt 2019-11-01 15:57:40.145739566 +0100
@@ -10,7 +10,7 @@
include/netinet/*.h include/arpa/*.h
libcxxabi/include/*
libcxxabi/src/*.h libcxxabi/src/*.hpp libcxxabi/src/*.ipp
- libcxx/include/* libcxx/ext/* libcxx/include/experimental/*
+ libcxx/include/* libcxx/include/ext/* libcxx/include/experimental/*
libcxx/src/*.h
libcxx/include/support/xlocale/*.h libcxx/src/support/atomic_support.h
libcxx/include/support/divine/*.h
# Missing build dependencies
diff -u a/divine/CMakeLists.txt b/divine/CMakeLists.txt
--- a/divine/CMakeLists.txt
+++ b/divine/CMakeLists.txt
@@ -69,7 +69,8 @@ target_link_libraries( divine-cc LLVMCore LLVMSupport LLVMMC LLVMIRReader
LLVMObject LLVMTransformUtils ${CC_TGTS}
clang clangBasic clangCodeGen lldELF )
target_link_libraries( divine-smt ${Z3_LIBRARIES} ${STP_LIBRARIES} )
-target_link_libraries( divine-dbg divine-vm )
+target_link_libraries( divine-vm divine-cc )
+target_link_libraries( divine-dbg divine-vm divine-smt )
target_link_libraries( divine-mc divine-vm divine-dbg divine-smt divine-rt divine-cc # FIXME divine-cc
liblart LLVMBitReader LLVMBitWriter LLVMLinker )
target_link_libraries( divine-ui divine-rt divine-cc divine-mc divine-ltl divine-ra )
diff -u a/dios/CMakeLists.txt b/dios/CMakeLists.txt
--- a/dios/CMakeLists.txt
+++ b/dios/CMakeLists.txt
@@ -132,6 +132,7 @@ include_directories( ${divine_SOURCE_DIR} )
add_definitions( -Wno-overlength-strings ${DIVINE_DEFINES} )
file( GLOB SRC_rt ${divine_SOURCE_DIR}/divine/rt/*.cpp )
add_library( divine-rt ${SRC_rt} ${dios_FILES} ${dios_native_FILES} dios_list.cpp dios_native_list.cpp )
+add_dependencies( divine-rt cxxabi_static cxx_static )
target_link_libraries( divine-rt divine-cc )
set_target_properties( divine-rt PROPERTIES POSITION_INDEPENDENT_CODE ON )
install( TARGETS divine-rt DESTINATION lib )
# Fix make install
diff -u a/dios/libcxx/CMakeLists.txt b/dios/libcxx/CMakeLists.txt
--- a/dios/libcxx/CMakeLists.txt
+++ b/dios/libcxx/CMakeLists.txt
@@ -214,13 +214,13 @@ cmake_dependent_option(LIBCXX_STATICALLY_LINK_ABI_IN_SHARED_LIBRARY
# is on. This option is also disabled when the ABI library is not specified
# or is specified to be "none".
set(ENABLE_LINKER_SCRIPT_DEFAULT_VALUE OFF)
-if (LLVM_HAVE_LINK_VERSION_SCRIPT AND NOT LIBCXX_STATICALLY_LINK_ABI_IN_SHARED_LIBRARY
- AND NOT LIBCXX_CXX_ABI_LIBNAME STREQUAL "none"
- AND NOT LIBCXX_CXX_ABI_LIBNAME STREQUAL "default"
- AND PYTHONINTERP_FOUND
- AND LIBCXX_ENABLE_SHARED)
- set(ENABLE_LINKER_SCRIPT_DEFAULT_VALUE ON)
-endif()
+# if (LLVM_HAVE_LINK_VERSION_SCRIPT AND NOT LIBCXX_STATICALLY_LINK_ABI_IN_SHARED_LIBRARY
+# AND NOT LIBCXX_CXX_ABI_LIBNAME STREQUAL "none"
+# AND NOT LIBCXX_CXX_ABI_LIBNAME STREQUAL "default"
+# AND PYTHONINTERP_FOUND
+# AND LIBCXX_ENABLE_SHARED)
+# set(ENABLE_LINKER_SCRIPT_DEFAULT_VALUE ON)
+# endif()
option(LIBCXX_ENABLE_ABI_LINKER_SCRIPT
"Use and install a linker script for the given ABI library"
# Set ENOMEM when calloc fails
diff -u a/dios/libc/_PDCLIB/glue.c b/dios/libc/_PDCLIB/glue.c
--- a/dios/libc/_PDCLIB/glue.c 2020-03-06 10:34:29.466926505 +0100
+++ b/dios/libc/_PDCLIB/glue.c 2020-03-06 10:34:29.466926505 +0100
@@ -101,8 +101,10 @@
void *mem = __vm_obj_make( n * size, _VM_PT_Heap ); // success
memset( mem, 0, n * size );
r = mem;
- } else
+ } else {
+ errno = ENOMEM;
r = NULL; // failure
+ }
__dios_mask( masked );
return r;
}
# Assume, that divine never reads from/writes to a terminal
diff --git a/dios/libc/sys/fs.cpp b/dios/libc/sys/fs.cpp
index d33696e8a..b0219eeec 100644
--- a/dios/libc/sys/fs.cpp
+++ b/dios/libc/sys/fs.cpp
@@ -260,13 +260,9 @@ extern "C" {
return res == 0 ? ENOTTY : res;
}
- int isatty(int fd)
+ int isatty(int /* fd */)
{
- struct stat fdStat;
-
- //just to set errno if fd is not valid file descriptor
- int res = __libc_fstat( fd, &fdStat );
- return res == 0 ? EINVAL : res;
+ return 0;
}
# patch 1a34f962f5e5640edf1b2215891a48ff5d7c9871
# Author: Petr Rockai <[email protected]>
# Date: Fri Mar 26 01:34:40 CET 2021
# * dios: Fix configuration of stdout/stderr tracing (#110).
# diff -rN -u old-divine-next/dios/vfs/file.hpp new-divine-next/dios/vfs/file.hpp
--- old-divine-next/dios/vfs/file.hpp 2021-04-05 23:00:21.867097482 +0200
+++ new-divine-next/dios/vfs/file.hpp 2021-04-05 23:00:21.867097482 +0200
@@ -97,6 +97,12 @@
Array< char > _content;
};
+struct NullFile : INode
+{
+ bool canWrite( int, Node ) const override { return true; }
+ bool write( const char *, size_t, size_t &, Node ) override { return true; }
+};
+
/* Each write is propagated to the trace/counterexample. */
struct VmTraceFile : INode
{
# diff -rN -u old-divine-next/dios/vfs/manager.h new-divine-next/dios/vfs/manager.h
--- old-divine-next/dios/vfs/manager.h 2021-04-05 23:00:21.867097482 +0200
+++ new-divine-next/dios/vfs/manager.h 2021-04-05 23:00:21.867097482 +0200
@@ -196,20 +196,20 @@
static Node make_tracefile( SysOpts& o, std::string_view stream )
{
- auto r = std::find_if( o.begin(), o.end(),
- [&]( const auto& o ) { return o.first == stream; } );
+ auto r = extract_opt( stream, o );
- if ( r == o.end() || r->second == "trace" )
+ if ( r.empty() || r == "trace" )
return new VmBuffTraceFile();
- if ( r->second == "unbuffered" )
+ if ( r == "unbuffered" )
return new VmTraceFile();
- if ( r->second == "notrace" )
- return nullptr;
+ if ( r == "notrace" )
+ return new NullFile();
__dios_trace_f( "Invalid configuration for file %.*s",
int( stream.size() ), stream.begin() );
- __dios_fault( _DiOS_F_Config, "Invalid file tracing configuration" );
- __builtin_trap();
+ __vm_ctl_flag( 0, _VM_CF_Error );
+
+ return new NullFile();
}
private: /* helper methods */
diff --git a/divine/cc/cc1.cpp b/divine/cc/cc1.cpp
index 5206553d8..edba4394c 100644
--- a/divine/cc/cc1.cpp
+++ b/divine/cc/cc1.cpp
@@ -147,6 +147,7 @@ namespace divine::cc
};
bool exceptions = type == FileType::Cpp || type == FileType::CppPreprocessed;
bool reloc_model_present = false;
+ bool no_strict_aliasing = false;
for ( auto &a : args )
{
@@ -154,11 +155,16 @@ namespace divine::cc
exceptions = false;
if ( a == "-mrelocation-model" )
reloc_model_present = true;
+ if ( a == "-fno-strict-aliasing" )
+ no_strict_aliasing = true;
}
if ( !reloc_model_present )
add( args, { "-mrelocation-model", "static" } );
+ if ( no_strict_aliasing )
+ add( args, { "-relaxed-aliasing" } );
+
add( args, cc1args );
if ( exceptions )
add( args, { "-fcxx-exceptions", "-fexceptions" } );
@@ -168,7 +174,7 @@ namespace divine::cc
std::vector< const char * > cc1a;
for ( auto &a : args )
- if ( a != "-fno-exceptions" )
+ if ( a != "-fno-exceptions" && a != "-fno-strict-aliasing" )
cc1a.push_back( a.c_str() );
TRACE( "cc1", cc1a );
diff --git a/divine/cc/options.cpp b/divine/cc/options.cpp
index ff7e08dec..aad94b990 100644
--- a/divine/cc/options.cpp
+++ b/divine/cc/options.cpp
@@ -103,7 +103,7 @@ namespace divine::cc
po.preprocessOnly = true;
else if ( *it == "-shared" )
po.shared = true;
- else if ( *it == "-fPIC" )
+ else if ( *it == "-fPIC" || *it == "-fpic" )
{
po.pic = true;
add( po.cc1_args, { "-pic-level", "1",
# We are on x86_64 and link failures should not be fatal!
diff --git a/divine/rt/dios-cc.cpp b/divine/rt/dios-cc.cpp
index 137f6b059..b33041b97 100644
--- a/divine/rt/dios-cc.cpp
+++ b/divine/rt/dios-cc.cpp
@@ -46,8 +46,6 @@ void add_dios_defines( std::vector< std::string >& flags )
, "-D__ELF__"
, "-D__unix__"
, "-D__divine__=4"
- , "-U__x86_64"
- , "-U__x86_64__"
});
}
@@ -73,7 +71,7 @@ NativeDiosCC::NativeDiosCC( const std::vector< std::string >& opts )
add_dios_header_paths( _po.opts );
add_dios_defines( _po.opts );
divine::rt::each( [&]( auto path, auto c ) { _clang.mapVirtualFile( path, c ); } );
- _missing_bc_fatal = true;
+ _missing_bc_fatal = false;
}
auto NativeDiosCC::link_dios_native( bool cxx )
diff --git a/divine/rt/dios-cc.cpp b/divine/rt/dios-cc.cpp
index 137f6b059..f5049d11c 100644
--- a/divine/rt/dios-cc.cpp
+++ b/divine/rt/dios-cc.cpp
@@ -107,17 +107,17 @@ std::unique_ptr< llvm::Module > NativeDiosCC::link_bitcode()
m = drv->takeLinked();
- if ( !_po.shared )
- {
- for ( auto& func : *m )
- if ( func.isDeclaration() && !whitelisted( func ) )
- throw cc::CompileError( "Symbol undefined (function): " + func.getName().str() );
-
- for ( auto& val : m->globals() )
- if ( auto G = dyn_cast< llvm::GlobalVariable >( &val ) )
- if ( !G->hasInitializer() && !whitelisted( *G ) )
- throw cc::CompileError( "Symbol undefined (global variable): " + G->getName().str() );
- }
+ // if ( !_po.shared )
+ // {
+ // for ( auto& func : *m )
+ // if ( func.isDeclaration() && !whitelisted( func ) )
+ // throw cc::CompileError( "Symbol undefined (function): " + func.getName().str() );
+
+ // for ( auto& val : m->globals() )
+ // if ( auto G = dyn_cast< llvm::GlobalVariable >( &val ) )
+ // if ( !G->hasInitializer() && !whitelisted( *G ) )
+ // throw cc::CompileError( "Symbol undefined (global variable): " + G->getName().str() );
+ // }
verifyModule( *m );
return m;