# HG changeset patch # User atton # Date 1465781737 0 # Node ID e27f4961281e16be0d54772d93ed4d28037c5c20 # Parent 9619480d0dc066f12aee99256efcf0337715c748 WIP: insert verification using cbmc (syntax valid) diff -r 9619480d0dc0 -r e27f4961281e cbmc/insert_verification/cbmcCS.c --- /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 +#include +#include +#include + +#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); +} diff -r 9619480d0dc0 -r e27f4961281e cbmc/insert_verification/cbmcLLRBContext.c --- /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 +#include + +#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); +} + diff -r 9619480d0dc0 -r e27f4961281e cbmc/insert_verification/include/cbmcCS.h --- /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); diff -r 9619480d0dc0 -r e27f4961281e cbmc/insert_verification/include/cbmcLLRBContext.h --- /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; +}; diff -r 9619480d0dc0 -r e27f4961281e cbmc/insert_verification/include/llrbContext.h --- /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" diff -r 9619480d0dc0 -r e27f4961281e cbmc/insert_verification/include/origin_cs.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" diff -r 9619480d0dc0 -r e27f4961281e cbmc/insert_verification/insert_verification.sh --- 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 diff -r 9619480d0dc0 -r e27f4961281e cbmc/insert_verification/main.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 +#include #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;ikey, 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); }