regehr

regehr@john-home:~/mctoll/llvm-project/llvm/tools/llvm-mctoll$ creduce --help
creduce 2.10.0 (fb91843) -- a C and C++ program reducer

C-Reduce requires an "interestingness test" and one or more files to
reduce, which must be writable. The interestingness test is an
executable program (usually a shell script) that returns 0 when a
partially reduced file is interesting (a candidate for further
reduction) and returns non-zero when a partially reduced file is not
interesting (not a candidate for further reduction -- all
uninteresting files are discarded).

regehr

regehr@john-home:~/remill-build$ ./tools/lift/remill-lift-4.0 -ir_out /dev/stdout --bytes 4889f9b802000000d3c0c3 --slice_inputs RSP,EDI --slice_outputs RAX
; ModuleID = 'lifted_code'
source_filename = "lifted_code"
target datalayout = "e-m:e-i64:64-f80:128-n8:16:32:64-S128"
target triple = "x86_64-pc-linux-gnu-elf"

%struct.Memory = type opaque
%struct.State = type { %struct.ArchState, [32 x %union.VectorReg], %struct.ArithFlags, %union.anon, %struct.Segments, %struct.AddressSpace, %struct.GPR, %struct.X87Stack, %struct.MMX, %struct.FPUStatusFlags, %union.anon, %union.FPU, %struct.SegmentCaches }
%struct.ArchState = type { i32, i32, %union.anon }
%union.VectorReg = type { %union.vec512_t }

regehr

89		if (current_clr_polling_and_test()) {
93			arch_cpu_idle();
arch_cpu_idle () at arch/x86/kernel/process.c:571
571		x86_idle();
__x86_indirect_thunk_rax () at arch/x86/lib/retpoline.S:32
32	GENERATE_THUNK(_ASM_AX)
default_idle () at arch/x86/kernel/process.c:578
578	{
579		trace_cpu_idle_rcuidle(1, smp_processor_id());
580		safe_halt();

regehr

#include <stdio.h>
#include <stdlib.h>
#include <unistd.h>

static void ensure(int x) {
  if (x)
    return;
  printf("ensure failed, exiting\n");
  exit(-1);
}

regehr

#include <stdio.h>
#include <stdlib.h>
#include <unistd.h>

void ensure(int x) {
  if (!x) {
    printf("ensure failed, exiting\n");
    exit(-1);
  }
}

regehr

#include <filesystem>
#include <iostream>

namespace fs = std::filesystem;
using namespace std;

int main() {
  fs::path aPath{"./path/to/file.txt"};

  cout << "Parent path: " << aPath.parent_path() << endl;

regehr

#define hash_prime 1009 \

#define streq(a,b) (strncmp(a,b,5) ==0)  \

#define min_treasure GOLD
#define is_treasure(t) (t>=min_treasure) 
#define max_obj CHAIN \

#define ok default_msg[RELAX] \

regehr

from z3 import *

n = 10

vars = []

def getConstraint(v, x, y):
  if x < 0 or x >= n or y < 0 or y >= n:
    return False
  return v == (1 + vars[x][y])

regehr

from z3 import *

width = 64

Range = Datatype("range")
Range.declare('make', ('lo', BitVecSort(width)), ('hi', BitVecSort(width)))
Range = Range.create()

def isEmptySet(r):
    return And((Range.lo(r) == BitVecVal(0, width)), (Range.hi(r) == BitVecVal(0, width)))

regehr

(define-fun div3 ((i Int)) Bool
  (= (mod i 3) 0)
)

(define-fun-rec sumit ((i Int)) Int
     (ite (< i 10)
          i
          (+ (mod i 10) (sumit (div i 10))))
)