Skip to content

SMT2 formulation of pointer objects #431

Closed
@mm95

Description

@mm95

Hello,
I have a problem in logical formulation of programs with pointers via smt2 core of cbmc.
for example for below code

void ss2n(unsigned int s, unsigned char* c) {
   	c[0]=(unsigned char)(((s)>> 8)&0xff);
	c[1]=(unsigned char)(((s)    )&0xff);
        c += 2;
}


int main(){

unsigned char* s_1 =8;
*s_1 = '8';
ss2n(18, s_1);
assert(0);
return 1;
}

I have a function(ss2n) that gets a pointer and set some values in object related to this pointer.
I use cbmc 5.6 to get SMT2 formula and got below result (I erplaced define-fun with pair(declare-fun, assert))

(set-info :source "Generated by CBMC 5.6")
(set-option :produce-models true)
(set-logic QF_AUFBV)

(declare-fun |__CPROVER_dead_object#1| () (_ BitVec 64))
(assert (= |__CPROVER_dead_object#1| (_ bv0 64)))


(declare-fun |__CPROVER_deallocated#1| () (_ BitVec 64))
(assert (= |__CPROVER_deallocated#1| (_ bv0 64)))


(declare-fun |__CPROVER_malloc_is_new_array#1| () Bool)
(assert (= |__CPROVER_malloc_is_new_array#1| false))


(declare-fun |__CPROVER_malloc_object#1| () (_ BitVec 64))
(assert (= |__CPROVER_malloc_object#1| (_ bv0 64)))


(declare-fun |__CPROVER_malloc_size#1| () (_ BitVec 64))
(assert (= |__CPROVER_malloc_size#1| (_ bv0 64)))


(declare-fun |__CPROVER_memory_leak#1| () (_ BitVec 64))
(assert (= |__CPROVER_memory_leak#1| (_ bv0 64)))


(declare-fun |__CPROVER_next_thread_id#1| () (_ BitVec 64))
(assert (= |__CPROVER_next_thread_id#1| (_ bv0 64)))


(declare-fun |__CPROVER_pipe_count#1| () (_ BitVec 32))
(assert (= |__CPROVER_pipe_count#1| (_ bv0 32)))


(declare-fun |__CPROVER_rounding_mode!0#1| () (_ BitVec 32))
(assert (= |__CPROVER_rounding_mode!0#1| (_ bv0 32)))


(declare-fun |__CPROVER_thread_id!0#1| () (_ BitVec 64))
(assert (= |__CPROVER_thread_id!0#1| (_ bv0 64)))


(declare-fun array_of.0 () (Array (_ BitVec 64) (_ BitVec 1)))
(declare-fun |__CPROVER_threads_exited#1| () (Array (_ BitVec 64) (_ BitVec 1)))
(assert (= |__CPROVER_threads_exited#1| array_of.0))


(declare-fun |main::1::s_1!0@1#2| () (_ BitVec 64))
(assert (= |main::1::s_1!0@1#2| ((_ sign_extend 32) (_ bv8 32))))


(declare-fun |__CPROVER_memory#0| () (Array (_ BitVec 64) (_ BitVec 8)))
(declare-fun |__CPROVER_memory#1| () (Array (_ BitVec 64) (_ BitVec 8)))
(assert (= |__CPROVER_memory#1| (store |__CPROVER_memory#0| (_ bv8 64) (_ bv56 8))))


(declare-fun |ss2n::s!0@1#1| () (_ BitVec 32))
(assert (= |ss2n::s!0@1#1| (_ bv18 32)))


(declare-fun |ss2n::c!0@1#1| () (_ BitVec 64))
(assert (= |ss2n::c!0@1#1| ((_ sign_extend 32) (_ bv8 32))))


(declare-fun |__CPROVER_memory#2| () (Array (_ BitVec 64) (_ BitVec 8)))
(assert (= |__CPROVER_memory#2| (store |__CPROVER_memory#1| (_ bv8 64) (_ bv0 8))))


(declare-fun |__CPROVER_memory#3| () (Array (_ BitVec 64) (_ BitVec 8)))
(assert (= |__CPROVER_memory#3| (store |__CPROVER_memory#2| (_ bv9 64) (_ bv18 8))))


(declare-fun |ss2n::c!0@1#2| () (_ BitVec 64))
(assert (= |ss2n::c!0@1#2| (bvadd ((_ sign_extend 32) (_ bv8 32)) (_ bv2 64))))


(declare-fun |main::1::s_1!0@1#1| () (_ BitVec 64))
(declare-fun |B0| () Bool)
(assert (= |B0| (= |main::1::s_1!0@1#1| |main::1::s_1!0@1#1|)))

(check-sat)
...

Unfortunately, in smt2 formula generated via cbmc, I can not track the relation between objects and their pointers via pointers'name.In above formula, 2 bytes of object of 'c'(or in fact 's') are set but in formula, his is reflected as setting cprover_memory, however if I want to input this formula to an external solver, it is not understood automatically.
Is there any way to deal with this matter?

Thanks so much.

Metadata

Metadata

Assignees

No one assigned

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions