Mercurial > hg > CbC > old > akasha

changeset 31:d2073e23f206

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Split verification functions
author Yasutaka Higa <e115763@ie.u-ryukyu.ac.jp>
date Tue, 07 Jun 2016 14:39:07 +0900
parents 865c1b265e80
children be67b0312bea
files src/insert_verification/CMakeLists.txt src/insert_verification/include/akashaLLRBContext.h src/insert_verification/include/verifySpefication.h src/insert_verification/main.c src/insert_verification/verifySpecification.c
diffstat 5 files changed, 73 insertions(+), 69 deletions(-) [+]
line wrap: on
line diff
--- a/src/insert_verification/CMakeLists.txt	Tue May 24 17:07:21 2016 +0900
+++ b/src/insert_verification/CMakeLists.txt	Tue Jun 07 14:39:07 2016 +0900
@@ -11,6 +11,7 @@
                main.c
                akashaCS.c
                akashaLLRBContext.c
+               verifySpecification.c
 
                ${llrb_path}/allocate.c
                ${llrb_path}/llrb.c
--- a/src/insert_verification/include/akashaLLRBContext.h	Tue May 24 17:07:21 2016 +0900
+++ b/src/insert_verification/include/akashaLLRBContext.h	Tue Jun 07 14:39:07 2016 +0900
@@ -2,7 +2,7 @@
 #include "stack.h"
 
 #define ALLOCATE_SIZE 20000000
-#define LIMIT_OF_VERIFICATION_SIZE 12
+#define LIMIT_OF_VERIFICATION_SIZE 8
 
 enum Code {
     ShowTree,
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/insert_verification/include/verifySpefication.h	Tue Jun 07 14:39:07 2016 +0900
@@ -0,0 +1,2 @@
+extern __code verifySpecification(struct Context*, struct Tree*, struct Iterator*);
+extern __code showTrace(struct Iterator*);
--- a/src/insert_verification/main.c	Tue May 24 17:07:21 2016 +0900
+++ b/src/insert_verification/main.c	Tue Jun 07 14:39:07 2016 +0900
@@ -5,7 +5,6 @@
 #include "akashaCS.h"
 
 extern void allocator(struct Context* context);
-void showTrace(struct Iterator* iter); //FIXME
 
 void* akashaMalloc(struct Context* context, size_t size) {
     context->data[++context->dataNum] = context->heap;
@@ -46,58 +45,6 @@
     newTree->deleted = nodeDeepCopy(newContext, oldTree->deleted);
 }
 
-/* C functions (TODO: convert to code segment) */
-
-unsigned int min_height(struct Node* node, unsigned int height) {
-    if ((node->left == NULL) && (node->right == NULL)) return height;
-    if (node->left  == NULL) return min_height(node->right, height+1);
-    if (node->right == NULL) return min_height(node->left, height+1);
-
-    unsigned int left_min  = min_height(node->left, height+1);
-    unsigned int right_min = min_height(node->right, height+1);
-
-    if (left_min < right_min) {
-        return left_min;
-    } else {
-        return right_min;
-    }
-}
-
-unsigned int max_height(struct Node* node, unsigned int height) {
-    if ((node->left == NULL) && (node->right == NULL)) return height;
-    if (node->left  == NULL) return max_height(node->right, height+1);
-    if (node->right == NULL) return max_height(node->left, height+1);
-
-    unsigned int left_max  = max_height(node->left, height+1);
-    unsigned int right_max = max_height(node->right, height+1);
-
-    if (left_max > right_max) {
-        return left_max;
-    } else {
-        return right_max;
-    }
-}
-
-void printTree(struct Node* node, int n) {
-    if (node != 0) {
-        printTree(node->left, n+1);
-        for (int i=0;i<n;i++)
-            printf("  ");
-        printf("key=%d value=%d color=%s\t%p\n", node->key, node->value,/* n, */node->color==0? "R":"B", node);
-        printTree(node->right, n+1);
-    }
-}
-
-void showTrace(struct Iterator* iter) {
-    printf("show trace(reversed):");
-
-    for (; iter != NULL; iter = iter->previousDepth) {
-        printf("%u ", iter->iteratedValue);
-    }
-    printf("\n");
-}
-
-
 /* Code Segments */
 
 __code showTree_stub(struct Context* context) {
@@ -153,21 +100,6 @@
     goto verifySpecification(context, &context->data[Tree]->tree, &context->data[Iter]->iterator);
 }
 
-__code verifySpecification(struct Context* context, struct Tree* tree, struct Iterator* iter) {
-    unsigned const int min_h = min_height(tree->root, 1);
-    unsigned const int max_h = max_height(tree->root, 1);
-
-    if (max_h > 2*min_h) {
-        printf("llrb-condition violated.\n");
-        printf("\tmin-height %u\n", min_h);
-        printf("\tmax-height %u\n", max_h);
-        showTrace(iter);
-        exit(1);
-    }
-
-    goto meta(context, DuplicateIterator);
-}
-
 __code duplicateIterator_stub(struct Context* context) {
     goto duplicateIterator(context, &context->data[Allocate]->allocate, &context->data[Iter]->iterator);
 }
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/insert_verification/verifySpecification.c	Tue Jun 07 14:39:07 2016 +0900
@@ -0,0 +1,69 @@
+/* C functions (TODO: convert to code segment) */
+
+#include <stdio.h>
+#include "akashaLLRBContext.h"
+
+void showTrace(struct Iterator* iter) {
+    printf("show trace(reversed):");
+
+    for (; iter != NULL; iter = iter->previousDepth) {
+        printf("%u ", iter->iteratedValue);
+    }
+    printf("\n");
+}
+
+unsigned int min_height(struct Node* node, unsigned int height) {
+    if ((node->left == NULL) && (node->right == NULL)) return height;
+    if (node->left  == NULL) return min_height(node->right, height+1);
+    if (node->right == NULL) return min_height(node->left, height+1);
+
+    unsigned int left_min  = min_height(node->left, height+1);
+    unsigned int right_min = min_height(node->right, height+1);
+
+    if (left_min < right_min) {
+        return left_min;
+    } else {
+        return right_min;
+    }
+}
+
+unsigned int max_height(struct Node* node, unsigned int height) {
+    if ((node->left == NULL) && (node->right == NULL)) return height;
+    if (node->left  == NULL) return max_height(node->right, height+1);
+    if (node->right == NULL) return max_height(node->left, height+1);
+
+    unsigned int left_max  = max_height(node->left, height+1);
+    unsigned int right_max = max_height(node->right, height+1);
+
+    if (left_max > right_max) {
+        return left_max;
+    } else {
+        return right_max;
+    }
+}
+void printTree(struct Node* node, int n) {
+    if (node != 0) {
+        printTree(node->left, n+1);
+        for (int i=0;i<n;i++)
+            printf("  ");
+        printf("key=%d value=%d color=%s\t%p\n", node->key, node->value,/* n, */node->color==0? "R":"B", node);
+        printTree(node->right, n+1);
+    }
+}
+
+/* Code Segments */
+
+__code verifySpecification(struct Context* context, struct Tree* tree, struct Iterator* iter) {
+    unsigned const int min_h = min_height(tree->root, 1);
+    unsigned const int max_h = max_height(tree->root, 1);
+
+    if (max_h > 2*min_h) {
+        printf("llrb-condition violated.\n");
+        printf("\tmin-height %u\n", min_h);
+        printf("\tmax-height %u\n", max_h);
+        showTrace(iter);
+        exit(1);
+    }
+
+    goto meta(context, DuplicateIterator);
+}