forked from aufover/rpm-divine
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathhotfix.patch
157 lines (143 loc) · 6.32 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
# 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 */