cprover
Loading...
Searching...
No Matches
cprover_contracts.c
Go to the documentation of this file.
1
3
4/* FUNCTION: __CPROVER_contracts_library */
5
6#ifndef __CPROVER_contracts_library_defined
7#define __CPROVER_contracts_library_defined
8
9// external dependencies
12extern const void *__CPROVER_deallocated;
13const void *__CPROVER_new_object = 0;
14extern const void *__CPROVER_memory_leak;
16#if defined(_WIN32) && defined(_M_X64)
17int __builtin_clzll(unsigned long long);
18#else
19int __builtin_clzl(unsigned long);
20#endif
23
36
45
48
67
70
106
109
116{
119 ((ptr == 0) | __CPROVER_rw_ok(ptr, size)),
120 "ptr NULL or writable up to size");
123 "CAR size is less than __CPROVER_max_malloc_size");
126 !(offset > 0) | (offset + size <= __CPROVER_max_malloc_size),
127 "no offset bits overflow on CAR upper bound computation");
129 .is_writable = ptr != 0, .size = size, .lb = ptr, .ub = (char *)ptr + size};
130}
131
137 __CPROVER_size_t max_elems)
138{
140#ifdef DFCC_DEBUG
143 "set writable");
144#endif
145 set->max_elems = max_elems;
146 set->elems =
147 __CPROVER_allocate(max_elems * sizeof(__CPROVER_contracts_car_t), 1);
148}
149
159 void *ptr,
160 __CPROVER_size_t size)
161{
163#ifdef DFCC_DEBUG
164 __CPROVER_assert((set != 0) & (idx < set->max_elems), "no OOB access");
165#endif
167 ((ptr == 0) | __CPROVER_rw_ok(ptr, size)),
168 "ptr NULL or writable up to size");
171 "CAR size is less than __CPROVER_max_malloc_size");
174 !(offset > 0) | (offset + size <= __CPROVER_max_malloc_size),
175 "no offset bits overflow on CAR upper bound computation");
178 .is_writable = ptr != 0, .size = size, .lb = ptr, .ub = (char *)ptr + size};
179}
180
187 void *ptr)
188{
191 __CPROVER_size_t idx = set->max_elems;
194 while(idx != 0)
195 {
197 elem->is_writable = 0;
198 ++elem;
199 --idx;
200 }
201}
202
230
241{
243#ifdef DFCC_DEBUG
246 "set writable");
247#endif
248 // compute the maximum number of objects that can exist in the
249 // symex state from the number of object_bits/offset_bits
250 // the number of object bits is determined by counting the number of leading
251 // zeroes of the built-in constant __CPROVER_max_malloc_size;
252#if defined(_WIN32) && defined(_M_X64)
254 __CPROVER_size_t nof_objects = 1ULL << object_bits;
255#else
256 int object_bits = __builtin_clzl(__CPROVER_max_malloc_size);
257 __CPROVER_size_t nof_objects = 1UL << object_bits;
258#endif
261 .watermark = 0,
262 .nof_elems = 0,
263 .is_empty = 1,
264 .indexed_by_object_id = 1,
265 .elems = __CPROVER_allocate(nof_objects * sizeof(*(set->elems)), 1)};
266}
267
275 __CPROVER_size_t max_elems)
276{
278#ifdef DFCC_DEBUG
281 "set writable");
282#endif
284 .max_elems = max_elems,
285 .watermark = 0,
286 .nof_elems = 0,
287 .is_empty = 1,
288 .indexed_by_object_id = 0,
289 .elems = __CPROVER_allocate(max_elems * sizeof(*(set->elems)), 1)};
290}
291
294{
296#ifdef DFCC_DEBUG
299 "set readable");
300 __CPROVER_assert(__CPROVER_rw_ok(&(set->elems), 0), "set->elems writable");
301#endif
303}
304
311 void *ptr)
312{
315#ifdef DFCC_DEBUG
316 __CPROVER_assert(set->indexed_by_object_id, "indexed by object id");
317 __CPROVER_assert(object_id < set->max_elems, "no OOB access");
318#endif
319 set->nof_elems = set->elems[object_id] ? set->nof_elems : set->nof_elems + 1;
320 set->elems[object_id] = ptr;
321 set->is_empty = 0;
322}
323
330 void *ptr)
331{
333#ifdef DFCC_DEBUG
334 __CPROVER_assert(!(set->indexed_by_object_id), "not indexed by object id");
335 __CPROVER_assert(set->watermark < set->max_elems, "no OOB access");
336#endif
337 set->nof_elems = set->watermark;
338 set->elems[set->watermark] = ptr;
339 set->watermark += 1;
340 set->is_empty = 0;
341}
342
349 void *ptr)
350{
353#ifdef DFCC_DEBUG
354 __CPROVER_assert(set->indexed_by_object_id, "indexed by object id");
355 __CPROVER_assert(object_id < set->max_elems, "no OOB access");
356#endif
357 set->nof_elems = set->elems[object_id] ? set->nof_elems - 1 : set->nof_elems;
358 set->is_empty = set->nof_elems == 0;
359 set->elems[object_id] = 0;
360}
361
369 void *ptr)
370{
373#ifdef DFCC_DEBUG
374 __CPROVER_assert(set->indexed_by_object_id, "indexed by object id");
375 __CPROVER_assert(object_id < set->max_elems, "no OOB access");
376#endif
377 return set->elems[object_id] != 0;
378}
379
386 void *ptr)
387{
390#ifdef DFCC_DEBUG
391 __CPROVER_assert(set->indexed_by_object_id, "indexed by object id");
392 __CPROVER_assert(object_id < set->max_elems, "no OOB access");
393#endif
394 return set->elems[object_id] == ptr;
395}
396
417 __CPROVER_bool assume_requires_ctx,
418 __CPROVER_bool assert_requires_ctx,
419 __CPROVER_bool assume_ensures_ctx,
420 __CPROVER_bool assert_ensures_ctx,
421 __CPROVER_bool allow_allocate,
422 __CPROVER_bool allow_deallocate)
423{
425#ifdef DFCC_DEBUG
428 "set writable");
429#endif
433 &(set->contract_frees));
438 set->linked_is_fresh = 0;
439 set->linked_allocated = 0;
440 set->linked_deallocated = 0;
441 set->assume_requires_ctx = assume_requires_ctx;
442 set->assert_requires_ctx = assert_requires_ctx;
443 set->assume_ensures_ctx = assume_ensures_ctx;
444 set->assert_ensures_ctx = assert_ensures_ctx;
445 set->allow_allocate = allow_allocate;
446 set->allow_deallocate = allow_deallocate;
447}
448
452{
454#ifdef DFCC_DEBUG
457 "set readable");
460 "contract_assigns writable");
463 "contract_frees writable");
466 "contract_frees_append writable");
468 __CPROVER_rw_ok(&(set->allocated.elems), 0), "allocated writable");
470 __CPROVER_rw_ok(&(set->deallocated.elems), 0), "deallocated writable");
471#endif
477 // do not free set->linked_is_fresh->elems or set->deallocated_linked->elems
478 // since they are owned by someone else.
479}
480
496
519
542
562
568 void *ptr)
569{
571 // we don't check yet that the pointer satisfies
572 // the __CPROVER_contracts_is_freeable as precondition.
573 // preconditions will be checked if there is an actual attempt
574 // to free the pointer.
575
576 // store pointer
578#ifdef DFCC_DEBUG
579 // manually inlined below
581 __CPROVER_assert(object_id < set->contract_frees.max_elems, "no OOB access");
582#else
585 : set->contract_frees.nof_elems + 1;
586 set->contract_frees.elems[object_id] = ptr;
587 set->contract_frees.is_empty = 0;
588#endif
589
590 // append pointer if available
591#ifdef DFCC_DEBUG
593#else
598#endif
599}
600
606 void *ptr)
607{
609 __CPROVER_assert(set->allow_allocate, "dynamic allocation is allowed");
610#if DFCC_DEBUG
611 // call inlined below
613#else
615 set->allocated.nof_elems = (set->allocated.elems[object_id] != 0)
616 ? set->allocated.nof_elems
617 : set->allocated.nof_elems + 1;
618 set->allocated.elems[object_id] = ptr;
619 set->allocated.is_empty = 0;
620#endif
621}
622
628 void *ptr)
629{
631#if DFCC_DEBUG
632 // call inlined below
634#else
636 set->allocated.nof_elems = (set->allocated.elems[object_id] != 0)
637 ? set->allocated.nof_elems
638 : set->allocated.nof_elems + 1;
639 set->allocated.elems[object_id] = ptr;
640 set->allocated.is_empty = 0;
641#endif
642}
643
653 void *ptr)
654{
656#ifdef DFCC_DEBUG
657 // manually inlined below
659#else
662 ? set->allocated.nof_elems - 1
663 : set->allocated.nof_elems;
664 set->allocated.is_empty = set->allocated.nof_elems == 0;
665 set->allocated.elems[object_id] = 0;
666#endif
667}
668
678 void *ptr)
679{
681#if DFCC_DEBUG
682 // we record the deallocation to be able to evaluate was_freed post conditions
687 // Manually inlined below
688#else
690
691 // __CPROVER_contracts_obj_set_add
694 : set->deallocated.nof_elems + 1;
695 set->deallocated.elems[object_id] = ptr;
696 set->deallocated.is_empty = 0;
697
698 // __CPROVER_contracts_obj_set_remove
700 ? set->allocated.nof_elems - 1
701 : set->allocated.nof_elems;
702 set->allocated.is_empty = set->allocated.nof_elems == 0;
703 set->allocated.elems[object_id] = 0;
704
705 // __CPROVER_contracts_obj_set_remove
707 ? set->contract_frees.nof_elems - 1
711
712 // __CPROVER_contracts_car_set_remove
715 while(idx != 0)
716 {
718 elem->is_writable = 0;
719 ++elem;
720 --idx;
721 }
722#endif
723}
724
736
747 void *ptr,
748 __CPROVER_size_t size)
749#if DFCC_DEBUG
750// manually inlined below
751{
754 ((ptr == 0) | __CPROVER_rw_ok(ptr, size)),
755 "ptr NULL or writable up to size");
756
758 (ptr == 0) | (__CPROVER_POINTER_OBJECT(ptr) < set->allocated.max_elems),
759 "no OOB access");
760
762 if(!car.is_writable)
763 return 0;
764
765 if(set->allocated.elems[__CPROVER_POINTER_OBJECT(ptr)] != 0)
766 return 1;
767
769}
770#else
771{
773# pragma CPROVER check push
774# pragma CPROVER check disable "pointer"
775# pragma CPROVER check disable "pointer-primitive"
776# pragma CPROVER check disable "unsigned-overflow"
777# pragma CPROVER check disable "signed-overflow"
778# pragma CPROVER check disable "undefined-shift"
779# pragma CPROVER check disable "conversion"
781 ((ptr == 0) | __CPROVER_rw_ok(ptr, size)),
782 "ptr NULL or writable up to size");
783
784 // the range is not writable
785 if(ptr == 0)
786 return 0;
787
788 // is ptr pointing within some a locally allocated object ?
789 if(set->allocated.elems[__CPROVER_POINTER_OBJECT(ptr)] != 0)
790 return 1;
791
792 // don't even drive symex into the rest of the function if the set is empty
793 if(set->contract_assigns.max_elems == 0)
794 return 0;
795
796 // Compute the upper bound, perform inclusion check against contract-assigns
799 "CAR size is less than __CPROVER_max_malloc_size");
800
802
804 !(offset > 0) | (offset + size <= __CPROVER_max_malloc_size),
805 "no offset bits overflow on CAR upper bound computation");
806 void *ub = (void *)((char *)ptr + size);
810
812 while(idx != 0)
813 {
814 incl |=
815 (int)elem->is_writable & (int)__CPROVER_same_object(elem->lb, ptr) &
816 (__CPROVER_POINTER_OFFSET(elem->lb) <= offset) &
818 ++elem;
819 --idx;
820 }
821 return incl;
822# pragma CPROVER check pop
823}
824#endif
825
845
865
893
912
925 void *ptr)
926{
929
930#ifdef DFCC_DEBUG
933 "set->contract_frees is indexed by object id");
936 "set->allocated is indexed by object id");
937#endif
938 return (set->allow_deallocate) &
939 ((ptr == 0) | (set->contract_frees.elems[object_id] == ptr) |
940 (set->allocated.elems[object_id] == ptr));
941}
942
955{
958 __CPROVER_contracts_car_t *current = candidate->contract_assigns.elems;
959 __CPROVER_size_t idx = candidate->contract_assigns.max_elems;
961 while(idx != 0)
962 {
963 if(current->is_writable)
964 {
966 reference, current->lb, current->size);
967 }
968 --idx;
969 ++current;
970 }
971 return incl;
972}
973
986{
988#ifdef DFCC_DEBUG
991 "reference->contract_frees is indexed by object id");
994 "reference->allocated is indexed by object id");
995#endif
997 void **current = candidate->contract_frees_append.elems;
998 __CPROVER_size_t idx = candidate->contract_frees_append.max_elems;
999
1001 while(idx != 0)
1002 {
1003 void *ptr = *current;
1005 all_incl &= (ptr == 0) |
1006 (reference->contract_frees.elems[object_id] == ptr) |
1007 (reference->allocated.elems[object_id] == ptr);
1008 --idx;
1009 ++current;
1010 }
1011
1012 return all_incl;
1013}
1014
1021
1031{
1033 void **current = set->contract_frees_append.elems;
1036 while(idx != 0)
1037 {
1038 void *ptr = *current;
1039
1040 // call free only iff the pointer is valid preconditions are met
1041 // skip checks on r_ok, dynamic_object and pointer_offset
1042 __CPROVER_bool preconditions =
1043 (ptr == 0) |
1044 ((int)__CPROVER_r_ok(ptr, 0) & (int)__CPROVER_DYNAMIC_OBJECT(ptr) &
1045 (__CPROVER_POINTER_OFFSET(ptr) == 0));
1046 // If there is aliasing between the pointers in the freeable set,
1047 // and we attempt to free again one of the already freed pointers,
1048 // the r_ok condition above will fail, preventing us to deallocate
1049 // the same pointer twice
1050 if((ptr != 0) & preconditions & __VERIFIER_nondet___CPROVER_bool())
1051 {
1054 // also record effects in the caller write set
1055 if(target != 0)
1057 }
1058 --idx;
1059 ++current;
1060 }
1061}
1062
1069{
1071#ifdef DFCC_DEBUG
1072 __CPROVER_assert(write_set != 0, "write_set not NULL");
1073#endif
1074 if((is_fresh_set != 0))
1075 {
1076 write_set->linked_is_fresh = is_fresh_set;
1077 }
1078 else
1079 {
1080 write_set->linked_is_fresh = 0;
1081 }
1082}
1083
1091{
1093#ifdef DFCC_DEBUG
1095 write_set_postconditions != 0, "write_set_postconditions not NULL");
1096#endif
1097 if((write_set_to_link != 0))
1098 {
1099 write_set_postconditions->linked_allocated =
1100 &(write_set_to_link->allocated);
1101 }
1102 else
1103 {
1104 write_set_postconditions->linked_allocated = 0;
1105 }
1106}
1107
1116{
1118#ifdef DFCC_DEBUG
1120 write_set_postconditions != 0, "write_set_postconditions not NULL");
1121#endif
1122 if((write_set_to_link != 0))
1123 {
1124 write_set_postconditions->linked_deallocated =
1125 &(write_set_to_link->deallocated);
1126 }
1127 else
1128 {
1129 write_set_postconditions->linked_deallocated = 0;
1130 }
1131}
1132
1139
1161 void **elem,
1162 __CPROVER_size_t size,
1164{
1167 (write_set != 0) & ((write_set->assume_requires_ctx == 1) |
1168 (write_set->assert_requires_ctx == 1) |
1169 (write_set->assume_ensures_ctx == 1) |
1170 (write_set->assert_ensures_ctx == 1)),
1171 "__CPROVER_is_fresh is used only in requires or ensures clauses");
1172#ifdef DFCC_DEBUG
1175 "set readable");
1177 write_set->linked_is_fresh, "set->linked_is_fresh is not NULL");
1178#endif
1179 if(write_set->assume_requires_ctx)
1180 {
1181#ifdef DFCC_DEBUG
1183 (write_set->assert_requires_ctx == 0) &
1184 (write_set->assume_ensures_ctx == 0) &
1185 (write_set->assert_ensures_ctx == 0),
1186 "only one context flag at a time");
1187#endif
1188 if(
1191 {
1192 // When --malloc-may-fail --malloc-fail-null
1193 // add implicit assumption that the size is capped
1195 }
1196 else if(
1199 {
1200 // When --malloc-may-fail --malloc-fail-assert
1201 // check if max allocation size is exceeded and
1202 // add implicit assumption that the size is capped
1205 "__CPROVER_is_fresh max allocation size exceeded");
1207 }
1208
1209 void *ptr = __CPROVER_allocate(size, 0);
1210 *elem = ptr;
1211
1212 // record the object size for non-determistic bounds checking
1216
1217 // do not detect memory leaks when assuming a precondition of a contract
1218 // for contract checking
1219 // __CPROVER_bool record_may_leak = __VERIFIER_nondet___CPROVER_bool();
1220 // __CPROVER_memory_leak = record_may_leak ? ptr : __CPROVER_memory_leak;
1221
1222 // record fresh object in the object set
1223#ifdef DFCC_DEBUG
1224 // manually inlined below
1225 __CPROVER_contracts_obj_set_add(write_set->linked_is_fresh, ptr);
1226#else
1228 write_set->linked_is_fresh->nof_elems =
1229 (write_set->linked_is_fresh->elems[object_id] != 0)
1230 ? write_set->linked_is_fresh->nof_elems
1231 : write_set->linked_is_fresh->nof_elems + 1;
1232 write_set->linked_is_fresh->elems[object_id] = ptr;
1233 write_set->linked_is_fresh->is_empty = 0;
1234#endif
1235 return 1;
1236 }
1237 else if(write_set->assume_ensures_ctx)
1238 {
1239#ifdef DFCC_DEBUG
1241 (write_set->assume_requires_ctx == 0) &
1242 (write_set->assert_requires_ctx == 0) &
1243 (write_set->assert_ensures_ctx == 0),
1244 "only one context flag at a time");
1245#endif
1246 // fail if size is too big
1247 if(
1250 {
1252 }
1253 else if(
1256 {
1259 "__CPROVER_is_fresh requires size <= __CPROVER_max_malloc_size");
1261 }
1262
1263 void *ptr = __CPROVER_allocate(size, 0);
1264 *elem = ptr;
1265
1266 // record the object size for non-determistic bounds checking
1270
1271 // detect memory leaks when is_fresh is assumed in a post condition
1272 // of a replaced contract to model a malloc performed by the function
1273 // being abstracted by the contract
1276
1277 // record fresh object in the caller's write set
1278#ifdef DFCC_DEBUG
1279 __CPROVER_contracts_obj_set_add(write_set->linked_allocated, ptr);
1280#else
1282 write_set->linked_allocated->nof_elems =
1283 (write_set->linked_allocated->elems[object_id] != 0)
1284 ? write_set->linked_allocated->nof_elems
1285 : write_set->linked_allocated->nof_elems + 1;
1286 write_set->linked_allocated->elems[object_id] = ptr;
1287 write_set->linked_allocated->is_empty = 0;
1288#endif
1289 return 1;
1290 }
1291 else if(write_set->assert_requires_ctx | write_set->assert_ensures_ctx)
1292 {
1293#ifdef DFCC_DEBUG
1295 (write_set->assume_requires_ctx == 0) &
1296 (write_set->assume_ensures_ctx == 0),
1297 "only one context flag at a time");
1298#endif
1299 __CPROVER_contracts_obj_set_ptr_t seen = write_set->linked_is_fresh;
1300 void *ptr = *elem;
1301 // null pointers or already seen pointers are not fresh
1302#ifdef DFCC_DEBUG
1303 // manually inlined below
1304 if((ptr == 0) || (__CPROVER_contracts_obj_set_contains(seen, ptr)))
1305 return 0;
1306#else
1307 if(ptr == 0)
1308 return 0;
1309
1311
1312 if(seen->elems[object_id] != 0)
1313 return 0;
1314#endif
1315 // record fresh object in the object set
1316#ifdef DFCC_DEBUG
1317 // manually inlined below
1319#else
1320 seen->nof_elems =
1321 (seen->elems[object_id] != 0) ? seen->nof_elems : seen->nof_elems + 1;
1322 seen->elems[object_id] = ptr;
1323 seen->is_empty = 0;
1324#endif
1325 // check size
1326 return __CPROVER_r_ok(ptr, size);
1327 }
1328 else
1329 {
1331 0, "__CPROVER_is_fresh is only called in requires or ensures clauses");
1333 return 0; // to silence libcheck
1334 }
1335}
1336
1338 void *lb,
1339 void **ptr,
1340 void *ub,
1342{
1345 (write_set != 0) & ((write_set->assume_requires_ctx == 1) |
1346 (write_set->assert_requires_ctx == 1) |
1347 (write_set->assume_ensures_ctx == 1) |
1348 (write_set->assert_ensures_ctx == 1)),
1349 "__CPROVER_pointer_in_range_dfcc is used only in requires or ensures "
1350 "clauses");
1351 __CPROVER_assert(__CPROVER_r_ok(lb, 0), "lb pointer must be valid");
1352 __CPROVER_assert(__CPROVER_r_ok(ub, 0), "ub pointer must be valid");
1354 __CPROVER_same_object(lb, ub),
1355 "lb and ub pointers must have the same object");
1359 lb_offset <= ub_offset, "lb and ub pointers must be ordered");
1360 if(write_set->assume_requires_ctx | write_set->assume_ensures_ctx)
1361 {
1363 return 0;
1364
1365 // add nondet offset
1367
1368 // this cast is safe because we prove that ub and lb are ordered
1370 __CPROVER_assume(offset <= max_offset);
1371 *ptr = (char *)lb + offset;
1372 return 1;
1373 }
1374 else /* write_set->assert_requires_ctx | write_set->assert_ensures_ctx */
1375 {
1377 return __CPROVER_same_object(lb, *ptr) && lb_offset <= offset &&
1378 offset <= ub_offset;
1379 }
1380}
1381
1386 __CPROVER_size_t idx)
1387{
1389#ifdef DFCC_DEBUG
1390 __CPROVER_assert(write_set != 0, "write_set not NULL");
1391#endif
1392
1394 if(car.is_writable)
1395 return car.lb;
1396 else
1397 return (void *)0;
1398}
1399
1405 __CPROVER_size_t idx)
1406{
1408 __CPROVER_assert(idx < set->contract_assigns.max_elems, "no OOB access");
1410 if(car.is_writable)
1412}
1413
1418 __CPROVER_size_t idx)
1419{
1421#ifdef DFCC_DEBUG
1422 __CPROVER_assert(idx < set->contract_assigns.max_elems, "no OOB access");
1423#endif
1425 if(car.is_writable)
1426 __CPROVER_havoc_slice(car.lb, car.size);
1427}
1428
1440 void *ptr,
1442{
1445 (set != 0) &
1446 ((set->assume_requires_ctx == 1) | (set->assert_requires_ctx == 1) |
1447 (set->assume_ensures_ctx == 1) | (set->assert_ensures_ctx == 1)),
1448 "__CPROVER_is_freeable is used only in requires or ensures clauses");
1449
1450 // These are all the preconditions checked by `free` of the CPROVER library
1451 __CPROVER_bool is_dynamic_object = (ptr == 0) | __CPROVER_DYNAMIC_OBJECT(ptr);
1453 (ptr == 0) | (__CPROVER_POINTER_OFFSET(ptr) == 0);
1454
1455 if((set->assume_requires_ctx == 1) || (set->assume_ensures_ctx == 1))
1456 return is_dynamic_object & has_offset_zero;
1457
1458 // these conditions cannot be used in assumptions since they involve
1459 // demonic non-determinism
1462 (ptr == 0) | (__CPROVER_deallocated != ptr);
1464 __CPROVER_bool is_not_array = (ptr == 0) | (__CPROVER_new_object != ptr) |
1466 return is_null_or_valid_pointer & is_dynamic_object & has_offset_zero &
1468}
1469
1472 void *ptr,
1474{
1477 (set != 0) &
1478 ((set->assume_ensures_ctx == 1) | (set->assert_ensures_ctx == 1)),
1479 "__CPROVER_was_freed is used only in ensures clauses");
1481 (set->linked_deallocated != 0), "linked_deallocated is not null");
1482#ifdef DFCC_DEBUG
1483 // manually inlined below
1485 set->linked_deallocated, ptr);
1486#else
1488 return set->linked_deallocated->elems[object_id] == ptr;
1489#endif
1490}
1491
1498 void *ptr,
1500{
1503 set && ((set->assume_ensures_ctx == 1) | (set->assert_ensures_ctx == 1)),
1504 "__CPROVER_was_freed is used only in ensures clauses");
1505
1506 if(set->assume_ensures_ctx)
1507 {
1508#ifdef DFCC_DEBUG
1509 // manually inlined below
1512 "assuming __CPROVER_was_freed(ptr) requires ptr to always exist in the "
1513 "contract's frees clause");
1514#else
1517 set->contract_frees.elems[object_id] == ptr,
1518 "assuming __CPROVER_was_freed(ptr) requires ptr to always exist in the "
1519 "contract's frees clause");
1520#endif
1521 }
1522}
1523
1533 void (**function_pointer)(void),
1534 void (*contract)(void),
1536{
1539 (set != 0) &
1540 ((set->assume_requires_ctx == 1) | (set->assert_requires_ctx == 1) |
1541 (set->assume_ensures_ctx == 1) | (set->assert_ensures_ctx == 1)),
1542 "__CPROVER_obeys_contract is used only in requires or ensures clauses");
1543 if((set->assume_requires_ctx == 1) | (set->assume_ensures_ctx == 1))
1544 {
1545 // decide if predicate must hold
1547 return 0;
1548
1549 // must hold, assign the function pointer to the contract function
1551 return 1;
1552 }
1553 else
1554 {
1555 // in assumption contexts, the pointer gets checked for equality
1556 return *function_pointer == contract;
1557 }
1558}
1559#endif // __CPROVER_contracts_library_defined
int __CPROVER_malloc_failure_mode
int __CPROVER_malloc_failure_mode_return_null
void * __CPROVER_allocate(__CPROVER_size_t size, __CPROVER_bool zero)
__CPROVER_bool __CPROVER_w_ok(const void *,...)
void __CPROVER_deallocate(void *)
int __CPROVER_malloc_failure_mode_assert_then_assume
__CPROVER_bool __CPROVER_rw_ok(const void *,...)
__CPROVER_bool __CPROVER_r_ok(const void *,...)
ait supplies three of the four components needed: an abstract interpreter (in this case handling func...
Definition ai.h:563
__CPROVER_size_t __CPROVER_OBJECT_SIZE(const void *)
void __CPROVER_assert(__CPROVER_bool assertion, const char *description)
void __CPROVER_havoc_slice(void *, __CPROVER_size_t)
__CPROVER_size_t __CPROVER_POINTER_OFFSET(const void *)
__CPROVER_size_t __CPROVER_POINTER_OBJECT(const void *)
__CPROVER_bool __CPROVER_same_object(const void *, const void *)
__CPROVER_bool __CPROVER_DYNAMIC_OBJECT(const void *)
void __CPROVER_assume(__CPROVER_bool assumption)
void __CPROVER_havoc_object(void *)
void __CPROVER_contracts_link_deallocated(__CPROVER_contracts_write_set_ptr_t write_set_postconditions, __CPROVER_contracts_write_set_ptr_t write_set_to_link)
Links write_set_to_link->deallocated to write_set_postconditions->linked_deallocated so that dealloca...
void __CPROVER_contracts_write_set_insert_object_whole(__CPROVER_contracts_write_set_ptr_t set, __CPROVER_size_t idx, void *ptr)
Inserts a snapshot of the range of bytes covering the whole object pointed to by ptr in set->contact_...
void __CPROVER_contracts_obj_set_release(__CPROVER_contracts_obj_set_ptr_t set)
Releases resources used by set.
__CPROVER_contracts_car_t __CPROVER_contracts_car_create(void *ptr, __CPROVER_size_t size)
Creates a __CPROVER_car_t struct from ptr and size.
__CPROVER_size_t __VERIFIER_nondet_size(void)
void __CPROVER_contracts_write_set_record_deallocated(__CPROVER_contracts_write_set_ptr_t set, void *ptr)
Records that an object is deallocated by adding the pointer ptr to set->deallocated.
__CPROVER_bool __CPROVER_contracts_write_set_check_havoc_object(__CPROVER_contracts_write_set_ptr_t set, void *ptr)
Checks if a havoc_object(ptr) is allowed according to set.
void __CPROVER_contracts_car_set_insert(__CPROVER_contracts_car_set_ptr_t set, __CPROVER_size_t idx, void *ptr, __CPROVER_size_t size)
Inserts a __CPROVER_contracts_car_t snapshotted from ptr and size into set at index idx.
void __CPROVER_contracts_write_set_insert_assignable(__CPROVER_contracts_write_set_ptr_t set, __CPROVER_size_t idx, void *ptr, __CPROVER_size_t size)
Inserts a snapshot of the range starting at ptr of size size at index idx in set->contract_assigns.
void __CPROVER_contracts_obj_set_remove(__CPROVER_contracts_obj_set_ptr_t set, void *ptr)
Removes ptr form set if ptr exists in set, no-op otherwise.
void __CPROVER_contracts_write_set_record_dead(__CPROVER_contracts_write_set_ptr_t set, void *ptr)
Records that an object is dead by removing the pointer ptr from set->allocated.
void __CPROVER_contracts_check_replace_ensures_was_freed_preconditions(void *ptr, __CPROVER_contracts_write_set_ptr_t set)
Asserts that ptr is found in set->contract_frees.
void * __CPROVER_contracts_write_set_havoc_get_assignable_target(__CPROVER_contracts_write_set_ptr_t set, __CPROVER_size_t idx)
Returns the start address of the conditional address range found at index idx in set->contract_assign...
void __CPROVER_contracts_obj_set_create_indexed_by_object_id(__CPROVER_contracts_obj_set_ptr_t set)
Initialises a __CPROVER_contracts_obj_set_t object to use it in "indexed by object id" mode.
__CPROVER_contracts_car_set_t * __CPROVER_contracts_car_set_ptr_t
Type of pointers to __CPROVER_contracts_car_set_t.
__CPROVER_bool __CPROVER_contracts_write_set_check_array_copy(__CPROVER_contracts_write_set_ptr_t set, void *dest)
Checks if the operation array_copy(dest, ...) is allowed according to set.
int __builtin_clzl(unsigned long)
void __CPROVER_contracts_write_set_deallocate_freeable(__CPROVER_contracts_write_set_ptr_t set, __CPROVER_contracts_write_set_ptr_t target)
Non-deterministically call __CPROVER_contracts_free on all elements of set->contract_frees,...
void __CPROVER_contracts_write_set_havoc_object_whole(__CPROVER_contracts_write_set_ptr_t set, __CPROVER_size_t idx)
Havocs the whole object pointed to by the lower bound pointer of the element stored at index idx in s...
__CPROVER_bool __CPROVER_contracts_is_fresh(void **elem, __CPROVER_size_t size, __CPROVER_contracts_write_set_ptr_t write_set)
Implementation of the is_fresh front-end predicate.
const void * __CPROVER_deallocated
void __CPROVER_contracts_write_set_add_decl(__CPROVER_contracts_write_set_ptr_t set, void *ptr)
Adds the pointer ptr to set->allocated.
const void * __CPROVER_new_object
void __CPROVER_contracts_write_set_release(__CPROVER_contracts_write_set_ptr_t set)
Releases resources used by set.
__CPROVER_bool __CPROVER_contracts_free(void *, __CPROVER_contracts_write_set_ptr_t)
Models the instrumented version of the free function.
__CPROVER_bool __CPROVER_contracts_obj_set_contains_exact(__CPROVER_contracts_obj_set_ptr_t set, void *ptr)
Checks if ptr is contained in set.
__CPROVER_bool __CPROVER_contracts_write_set_check_array_replace(__CPROVER_contracts_write_set_ptr_t set, void *dest, void *src)
Checks if the operation array_replace(dest, src) is allowed according to set.
void __CPROVER_contracts_car_set_create(__CPROVER_contracts_car_set_ptr_t set, __CPROVER_size_t max_elems)
Initialises a __CPROVER_contracts_car_set_ptr_t object.
__CPROVER_bool __CPROVER_contracts_obeys_contract(void(**function_pointer)(void), void(*contract)(void), __CPROVER_contracts_write_set_ptr_t set)
Implementation of the obeys_contract front-end predicate.
void __CPROVER_contracts_write_set_havoc_slice(__CPROVER_contracts_write_set_ptr_t set, __CPROVER_size_t idx)
Havocs the range of bytes represented byt the element stored at index idx in set->contract_assigns,...
void __CPROVER_contracts_obj_set_append(__CPROVER_contracts_obj_set_ptr_t set, void *ptr)
Appends ptr to set.
void __CPROVER_contracts_obj_set_create_append(__CPROVER_contracts_obj_set_ptr_t set, __CPROVER_size_t max_elems)
Initialises a __CPROVER_contracts_obj_set_t object to use it in "append" mode for at most max_elems e...
__CPROVER_size_t __CPROVER_max_malloc_size
__CPROVER_bool __VERIFIER_nondet___CPROVER_bool(void)
__CPROVER_contracts_write_set_t * __CPROVER_contracts_write_set_ptr_t
Type of pointers to __CPROVER_contracts_write_set_t.
void __CPROVER_contracts_write_set_add_freeable(__CPROVER_contracts_write_set_ptr_t set, void *ptr)
Adds the freeable pointer ptr to set->contract_frees.
__CPROVER_bool __CPROVER_contracts_car_set_contains(__CPROVER_contracts_car_set_ptr_t set, __CPROVER_contracts_car_t candidate)
Checks if candidate is included in one of set 's elements.
__CPROVER_bool __CPROVER_contracts_was_freed(void *ptr, __CPROVER_contracts_write_set_ptr_t set)
Returns true iff the pointer ptr is found in set->deallocated.
__CPROVER_bool __CPROVER_contracts_is_freeable(void *ptr, __CPROVER_contracts_write_set_ptr_t set)
Implementation of the is_freeable front-end predicate.
__CPROVER_bool __CPROVER_contracts_write_set_check_assigns_clause_inclusion(__CPROVER_contracts_write_set_ptr_t reference, __CPROVER_contracts_write_set_ptr_t candidate)
Checks the inclusion of the candidate->contract_assigns elements in reference->contract_assigns or re...
void __CPROVER_contracts_car_set_remove(__CPROVER_contracts_car_set_ptr_t set, void *ptr)
Invalidates all cars in the set that point into the same object as the given ptr.
__CPROVER_bool __CPROVER_contracts_write_set_check_assignment(__CPROVER_contracts_write_set_ptr_t set, void *ptr, __CPROVER_size_t size)
Checks if an assignment to the range of bytes starting at ptr and of size bytes is allowed according ...
const void * __CPROVER_memory_leak
__CPROVER_bool __CPROVER_contracts_write_set_check_deallocate(__CPROVER_contracts_write_set_ptr_t set, void *ptr)
Checks if the deallocation of ptr is allowed according to set.
void __CPROVER_contracts_obj_set_add(__CPROVER_contracts_obj_set_ptr_t set, void *ptr)
Adds the ptr to set.
const void * __CPROVER_alloca_object
__CPROVER_contracts_obj_set_t * __CPROVER_contracts_obj_set_ptr_t
Type of pointers to __CPROVER_contracts_car_set_t.
__CPROVER_bool __CPROVER_malloc_is_new_array
void __CPROVER_contracts_write_set_create(__CPROVER_contracts_write_set_ptr_t set, __CPROVER_size_t contract_assigns_size, __CPROVER_size_t contract_frees_size, __CPROVER_bool assume_requires_ctx, __CPROVER_bool assert_requires_ctx, __CPROVER_bool assume_ensures_ctx, __CPROVER_bool assert_ensures_ctx, __CPROVER_bool allow_allocate, __CPROVER_bool allow_deallocate)
Initialises a __CPROVER_contracts_write_set_t object.
__CPROVER_bool __CPROVER_contracts_write_set_check_frees_clause_inclusion(__CPROVER_contracts_write_set_ptr_t reference, __CPROVER_contracts_write_set_ptr_t candidate)
Checks the inclusion of the candidate->contract_frees elements in reference->contract_frees or refere...
void __CPROVER_contracts_write_set_insert_object_upto(__CPROVER_contracts_write_set_ptr_t set, __CPROVER_size_t idx, void *ptr, __CPROVER_size_t size)
Inserts a snapshot of the range of bytes starting at ptr of size bytes in set->contact_assigns at ind...
__CPROVER_bool __CPROVER_contracts_obj_set_contains(__CPROVER_contracts_obj_set_ptr_t set, void *ptr)
Checks if a pointer with the same object id as ptr is contained in set.
void __CPROVER_contracts_link_is_fresh(__CPROVER_contracts_write_set_ptr_t write_set, __CPROVER_contracts_obj_set_ptr_t is_fresh_set)
Links is_fresh_set to write_set->linked_is_fresh so that the is_fresh predicates can be evaluated in ...
__CPROVER_bool __CPROVER_contracts_write_set_check_allocated_deallocated_is_empty(__CPROVER_contracts_write_set_ptr_t set)
Returns true iff set->deallocated is empty.
void __CPROVER_contracts_link_allocated(__CPROVER_contracts_write_set_ptr_t write_set_postconditions, __CPROVER_contracts_write_set_ptr_t write_set_to_link)
Links write_set_to_link->allocated to write_set_postconditions->linked_allocated so that allocations ...
void __CPROVER_contracts_write_set_insert_object_from(__CPROVER_contracts_write_set_ptr_t set, __CPROVER_size_t idx, void *ptr)
Inserts a snapshot of the range of bytes starting at ptr and extending to the end of the object in se...
__CPROVER_bool __CPROVER_contracts_pointer_in_range_dfcc(void *lb, void **ptr, void *ub, __CPROVER_contracts_write_set_ptr_t write_set)
void __CPROVER_contracts_write_set_add_allocated(__CPROVER_contracts_write_set_ptr_t set, void *ptr)
Adds the dynamically allocated pointer ptr to set->allocated.
void * __CPROVER_contracts_malloc(__CPROVER_size_t, __CPROVER_contracts_write_set_ptr_t)
Models the instrumented interface of the malloc function.
__CPROVER_bool __CPROVER_contracts_write_set_check_array_set(__CPROVER_contracts_write_set_ptr_t set, void *dest)
Checks if the operation array_set(dest, ...) is allowed according to set.
int __builtin_clzll(unsigned long long)
A set of __CPROVER_contracts_car_t.
__CPROVER_size_t max_elems
Maximum number of elements that can be stored in the set.
__CPROVER_contracts_car_t * elems
An array of car_t of size max_elems.
A conditionally writable range of bytes.
__CPROVER_size_t size
Size of the range in bytes.
void * lb
Lower bound address of the range.
__CPROVER_bool is_writable
True iff __CPROVER_w_ok(lb, size) holds at creation.
void * ub
Upper bound address of the range.
__CPROVER_bool is_empty
True iff nof_elems is 0.
void ** elems
Array of void *pointers, indexed by their object ID or some other order.
__CPROVER_bool indexed_by_object_id
True iff elems is indexed by the object id of the pointers.
__CPROVER_size_t watermark
next usable index in elems if less than max_elems (1 + greatest used index in elems)
__CPROVER_size_t nof_elems
Number of elements currently in the elems array.
__CPROVER_size_t max_elems
Maximum number of elements that can be stored in the set.
Runtime representation of a write set.
__CPROVER_contracts_obj_set_ptr_t linked_allocated
Object set recording the is_fresh allocations in post conditions.
__CPROVER_bool allow_deallocate
True iff dynamic deallocation is allowed (default: true)
__CPROVER_contracts_obj_set_t contract_frees
Set of freeable pointers derived from the contract (indexed mode)
__CPROVER_contracts_obj_set_t deallocated
Set of objects deallocated by the function under analysis (indexed mode)
__CPROVER_contracts_obj_set_ptr_t linked_deallocated
Object set recording the deallocations (used by was_freed)
__CPROVER_contracts_obj_set_ptr_t linked_is_fresh
Pointer to object set supporting the is_fresh predicate checks (indexed mode)
__CPROVER_contracts_car_set_t contract_assigns
Set of car derived from the contract.
__CPROVER_bool assert_requires_ctx
True iff the write set checks requires clauses in an assertion ctx.
__CPROVER_bool assume_requires_ctx
True iff the write set checks requires clauses in an assumption ctx.
__CPROVER_bool assert_ensures_ctx
True iff this write set checks ensures clauses in an assertion ctx.
__CPROVER_contracts_obj_set_t allocated
Set of objects allocated by the function under analysis (indexed mode)
__CPROVER_bool assume_ensures_ctx
True iff the write set checks ensures clauses in an assumption ctx.
__CPROVER_bool allow_allocate
True iff dynamic allocation is allowed (default: true)
__CPROVER_contracts_obj_set_t contract_frees_append
Set of freeable pointers derived from the contract (append mode)