From 43c67c98877feeb2e91cb4be3835e70834379d5a Mon Sep 17 00:00:00 2001 From: Sylvain Boulmé Date: Tue, 3 Sep 2019 15:50:17 +0200 Subject: a dedicated entry-point to the doc of Coq sources --- doc/index-mppa_k1c.html | 380 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 380 insertions(+) create mode 100644 doc/index-mppa_k1c.html diff --git a/doc/index-mppa_k1c.html b/doc/index-mppa_k1c.html new file mode 100644 index 00000000..41a44a0d --- /dev/null +++ b/doc/index-mppa_k1c.html @@ -0,0 +1,380 @@ + + + +The CompCert verified compiler + + + + + + + +

The CompCert verified compiler

+

Commented Coq development

+

Version 3.5, 2019-02-27

+

PATCHED FOR MPPA-K1C

+ +

Introduction

+ +

CompCert is a compiler that generates PowerPC, ARM, RISC-V and x86 assembly +code from CompCert C, a large subset of the C programming language. +The particularity of this compiler is that it is written mostly within +the specification language of the Coq proof assistant, and its +correctness --- the fact that the generated assembly code is +semantically equivalent to its source program --- was entirely proved +within the Coq proof assistant.

+ +

High-level descriptions of the CompCert compiler and its proof of +correctness can be found in the following papers (in increasing order of technical details):

+ + +

This Web site gives a commented listing of the underlying Coq +specifications and proofs. Proof scripts are folded by default, but +can be viewed by clicking on "Proof". Some modules (written in italics below) differ between the four target architectures. The +PowerPC versions of these modules are shown below; the ARM, x86 and RISC-V +versions can be found in the source distribution. +

+ +

This development is a work in progress; some parts have +substantially changed since the overview papers above were +written.

+ +

The complete sources for CompCert can be downloaded from +the CompCert Web site.

+ +

This document and the CompCert sources are copyright Institut +National de Recherche en Informatique et en Automatique (INRIA) and +AbsInt Angewandte Informatik GmbH, and are distributed under the terms of the +following license. +

+ +

Table of contents

+ +

General-purpose libraries, data structures and algorithms

+ + + +

Definitions and theorems used in many parts of the development

+ + + +

Source, intermediate and target languages: syntax and semantics

+ + + +

Compiler passes

+ + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + +
PassSource & targetCompiler codeCorrectness proof
Pulling side-effects out of expressions;
+ fixing an evaluation order		CompCert C to ClightSimplExprSimplExprspec
+ SimplExprproof
Pulling non-adressable scalar local variables out of memoryClight to ClightSimplLocalsSimplLocalsproof
Simplification of control structures;
+ explication of type-dependent computations		Clight to CsharpminorCshmgenCshmgenproof
Stack allocation of local variables
+ whose address is taken;
+ simplification of switch statements		Csharpminor to CminorCminorgenCminorgenproof
Recognition of operators
and addressing modes		Cminor to CminorSelSelection
+ SelectOp
+ SelectLong
+ SelectDiv
+ SplitLong		Selectionproof
+ SelectOpproof
+ SelectLongproof
+ SelectDivproof
+ SplitLongproof
Construction of the CFG,
3-address code generation		CminorSel to RTLRTLgenRTLgenspec
+ RTLgenproof
Recognition of tail callsRTL to RTLTailcallTailcallproof
Function inliningRTL to RTLInliningInliningspec
+ Inliningproof
Postorder renumbering of the CFGRTL to RTLRenumberRenumberproof
Constant propagationRTL to RTLConstprop
+ ConstpropOp		Constpropproof
+ ConstproppOproof
Common subexpression eliminationRTL to RTLCSE
+ CombineOp		CSEproof
+ CombineOpproof
Redundancy eliminationRTL to RTLDeadcodeDeadcodeproof
Removal of unused static globalsRTL to RTLUnusedglobUnusedglobproof
Register allocation (validation a posteriori)RTL to LTLAllocationAllocproof
Branch tunnelingLTL to LTLTunnelingTunnelingproof
Linearization of the CFGLTL to LinearLinearizeLinearizeproof
Removal of unreferenced labelsLinear to LinearCleanupLabelsCleanupLabelsproof
Synthesis of debugging informationLinear to LinearDebugvarDebugvarproof
Laying out the activation recordsLinear to MachStacking
+ Bounds
+ Stacklayout		Stackingproof
+ Separation
Reconstruction of basic-blocks at Mach levelMach to MachblockMachblockgenForwardSimulationBlock
+ Machblockgenproof
Emission of purely sequential assembly codeMachblock to AsmblockAsmblockgenAsmblockgenproof0
+ Asmblockgenproof1
+ Asmblockgenproof
Bundling (and basic-block scheduling)Asmblock to AsmvliwPostpassScheduling using
+ Asmblockdeps and the abstractbb library		PostpassSchedulingproof
Flattening bundles (only a bureaucratic operation)Asmvliw to AsmAsmgenAsmgenproof
+ +

All together

+ + + +

Static analyses

+ +The following static analyses are performed over the RTL intermediate +representation to support optimizations such as constant propagation, +CSE, and dead code elimination. + + +

Type systems

+ +The type system of CompCert C is fully formalized. For some intermediate languages of the back-end, simpler type systems are used to statically capture well-formedness conditions. + + +
+
Xavier.Leroy@inria.fr
+
+ + + -- cgit From 7cfc487a56aca2c1444e98a0b845ec25c9069476 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 5 Sep 2019 14:08:49 +0200 Subject: (#157) Fixing warning for desactivated afaddd builtin. No implementation yet --- runtime/include/ccomp_k1c_fixes.h | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/runtime/include/ccomp_k1c_fixes.h b/runtime/include/ccomp_k1c_fixes.h index 5c543d8f..718ac3e5 100644 --- a/runtime/include/ccomp_k1c_fixes.h +++ b/runtime/include/ccomp_k1c_fixes.h @@ -17,6 +17,12 @@ extern __int128 __compcert_acswapd(void *address, unsigned long long new_value, #define __builtin_k1_acswapw __compcert_acswapw extern __int128 __compcert_acswapw(void *address, unsigned long long new_value, unsigned long long old_value); + +#define __builtin_k1_afaddd __compcert_afaddd +extern long long __compcert_afaddd(void *address, unsigned long long incr); + +#define __builtin_k1_afaddw __compcert_afaddw +extern int __compcert_afaddw(void *address, unsigned int incr); #endif #define __builtin_expect(x, y) (x) -- cgit From 2e1ecb87d05d7a6b5921be04ba10f6b9eae1be9c Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 5 Sep 2019 14:10:45 +0200 Subject: Adding tests for cmoved --- test/mppa/instr/i32.c | 48 ++++++++++++++++++++++++++++++++++++++++++++++++ test/mppa/instr/i64.c | 37 +++++++++++++++++++++++++++++++++++++ 2 files changed, 85 insertions(+) diff --git a/test/mppa/instr/i32.c b/test/mppa/instr/i32.c index 4e389620..e350931c 100644 --- a/test/mppa/instr/i32.c +++ b/test/mppa/instr/i32.c @@ -28,6 +28,7 @@ BEGIN_TEST(int) c = a+b; c += a&b; + /* testing if, cb version */ if ((a & 0x1) == 1) c += fact(1); else @@ -38,6 +39,11 @@ BEGIN_TEST(int) else c += fact(8); + if (a & 0x1 == 0) + c += fact(4); + else + c += fact(8); + b = !(a & 0x01); if (!b) c += fact(16); @@ -67,6 +73,48 @@ BEGIN_TEST(int) else c += fact(8192); + /* cmoved version */ + if ((a & 0x1) == 1) + c += 1; + else + c += 2; + + if (a & 0x1 == 0) + c += 4; + else + c += 8; + + if (a & 0x1 == 0) + c += 4; + else + c += 8; + + b = !(a & 0x01); + if (!b) + c += 16; + else + c += 32; + + if (0 > (a & 0x1) - 1) + c += 64; + else + c += 128; + + if (0 >= (a & 0x1)) + c += 256; + else + c += 512; + + if ((a & 0x1) > 0) + c += 1024; + else + c += 2048; + + if ((a & 0x1) - 1 >= 0) + c += 4096; + else + c += 8192; + c += ((a & 0x1) == (b & 0x1)); c += (a > b); c += (a <= b); diff --git a/test/mppa/instr/i64.c b/test/mppa/instr/i64.c index dc5fa6ee..b1fce564 100644 --- a/test/mppa/instr/i64.c +++ b/test/mppa/instr/i64.c @@ -74,6 +74,7 @@ BEGIN_TEST(long long) c += a^b; c += (unsigned int) a; + /* Testing if, cb */ if (0 != (a & 0x1LL)) c += fact(1); else @@ -109,6 +110,42 @@ BEGIN_TEST(long long) else c += fact(2048); + /* Testing if, cmoved */ + if (0 != (a & 0x1LL)) + c += 1; + else + c += 2; + + if (0 > (a & 0x1LL)) + c += 4; + else + c += 8; + + if (0 >= (a & 0x1LL) - 1) + c += 16; + else + c += 32; + + if (a-41414141 > 0) + c += 13; + else + c += 31; + + if (a & 0x1LL > 0) + c += 64; + else + c += 128; + + if ((a & 0x1LL) - 1 >= 0) + c += 256; + else + c += 512; + + if (0 == (a & 0x1LL)) + c += 1024; + else + c += 2048; + c += ((a & 0x1LL) == (b & 0x1LL)); c += (a >= b); c += (a > b); -- cgit From 5a095e968ca040757db22a4bd7cde34b91bf44e1 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 5 Sep 2019 14:25:21 +0200 Subject: Removing unused .all, .any, .nall and .none conditions --- mppa_k1c/Asmvliw.v | 13 ------------- mppa_k1c/TargetPrinter.ml | 4 ---- test/mppa/coverage_helper.py | 2 +- 3 files changed, 1 insertion(+), 18 deletions(-) diff --git a/mppa_k1c/Asmvliw.v b/mppa_k1c/Asmvliw.v index 54654abb..54e9c847 100644 --- a/mppa_k1c/Asmvliw.v +++ b/mppa_k1c/Asmvliw.v @@ -203,11 +203,6 @@ Inductive itest: Type := | ITgeu (**r Greater Than or Equal Unsigned *) | ITleu (**r Less Than or Equal Unsigned *) | ITgtu (**r Greater Than Unsigned *) - (* Not used yet *) - | ITall (**r All Bits Set in Mask *) - | ITnall (**r Not All Bits Set in Mask *) - | ITany (**r Any Bits Set in Mask *) - | ITnone (**r Not Any Bits Set in Mask *) . Inductive ftest: Type := @@ -909,10 +904,6 @@ Definition compare_int (t: itest) (v1 v2: val): val := | ITgeu => Val_cmpu Cge v1 v2 | ITleu => Val_cmpu Cle v1 v2 | ITgtu => Val_cmpu Cgt v1 v2 - | ITall - | ITnall - | ITany - | ITnone => Vundef end. Definition compare_long (t: itest) (v1 v2: val): val := @@ -929,10 +920,6 @@ Definition compare_long (t: itest) (v1 v2: val): val := | ITgeu => Some (Val_cmplu Cge v1 v2) | ITleu => Some (Val_cmplu Cle v1 v2) | ITgtu => Some (Val_cmplu Cgt v1 v2) - | ITall - | ITnall - | ITany - | ITnone => Some Vundef end in match res with | Some v => v diff --git a/mppa_k1c/TargetPrinter.ml b/mppa_k1c/TargetPrinter.ml index 5618875f..0c179a07 100644 --- a/mppa_k1c/TargetPrinter.ml +++ b/mppa_k1c/TargetPrinter.ml @@ -262,10 +262,6 @@ module Target (*: TARGET*) = | ITgeu -> "geu" | ITleu -> "leu" | ITgtu -> "gtu" - | ITall -> "all" - | ITnall -> "nall" - | ITany -> "any" - | ITnone -> "none" let icond oc c = fprintf oc "%s" (icond_name c) diff --git a/test/mppa/coverage_helper.py b/test/mppa/coverage_helper.py index cf7a84c9..e5b1907c 100644 --- a/test/mppa/coverage_helper.py +++ b/test/mppa/coverage_helper.py @@ -5,7 +5,7 @@ all_loads_stores = "lbs lbz lhz lo lq ld lhs lws sb sd sh so sq sw".split(" ") all_bconds = "wnez weqz wltz wgez wlez wgtz dnez deqz dltz dgez dlez dgtz".split(" ") -all_iconds = "ne eq lt ge le gt ltu geu leu gtu all nall any none".split(" ") +all_iconds = "ne eq lt ge le gt ltu geu leu gtu".split(" ") all_fconds = "one ueq oeq une olt uge oge ult".split(" ") -- cgit From 8caa5a2e1f825b6e3d6b87e294c1a53c65d62612 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Thu, 5 Sep 2019 14:29:19 +0200 Subject: Test for compd.geu --- test/mppa/instr/i64.c | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/test/mppa/instr/i64.c b/test/mppa/instr/i64.c index b1fce564..e869d93c 100644 --- a/test/mppa/instr/i64.c +++ b/test/mppa/instr/i64.c @@ -90,6 +90,12 @@ BEGIN_TEST(long long) else c += fact(32); + if ((unsigned long long)(a & 0x1LL) >= 1) + c += fact(18); + else + c += fact(31); + + if (a-41414141 > 0) c += fact(13); else -- cgit From 5b6c019a507688dfcf63b9ef54f7731137422ab5 Mon Sep 17 00:00:00 2001 From: Cyril SIX Date: Tue, 10 Sep 2019 17:50:42 +0200 Subject: Starting to modify official CompCert tests to be passable with the simu --- test/c/Makefile | 23 +++++++++++------ test/c/Results/binarytrees | 12 ++++----- test/c/Results/fannkuch | 62 +++++++++++++++++++++++----------------------- test/c/Results/fft | 2 +- test/c/Results/fftsp | 2 +- test/c/Results/fib | 2 +- test/c/Results/integr | 2 +- test/c/Results/knucleotide | 27 -------------------- test/c/binarytrees.c | 4 ++- test/c/fannkuch.c | 6 ++++- test/c/fft.c | 5 +++- test/c/fftsp.c | 2 +- test/c/fftw.c | 2 +- test/c/fib.c | 4 --- test/c/integr.c | 2 +- test/c/knucleotide.c | 6 +++++ test/c/lists.c | 5 +++- test/c/qsort.c | 2 +- 18 files changed, 81 insertions(+), 89 deletions(-) diff --git a/test/c/Makefile b/test/c/Makefile index 14c856ff..9580c8cc 100644 --- a/test/c/Makefile +++ b/test/c/Makefile @@ -3,18 +3,22 @@ include ../../Makefile.config CCOMP=../../ccomp CCOMPFLAGS=$(CCOMPOPTS) -stdlib ../../runtime -dc -dclight -dasm -CFLAGS+=-O1 -Wall +CFLAGS+=-O2 -Wall +EXECUTE:=timeout --signal=SIGTERM 90s $(EXECUTE) LIBS=$(LIBMATH) #TIME=xtime -o /dev/null -mintime 2.0 # Xavier's hack TIME=time >/dev/null # Otherwise -PROGS?=fib qsort fftw sha1 sha3 aes \ - lists binarytrees fannkuch \ - nsieve nsievebits vmach \ - chomp perlin siphash24\ - integr fft fftsp almabench knucleotide mandelbrot nbody spectral bisect +PROGS?=fib integr qsort fft fftsp fftw sha1 sha3 aes almabench \ + lists binarytrees fannkuch mandelbrot nbody \ + nsieve nsievebits spectral vmach \ + bisect chomp perlin siphash24 + +# Kalray NOTE : removed knucleotide from PROGS, it is hard to edit the input +# to modify its size without resulting in a seg fault, and the base input +# takes a too long time to complete in the simulator. all: $(PROGS:%=%.compcert) @@ -33,7 +37,8 @@ all_gcc: $(PROGS:%=%.gcc) test: all @for i in $(PROGS); do \ - if $(EXECUTE) ./$$i.compcert | cmp -s - Results/$$i; \ + $(EXECUTE) ./$$i.compcert > $$i.compcert.out;\ + if cmp -s $$i.compcert.out Results/$$i; \ then echo "$$i: passed"; \ else echo "$$i: FAILED"; exit 2; \ fi; \ @@ -41,7 +46,8 @@ test: all test_gcc: all_gcc @for i in $(PROGS); do \ - if $(EXECUTE) ./$$i.gcc | cmp -s - Results/$$i; \ + $(EXECUTE) ./$$i.gcc > $$i.gcc.out;\ + if cmp -s $$i.gcc.out Results/$$i; \ then echo "$$i: passed"; \ else echo "$$i: FAILED"; \ fi; \ @@ -60,3 +66,4 @@ bench: all clean: rm -f *.compcert *.gcc rm -f *.compcert.c *.light.c *.parsed.c *.s *.o *.sdump *~ + rm -f *.out diff --git a/test/c/Results/binarytrees b/test/c/Results/binarytrees index 9dfe1355..db0f0ef7 100644 --- a/test/c/Results/binarytrees +++ b/test/c/Results/binarytrees @@ -1,7 +1,5 @@ -stretch tree of depth 13 check: -1 -8192 trees of depth 4 check: -8192 -2048 trees of depth 6 check: -2048 -512 trees of depth 8 check: -512 -128 trees of depth 10 check: -128 -32 trees of depth 12 check: -32 -long lived tree of depth 12 check: -1 +stretch tree of depth 9 check: -1 +512 trees of depth 4 check: -512 +128 trees of depth 6 check: -128 +32 trees of depth 8 check: -32 +long lived tree of depth 8 check: -1 diff --git a/test/c/Results/fannkuch b/test/c/Results/fannkuch index be1815d4..dac06137 100644 --- a/test/c/Results/fannkuch +++ b/test/c/Results/fannkuch @@ -1,31 +1,31 @@ -12345678910 -21345678910 -23145678910 -32145678910 -31245678910 -13245678910 -23415678910 -32415678910 -34215678910 -43215678910 -42315678910 -24315678910 -34125678910 -43125678910 -41325678910 -14325678910 -13425678910 -31425678910 -41235678910 -14235678910 -12435678910 -21435678910 -24135678910 -42135678910 -23451678910 -32451678910 -34251678910 -43251678910 -42351678910 -24351678910 -Pfannkuchen(10) = 38 +12345678 +21345678 +23145678 +32145678 +31245678 +13245678 +23415678 +32415678 +34215678 +43215678 +42315678 +24315678 +34125678 +43125678 +41325678 +14325678 +13425678 +31425678 +41235678 +14235678 +12435678 +21435678 +24135678 +42135678 +23451678 +32451678 +34251678 +43251678 +42351678 +24351678 +Pfannkuchen(8) = 22 diff --git a/test/c/Results/fft b/test/c/Results/fft index a48608b0..cbeb0999 100644 --- a/test/c/Results/fft +++ b/test/c/Results/fft @@ -1 +1 @@ -262144 points, result OK +4096 points, result OK diff --git a/test/c/Results/fftsp b/test/c/Results/fftsp index cbeb0999..36264416 100644 --- a/test/c/Results/fftsp +++ b/test/c/Results/fftsp @@ -1 +1 @@ -4096 points, result OK +64 points, result OK diff --git a/test/c/Results/fib b/test/c/Results/fib index 84ce6474..d8beea8c 100644 --- a/test/c/Results/fib +++ b/test/c/Results/fib @@ -1 +1 @@ -fib(35) = 14930352 +fib(26) = 196418 diff --git a/test/c/Results/integr b/test/c/Results/integr index 973806c9..bb755482 100644 --- a/test/c/Results/integr +++ b/test/c/Results/integr @@ -1 +1 @@ -integr(square, 0.0, 1.0, 10000000) = 0.333333 +integr(square, 0.0, 1.0, 1000000) = 0.333333 diff --git a/test/c/Results/knucleotide b/test/c/Results/knucleotide index d13ae7dc..e69de29b 100644 --- a/test/c/Results/knucleotide +++ b/test/c/Results/knucleotide @@ -1,27 +0,0 @@ -A 30.284 -T 29.796 -C 20.312 -G 19.608 - -AA 9.212 -AT 8.950 -TT 8.948 -TA 8.936 -CA 6.166 -CT 6.100 -AC 6.086 -TC 6.042 -AG 6.036 -GA 5.968 -TG 5.868 -GT 5.798 -CC 4.140 -GC 4.044 -CG 3.906 -GG 3.798 - -562 GGT -152 GGTA -15 GGTATT -0 GGTATTTTAATT -0 GGTATTTTAATTTATAGT diff --git a/test/c/binarytrees.c b/test/c/binarytrees.c index b4b10232..f2921d9a 100644 --- a/test/c/binarytrees.c +++ b/test/c/binarytrees.c @@ -7,6 +7,7 @@ icc -O3 -ip -unroll -static binary-trees.c -lm */ +#include #include #include #include @@ -24,6 +25,7 @@ treeNode* NewTreeNode(treeNode* left, treeNode* right, long item) treeNode* new; new = (treeNode*)malloc(sizeof(treeNode)); + assert(new != NULL && "NewTreeNode: new malloc failed"); new->left = left; new->right = right; @@ -73,7 +75,7 @@ int main(int argc, char* argv[]) unsigned N, depth, minDepth, maxDepth, stretchDepth; treeNode *stretchTree, *longLivedTree, *tempTree; - N = argc < 2 ? 12 : atol(argv[1]); + N = argc < 2 ? 8 : atol(argv[1]); minDepth = 4; diff --git a/test/c/fannkuch.c b/test/c/fannkuch.c index 9cc7a693..ddaa7309 100644 --- a/test/c/fannkuch.c +++ b/test/c/fannkuch.c @@ -8,6 +8,7 @@ * $Id: fannkuch-gcc.code,v 1.33 2006/02/25 16:38:58 igouy-guest Exp $ */ +#include #include #include @@ -31,8 +32,11 @@ fannkuch( int n ) if( n < 1 ) return 0; perm = calloc(n, sizeof(*perm )); + assert(perm != NULL && "fannkuch: perm malloc failed"); perm1 = calloc(n, sizeof(*perm1)); + assert(perm != NULL && "fannkuch: perm1 malloc failed"); count = calloc(n, sizeof(*count)); + assert(perm != NULL && "fannkuch: count malloc failed"); for( i=0 ; i1) ? atoi(argv[1]) : 10; + int n = (argc>1) ? atoi(argv[1]) : 8; printf("Pfannkuchen(%d) = %ld\n", n, fannkuch(n)); return 0; diff --git a/test/c/fft.c b/test/c/fft.c index 2bd55a18..f91f5300 100644 --- a/test/c/fft.c +++ b/test/c/fft.c @@ -3,6 +3,7 @@ by: Dave Edelblute, edelblut@cod.nosc.mil, 05 Jan 1993 */ +#include #include #include #include @@ -151,13 +152,15 @@ int main(int argc, char ** argv) double enp, t, y, z, zr, zi, zm, a; double * xr, * xi, * pxr, * pxi; - if (argc >= 2) n = atoi(argv[1]); else n = 18; + if (argc >= 2) n = atoi(argv[1]); else n = 12; np = 1 << n; enp = np; npm = np / 2 - 1; t = PI / enp; xr = calloc(np, sizeof(double)); + assert(xr != NULL && "xr calloc failed"); xi = calloc(np, sizeof(double)); + assert(xi != NULL && "xi calloc failed"); pxr = xr; pxi = xi; for (nruns = 0; nruns < NRUNS; nruns++) { diff --git a/test/c/fftsp.c b/test/c/fftsp.c index 26b18b62..316ef714 100644 --- a/test/c/fftsp.c +++ b/test/c/fftsp.c @@ -153,7 +153,7 @@ int main(int argc, char ** argv) float enp, t, y, z, zr, zi, zm, a; float * xr, * xi, * pxr, * pxi; - if (argc >= 2) n = atoi(argv[1]); else n = 12; + if (argc >= 2) n = atoi(argv[1]); else n = 6; np = 1 << n; enp = np; npm = np / 2 - 1; diff --git a/test/c/fftw.c b/test/c/fftw.c index 913091d9..1d5b6526 100644 --- a/test/c/fftw.c +++ b/test/c/fftw.c @@ -74,7 +74,7 @@ const E KP1_847759065 = ((E) +1.847759065022573512256366378793576573644833252); /* Test harness */ -#define NRUNS (100 * 1000) +#define NRUNS (100 * 10) int main() { diff --git a/test/c/fib.c b/test/c/fib.c index 19548415..77aa7bb9 100644 --- a/test/c/fib.c +++ b/test/c/fib.c @@ -12,11 +12,7 @@ int fib(int n) int main(int argc, char ** argv) { int n, r; -#ifdef __K1C_COS__ if (argc >= 2) n = atoi(argv[1]); else n = 26; -#else - if (argc >= 2) n = atoi(argv[1]); else n = 35; -#endif r = fib(n); printf("fib(%d) = %d\n", n, r); return 0; diff --git a/test/c/integr.c b/test/c/integr.c index 882325c3..9c762297 100644 --- a/test/c/integr.c +++ b/test/c/integr.c @@ -25,7 +25,7 @@ double test(int n) int main(int argc, char ** argv) { int n; double r; - if (argc >= 2) n = atoi(argv[1]); else n = 10000000; + if (argc >= 2) n = atoi(argv[1]); else n = 1000000; r = test(n); printf("integr(square, 0.0, 1.0, %d) = %g\n", n, r); return 0; diff --git a/test/c/knucleotide.c b/test/c/knucleotide.c index 3ac469be..1982834e 100644 --- a/test/c/knucleotide.c +++ b/test/c/knucleotide.c @@ -8,6 +8,7 @@ http://cvs.alioth.debian.org/cgi-bin/cvsweb.cgi/shootout/bench/Include/?cvsroot=shootout */ +#include #include #include #include @@ -76,9 +77,11 @@ struct ht_node *ht_node_create(char *key) { struct ht_ht *ht_create(int size) { int i = 0; struct ht_ht *ht = (struct ht_ht *)malloc(sizeof(struct ht_ht)); + assert (ht != NULL && "ht_create: ht malloc failed"); while (ht_prime_list[i] < size) { i++; } ht->size = ht_prime_list[i]; ht->tbl = (struct ht_node **)calloc(ht->size, sizeof(struct ht_node *)); + assert (ht->tbl != NULL && "ht_create: ht->tbl calloc failed"); ht->iter_index = 0; ht->iter_next = 0; ht->items = 0; @@ -250,6 +253,7 @@ write_frequencies (int fl, char *buffer, long buflen) size++; } s = calloc (size, sizeof (sorter)); + assert(s != NULL && "write_frequencies: s alloc failed"); i = 0; for (nd = ht_first (ht); nd != NULL; nd = ht_next (ht)) { @@ -293,6 +297,7 @@ main () FILE * f; line = malloc (256); + assert (line != NULL && "line alloc failed"); if (!line) return 2; seqlen = 0; @@ -308,6 +313,7 @@ main () buflen = 10240; buffer = malloc (buflen + 1); + assert (buffer != NULL && "buffer alloc failed"); if (!buffer) return 2; x = buffer; diff --git a/test/c/lists.c b/test/c/lists.c index ced384c0..d1c67954 100644 --- a/test/c/lists.c +++ b/test/c/lists.c @@ -1,5 +1,6 @@ /* List manipulations */ +#include #include #include #include @@ -11,6 +12,7 @@ struct list * buildlist(int n) struct list * r; if (n < 0) return NULL; r = malloc(sizeof(struct list)); + assert(r != NULL && "buildlist: r malloc failed"); r->hd = n; r->tl = buildlist(n - 1); return r; @@ -21,6 +23,7 @@ struct list * reverselist (struct list * l) struct list * r, * r2; for (r = NULL; l != NULL; l = l->tl) { r2 = malloc(sizeof(struct list)); + assert(r2 != NULL && "reverselist: r2 malloc failed"); r2->hd = l->hd; r2->tl = r; r = r2; @@ -58,7 +61,7 @@ int main(int argc, char ** argv) int n, niter, i; struct list * l; - if (argc >= 2) n = atoi(argv[1]); else n = 1000; + if (argc >= 2) n = atoi(argv[1]); else n = 100; if (argc >= 3) niter = atoi(argv[1]); else niter = 20000; l = buildlist(n); if (checklist(n, reverselist(l))) { diff --git a/test/c/qsort.c b/test/c/qsort.c index 66eef68d..a9d5757a 100644 --- a/test/c/qsort.c +++ b/test/c/qsort.c @@ -34,7 +34,7 @@ int main(int argc, char ** argv) int n, i, j; int * a, * b; - if (argc >= 2) n = atoi(argv[1]); else n = 100000; + if (argc >= 2) n = atoi(argv[1]); else n = 10000; a = malloc(n * sizeof(int)); b = malloc(n * sizeof(int)); for (j = 0; j < NITER; j++) { -- cgit