diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-10 14:06:41 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-10 14:06:41 +0200 |
| commit | 3d0204fddb71ca377fa65952ede872583c8a7242 (patch) | |
| tree | 4563132cbe6e9d103ea6e2178f7b9ecaae4c0246 /test/monniaux/minisat | |
| parent | be92a8c71192e014caf292312865dee32ee1b901 (diff) | |
| download | compcert-kvx-3d0204fddb71ca377fa65952ede872583c8a7242.tar.gz compcert-kvx-3d0204fddb71ca377fa65952ede872583c8a7242.zip | |
various fixes for aarch64 profiling
Diffstat (limited to 'test/monniaux/minisat')
| -rw-r--r-- | test/monniaux/minisat/Makefile.profiled | 16 | ||||
| -rw-r--r-- | test/monniaux/minisat/solver.h | 5 |
2 files changed, 15 insertions, 6 deletions
diff --git a/test/monniaux/minisat/Makefile.profiled b/test/monniaux/minisat/Makefile.profiled index 840261b4..349089b7 100644 --- a/test/monniaux/minisat/Makefile.profiled +++ b/test/monniaux/minisat/Makefile.profiled @@ -1,28 +1,32 @@ +# -*- mode: makefile; -*- + CFILES=main.c solver.c clock.c GCDAFILES=$(CFILES:.c=.gcda) CCOMP=../../../ccomp -GCC=k1-cos-gcc +GCC=aarch64-linux-gnu-gcc # k1-cos-gcc LIBS=-lm PROFILING_DAT=compcert_profiling.dat -EXECUTE=k1-cluster -- +EXECUTE=qemu-aarch64 # k1-cluster -- EXECUTE_CYCLES=k1-cluster --cycle-based -- EXAMPLE=sudoku.sat -CCOMPFLAGS=-finline-auto-threshold 50 +CCOMPFLAGS=-finline-auto-threshold 50 -static -finline-asm +GCCFLAGS=-static ALL=minisat.ccomp.log minisat.ccomp.trace-linearize.log minisat.ccomp.profiled.log minisat.gcc-O3.log minisat.gcc-O3.profiled.log all: $(ALL) +exe: $(ALL:.log=.exe) minisat.ccomp.exe: $(CFILES) $(CCOMP) $(CCOMPFLAGS) $(CFILES) -o $@ $(LIBS) minisat.ccomp.profile-arcs.exe: $(CFILES) - $(CCOMP) $(CCOMPFLAGS) -fprofile-arcs $(CFILES) -o $@ $(LIBS) + $(CCOMP) -DAMD_NO_PRIVILEGE $(CCOMPFLAGS) -fprofile-arcs $(CFILES) -o $@ $(LIBS) minisat.gcc-O3.exe: $(CFILES) $(GCC) $(GCCFLAGS) -O3 $(CFILES) -o $@ $(LIBS) minisat.gcc-O3.profile-arcs.exe: $(CFILES) - $(GCC) $(GCCFLAGS) -fprofile-arcs -O3 $(CFILES) -o $@ $(LIBS) + $(GCC) -DAMD_NO_PRIVILEGE $(GCCFLAGS) -fprofile-arcs -O3 $(CFILES) -o $@ $(LIBS) gcda: minisat.gcc-O3.profile-arcs.exe $(EXECUTE) $< $(EXAMPLE) @@ -48,6 +52,6 @@ minisat.ccomp.profiled.exe: $(CFILES) $(PROFILING_DAT) clean: -rm -f *.log *.exe $(PROFILING_DAT) $(GCDAFILES) -.PHONY: clean gcda +.PHONY: clean gcda exe all .SECONDARY: diff --git a/test/monniaux/minisat/solver.h b/test/monniaux/minisat/solver.h index c9ce0219..4b96b017 100644 --- a/test/monniaux/minisat/solver.h +++ b/test/monniaux/minisat/solver.h @@ -19,6 +19,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA **************************************************************************************************/ // Modified to compile with MS Visual Studio 6.0 by Alan Mishchenko +#include <stdint.h> + #ifndef solver_h #define solver_h @@ -39,11 +41,14 @@ static const bool false = 0; typedef int lit; typedef char lbool; +#if 0 #ifdef _WIN32 typedef signed __int64 uint64; // compatible with MS VS 6.0 #else typedef unsigned long long uint64; #endif +#endif +typedef uint64_t uint64; static const int var_Undef = -1; static const lit lit_Undef = -2; |