jepler

import os
import re
import sys
import xml.etree.ElementTree
import BeautifulSoup

def exc_wrap(f):
    def inner(*args, **kw):
        try:
            return f(*args, **kw)

jepler

jepler@babs:~$ gcc -Os rsq.c -lm && ./a.out
0.993271
jepler@babs:~$ gcc -Os -funsafe-math-optimizations rsq.c -lm && ./a.out
1.365475

jepler

$ halrun test.hal 
test.hal:1: Warning: HAL_LIB: HAL will pretend that the exact base period requested is possible.
This mode is not suitable for running real hardware.
hal/components/sampler.c:429:22: runtime error: unsigned integer overflow: 0 - 1 cannot be represented in type 'unsigned long'
==22536==WARNING: ASan doesn't fully support makecontext/swapcontext functions and may produce false positives in some cases!
hal/components/sampler_usr.c:255:22: runtime error: unsigned integer overflow: 18446744073709551615 + 1 cannot be represented in type 'unsigned long'

jepler

@unix
mem = 1042
^?^?RESTRICTED RIGHTS
^?^?
^?^?Use, duplication or disclosure is subject to
^?^?restrictions stated in Contract with Western
^?^?Electric Company, Inc.
^?^?# STTY -LCASE
# echo 'main() { printf("hi\n"); } ' > hi.c
# cc hi.c

jepler

#if defined(__clang__) && __clang__
#define RTAPI_USE_ATOMIC 1
#elif defined(__GNUC__) && (__GNUC__ > 4) && (__GNUC_MINOR__ >= 7)
#define RTAPI_USE_ATOMIC 1
#else
#define RTAPI_USE_ATOMIC 0
#endif

typedef unsigned long rtapi_atomic_type;
#define RTAPI_DIV_ROUND_UP(n,d) (((n) + (d) - 1) / (d))

jepler

#!/usr/bin/python
from __future__ import division
import bisect
import random
import sys

# 9 animal types - even probability
# 10 potion types - uneven probability
#       1/5: set of 10
#       1/5: set of 9

jepler

// cbmc cmbc.c ref.c jepler.c -DBUFSIZE=1 -DCMBC
#include "nibble.h"
#include <assert.h>
#include <inttypes.h>
#include <string.h>

uint64_t nondet_u64(); 
void main() {
    setup_jepler();
    uint64_t ref[BUFSIZE], res[BUFSIZE];

jepler

              ns     ns / 8 bytes       entry name           errors
           42447            41.45       alexander2                0
           42604            41.61          vetter4                0
           44426            43.38          vetter3               64
           54061            52.79           jepler                0
           58071            56.71           jerome                0
           62759            61.29          parnell                0
           62967            61.49          burton2                0
           79841            77.97             rjk9                0
           80519            78.63            nadav                0

jepler

import sha
import sys

f = open("/dev/urandom", "rb")
while 1:
    sys.stderr.write(".")
    message0 = f.read(256)
    cs0 = sha.new(message0).digest()[:2]

    flip_bit = 1 << (ord(f.read(1)) % 8)

jepler

$ /tmp/cbmc -D FAIL mycmp.c  --trace 
CBMC version 5.6 64-bit x86_64 linux
Parsing mycmp.c
Converting
Type-checking mycmp
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation