Mercurial > hg > CbC > old > akasha

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cbmc/insert_verification/cbmcCS.c	Mon Jun 13 01:35:37 2016 +0000
@@ -0,0 +1,26 @@
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <stdbool.h>
+
+#include "cbmcLLRBContext.h"
+
+extern void initLLRBContext(struct Context* context, enum Code next);
+
+void meta(struct Context* context, enum Code next) {
+    context->prev = next;
+    return (context->code[next])(context);
+}
+
+void startCode(enum Code next) {
+    struct Context* context = (struct Context*)malloc(sizeof(struct Context));
+
+    return initLLRBContext(context, next);
+}
+
+void exitCode(struct Context* context) {
+    free(context->code);
+    free(context->data);
+    free(context->heapStart);
+    exit(0);
+}
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cbmc/insert_verification/cbmcLLRBContext.c	Mon Jun 13 01:35:37 2016 +0000
@@ -0,0 +1,101 @@
+#include <stdlib.h>
+#include <string.h>
+
+#include "cbmcLLRBContext.h"
+
+/* for CBMC */
+extern void verifySpecification_stub(struct Context*);
+
+/* definitions from llrb */
+extern void meta(struct Context*, enum Code next);
+extern void put_stub(struct Context*);
+extern void replaceNode_stub(struct Context*);
+extern void insertNode_stub(struct Context*);
+extern void rotateLeft_stub(struct Context*);
+extern void rotateRight_stub(struct Context*);
+extern void colorFlip_stub(struct Context*);
+extern void fixUp_stub(struct Context*);
+extern void changeReference_stub(struct Context*);
+extern void insert1_stub(struct Context*);
+extern void insert2_stub(struct Context*);
+extern void insert3_stub(struct Context*);
+extern void insert4_stub(struct Context*);
+extern void insert4_1_stub(struct Context*);
+extern void insert4_2_stub(struct Context*);
+extern void insert5_stub(struct Context*);
+extern void stackClear_stub(struct Context*);
+extern void get_stub(struct Context*);
+extern void search_stub(struct Context*);
+extern void delete_stub(struct Context*);
+extern void delete1_stub(struct Context*);
+extern void delete2_stub(struct Context*);
+extern void delete3_stub(struct Context*);
+extern void replaceNodeForDelete1_stub(struct Context*);
+extern void replaceNodeForDelete2_stub(struct Context*);
+extern void findMax1_stub(struct Context*);
+extern void findMax2_stub(struct Context*);
+extern void deleteCase1_stub(struct Context*);
+extern void deleteCase2_stub(struct Context*);
+extern void deleteCase3_stub(struct Context*);
+extern void deleteCase4_stub(struct Context*);
+extern void deleteCase5_stub(struct Context*);
+extern void deleteCase6_stub(struct Context*);
+extern void exitCode(struct Context*);
+
+/* for allocator */
+extern void allocator(struct Context* context);
+
+
+void initLLRBContext(struct Context* context, enum Code next) {
+    context->codeNum   = Exit;
+
+    context->heapLimit = sizeof(union Data)*ALLOCATE_SIZE;
+    context->code      = malloc(sizeof(void*)*(context->codeNum+1));
+    context->data      = malloc(sizeof(union Data*)*ALLOCATE_SIZE);
+    context->heapStart = malloc(context->heapLimit);
+    memset(context->heapStart, 0, context->heapLimit);
+
+    context->code[VerifySpecification] = verifySpecification_stub;
+
+    /* definitions from llrb */
+    context->code[Put]           = put_stub;
+    context->code[Replace]       = replaceNode_stub;
+    context->code[Insert]        = insertNode_stub;
+    context->code[RotateL]       = rotateLeft_stub;
+    context->code[RotateR]       = rotateRight_stub;
+    context->code[InsertCase1]   = insert1_stub;
+    context->code[InsertCase2]   = insert2_stub;
+    context->code[InsertCase3]   = insert3_stub;
+    context->code[InsertCase4]   = insert4_stub;
+    context->code[InsertCase4_1] = insert4_1_stub;
+    context->code[InsertCase4_2] = insert4_2_stub;
+    context->code[InsertCase5]   = insert5_stub;
+    context->code[StackClear]    = stackClear_stub;
+    context->code[Exit]          = exitCode;
+
+    context->heap = context->heapStart;
+
+    context->data[Allocate] = context->heap;
+    context->heap += sizeof(struct Allocate);
+
+    context->data[Tree] = context->heap;
+    context->heap += sizeof(struct Tree);
+
+    context->data[Node] = context->heap;
+    context->heap += sizeof(struct Node);
+
+    context->dataNum = Node;
+
+    struct Tree* tree = &context->data[Tree]->tree;
+    tree->root = 0;
+    tree->current = 0;
+    tree->deleted = 0;
+
+    context->node_stack = stack_init(sizeof(struct Node*), 1000);
+    context->code_stack = stack_init(sizeof(enum Code), 1000);
+
+    context->loopCount = 0;
+
+    return meta(context, next);
+}
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cbmc/insert_verification/include/cbmcCS.h	Mon Jun 13 01:35:37 2016 +0000
@@ -0,0 +1,3 @@
+extern void startCode(enum Code next);
+extern void exitCode(struct Context* context);
+extern void meta(struct Context* context, enum Code next);
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cbmc/insert_verification/include/cbmcLLRBContext.h	Mon Jun 13 01:35:37 2016 +0000
@@ -0,0 +1,108 @@
+/* Context definition for llrb example */
+#include "stack.h"
+
+#define ALLOCATE_SIZE 20000000
+#define LIMIT_OF_VERIFICATION_SIZE 5
+
+enum Code {
+    /* for CBMC */
+    VerifySpecification,
+
+    /* definitions from llrb */
+    Allocator,
+    Put,
+    Replace,
+    Insert,
+    Compare,
+    RotateL,
+    RotateR,
+    SetTree,
+    InsertCase1,
+    InsertCase2,
+    InsertCase3,
+    InsertCase4,
+    InsertCase4_1,
+    InsertCase4_2,
+    InsertCase5,
+    StackClear,
+    Get,
+    Search,
+    Delete,
+    Delete1,
+    Delete2,
+    Delete3,
+    Replace_d1,
+    Replace_d2,
+    FindMax1,
+    FindMax2,
+    DeleteCase1,
+    DeleteCase2,
+    DeleteCase3,
+    DeleteCase4,
+    DeleteCase5,
+    DeleteCase6,
+    Exit,
+};
+
+enum Relational {
+    EQ,
+    GT,
+    LT,
+};
+
+enum UniqueData {
+    Allocate,
+    Tree,
+    Node,
+};
+
+struct Context {
+    enum Code next;
+    enum Code prev;
+    unsigned int codeNum;
+    void (**code) (struct Context*);
+    void* heapStart;
+    void* heap;
+    unsigned long heapLimit;
+    unsigned long dataNum;
+    stack_ptr code_stack;
+    stack_ptr node_stack;
+    union Data **data;
+
+    unsigned int loopCount;
+};
+
+union Data {
+    struct Comparable { // inteface
+        enum Code compare;
+        union Data* data;
+    } compare;
+    struct Count {
+        enum Code next;
+        long i;
+    } count;
+    struct Tree {
+        enum Code next;
+        struct Node* root;
+        struct Node* current;
+        struct Node* deleted;
+        int result;
+    } tree;
+    struct Node {
+        // need to tree
+        enum Code next;
+        int key; // comparable data segment
+        int value;
+        struct Node* left;
+        struct Node* right;
+        // need to balancing
+        enum Color {
+            Red,
+            Black,
+        } color;
+    } node;
+    struct Allocate {
+        enum Code next;
+        long size;
+    } allocate;
+};
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cbmc/insert_verification/include/llrbContext.h	Mon Jun 13 01:35:37 2016 +0000
@@ -0,0 +1,1 @@
+#include "cbmcLLRBContext.h"
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/cbmc/insert_verification/include/origin_cs.h	Mon Jun 13 01:35:37 2016 +0000
@@ -0,0 +1,1 @@
+#include "cbmcCS.h"
--- a/cbmc/insert_verification/insert_verification.sh	Mon Jun 13 01:34:43 2016 +0000
+++ b/cbmc/insert_verification/insert_verification.sh	Mon Jun 13 01:35:37 2016 +0000
@@ -14,6 +14,7 @@
     sed -i -e 's/__code/void/g' $filename
 }

+rm -rf ${CBMC_FILE_DIR}

 copy_and_substitute ${LLRB_PATH}/allocate.c ${CBMC_FILE_DIR}
 copy_and_substitute ${LLRB_PATH}/llrb.c     ${CBMC_FILE_DIR}
@@ -22,13 +23,5 @@

 copy_and_substitute ${LLRB_PATH}/include/stack.h       ${CBMC_INCLUDE_DIR}

-copy_and_substitute ${GEARS_PATH}/src/include/origin_cs.h      ${CBMC_INCLUDE_DIR}
-
-
-#main.c
-#akashaCS.c
-#akashaLLRBContext.c
-#verifySpecification.c
-
-
 cbmc --unwind 50 -I ${CBMC_INCLUDE_DIR} -I include cbmc_files/*.c *.c
+#/bin/clang -Wall -O0 -g -I ${CBMC_INCLUDE_DIR} -I include cbmc_files/*.c *.c
--- a/cbmc/insert_verification/main.c	Mon Jun 13 01:34:43 2016 +0000
+++ b/cbmc/insert_verification/main.c	Mon Jun 13 01:35:37 2016 +0000
@@ -1,25 +1,43 @@
 #include <stdio.h>
+#include <assert.h>

 #include "cbmcLLRBContext.h"

+void meta(struct Context*, enum Code);
+
 /* cbmc built in functions */
-int nondet_int();
+int nondet_int() { return 9 ;}

-void verifySpecification_stub(struct Context* context) {
-    verifySpecification(context);
+// TODO c functions
+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 verifySpecification(struct Context* context, struct Node* node) {
-    for (int i = 0; i < 10; i++) {
-        int hoge      = nodet_int();
-        node->key     = hoge;
-        node->value   = node->key;
-        context->next = VerifySpecification;
+    if (context->loopCount > LIMIT_OF_VERIFICATION_SIZE) {
+        return meta(context, Exit);
+    }
+    printTree(context->data[Tree]->tree.root, 0);
+    //assert(context->data[Tree]->tree.root->key == 0);

-        assert(&context->data[Tree]->tree.root->key == hoge);
-        meta(context, Put);
-    }
-    meta(context, Exit);
+    int hoge      = nondet_int();
+    node->key     = hoge;
+    node->value   = node->key;
+    context->next = VerifySpecification;
+    context->loopCount++;
+
+    return meta(context, Put);
+}
+
+void verifySpecification_stub(struct Context* context) {
+    return verifySpecification(context, &context->data[Node]->node);
 }