Skip to content

Instantly share code, notes, and snippets.

View delcypher's full-sized avatar

Dan Liew delcypher

109 followers · 31 following
View GitHub Profile
@delcypher
delcypher / smt2
Last active February 15, 2019 09:36
Proof that an equality (that would be useful if true) does not hold
;;
;; Prove that
;; (x -y) >> 3 != ((x >> 3) - (y >> 3))
;;
;; if x >= y
;;
;;
(declare-fun x () (_ BitVec 32))
(declare-fun y () (_ BitVec 32))
(declare-fun shift () (_ BitVec 32))
@delcypher
delcypher / idrac_auth.sh
Created July 7, 2017 14:39
Enable iDRAC web access ADMIN privilidge
#!/bin/bash
# Based on http://lists.us.dell.com/pipermail/linux-poweredge/2013-April/047905.html
set -x
set -e
set -o pipefail
function usage() {
echo "$0 <user_id>"
}
@delcypher
delcypher / PKGBUILD
Created January 22, 2017 19:30
Hacked version of PKGBUILD for AUR build of git-lfs
# Maintainer: Michael Schubert <mschu.dev at gmail>
# Contributor: Mikkel Oscar Lyderik <mikkeloscar at gmail dot com>
pkgname=git-lfs
pkgver=1.5.5
pkgrel=1
pkgdesc="An open source Git extension for versioning large files"
arch=('i686' 'x86_64' 'armv7h')
url="https://${pkgname}.github.com"
license=('MIT')
makedepends=('go' 'ruby-ronn')
@delcypher
delcypher / # llvm34 - 2016-12-18_23-15-29.txt
Created December 18, 2016 23:17
llvm34 (homebrew/versions/llvm34) on macOS 10.12.2 - Homebrew build logs
Homebrew build logs for homebrew/versions/llvm34 on macOS 10.12.2
Build date: 2016-12-18 23:15:29
@delcypher
delcypher / fuzz_subnormal_result_implies_exact.c
Created December 2, 2016 14:08
Use LibFuzzer to look for violations of the result of floating point addition being subnormal implying
#include <assert.h>
#include <fenv.h>
#include <inttypes.h>
#include <math.h>
#include <stdlib.h>
#include <stdint.h>
#include <stdio.h>
#include <string.h>
int is_subnormal(float f) {
@delcypher
delcypher / fuzz_subnormal_result_implies_exact.c
Created December 2, 2016 13:15
Fuzzing "subnormal result implies exact result with LibFuzzer"
#include <assert.h>
#include <inttypes.h>
#include <math.h>
#include <stdlib.h>
#include <stdint.h>
#include <stdio.h>
#include <string.h>
int is_subnormal(float f) {
return fpclassify(f) == FP_SUBNORMAL;
@delcypher
delcypher / test_subnormal_result_implies_exact_result.c
Created December 2, 2016 12:40
Approximately check if result of addition is subnormal with KLEE
#include "klee/klee.h"
#include <assert.h>
#include <math.h>
#include <stdio.h>
int is_subnormal(float f) {
return fpclassify(f) == FP_SUBNORMAL;
}
int main() {
@delcypher
delcypher / hamming.c
Last active July 18, 2017 12:57
Check equivalence with KLEE
#include "klee/klee.h"
#include <assert.h>
#include <inttypes.h>
#include <stdio.h>
//types and constants used in the functions below
const uint64_t m1 = 0x5555555555555555; //binary: 0101...
const uint64_t m2 = 0x3333333333333333; //binary: 00110011..
const uint64_t m4 = 0x0f0f0f0f0f0f0f0f; //binary: 4 zeros, 4 ones ...
const uint64_t m8 = 0x00ff00ff00ff00ff; //binary: 8 zeros, 8 ones ...
@delcypher
delcypher / try-catch.c
Last active April 29, 2016 13:43
Demonstration of poor man's try-catch construct in C99 using preprocessor macros
/* Demonstration of a poor man's try-catch construct in C99 using
* C preprocessor macros to make the syntax look vaguely like
* try-catch constructs in other lagnuages. This implementation
* is incredibly bad because C macros are very error prone and
* this implementation cannot have nested try-catch constructs
*/
#include <stdio.h>
#include <assert.h>
#define TRY ; _Pragma("pop_macro(\"EXCEPTION_EXIT_LABEL\")")
@delcypher
delcypher / gist:a929b1d289270a04040c
Last active November 26, 2015 18:32
PKGBUILD (Arch Linux build script) for fork of Z3 that supports installing java, python and Z3 bindings
# Maintainer: d.woffinden
# Contributor: Dan Liew <[email protected]>
pkgbase=('z3-git')
pkgname=('z3-git' 'z3py-git' 'z3-sharp-git' 'z3-java-git')
pkgver=4.4.1.r308.g9e28819
pkgrel=1
pkgdesc="Z3 is a high-performance theorem prover being developed at Microsoft Research"
arch=('i686' 'x86_64')
url="https://github.com/delcypher/z3-1.git"
license=('MIT')