Skip to content

Instantly share code, notes, and snippets.

Avatar

Davide Italiano dcci

View GitHub Profile
@dcci
dcci / first.v
Last active Mar 5, 2018
software foundations
View first.v
Check 3 = 3.
Check forall n m : nat, n + m = m + n.
Definition is_three (n : nat) : Prop :=
n = 3.
Definition injective {A B} (f : A -> B) :=
forall x y : A, f x = f y -> x = y.
Lemma succ_inj : injective S.
View gist:891cd98d80b1b95352a407d80914f7cf
#!/bin/bash
# git bisect start
# git bisect good <rev>
# git bisect bad <rev>
# git bisect run [script]
cd /home/davide/work/llvm-monorepo/build
ninja opt lli || exit 125 #125 tells git-bisect to skip
ulimit -t 5 && /home/davide/work/llvm-monorepo/build/bin/opt /home/davide/work/llvm-monorepo/build/bin/foo.ll -O3 | /home/davide/work/llvm-monorepo/build/bin/lli
[[ $? == 0 ]] && exit 0
View gist:01c10b405041fa8d139a4f71aec102f7
#include <cassert>
#include <cstdint>
enum Register_count {
gpr_registers_count = 0,
fpr_registers_count,
msa_registers_count,
register_set_count
};
@dcci
dcci / btree.rs
Last active Mar 1, 2017
btree interface
View btree.rs
use std::marker::PhantomData;
/// A B-tree data structure which nodes are allocated from a pool.
pub struct BTree<K, V> {
index : u32,
unused1: PhantomData<K>,
unused2: PhantomData<V>
}
// A Node reference is a direct index to an element of the pool.
View gist:95da518b5216c7e187d49b0dcf88d880
[davide@localhost build]$ ninja check-llvm
[573/2081] Building CXX object lib/Transfor...ar/CMakeFiles/LLVMScalarOpts.dir/SCCP.cpp.o
FAILED: /usr/lib64/ccache/c++ -DGTEST_HAS_RTTI=0 -D_DEBUG -D_GNU_SOURCE -D__STDC_CONSTANT_MACROS -D__STDC_FORMAT_MACROS -D__STDC_LIMIT_MACROS -Ilib/Transforms/Scalar -I../lib/Tran
sforms/Scalar -Iinclude -I../include -fPIC -fvisibility-inlines-hidden -Wall -W -Wno-unused-parameter -Wwrite-strings -Wcast-qual -Wno-missing-field-initializers -pedantic -Wno-long
-long -Wno-maybe-uninitialized -Wdelete-non-virtual-dtor -Wno-comment -Werror=date-time -std=c++11 -g -fno-exceptions -fno-rtti -MMD -MT lib/Transforms/Scalar/CMakeFiles/LLVMScal
arOpts.dir/SCCP.cpp.o -MF lib/Transforms/Scalar/CMakeFiles/LLVMScalarOpts.dir/SCCP.cpp.o.d -o lib/Transforms/Scalar/CMakeFiles/LLVMScalarOpts.dir/SCCP.cpp.o -c ../lib/Transforms/Sca
lar/SCCP.cpp
../lib/Transforms/Scalar/SCCP.cpp: In member function ‘void {anonymous}::SCCPSolver::markOverdefined({anonymous}::LatticeVal&, llvm::Value*)’:
../lib/
View gist:5f674b93f8bfeae393e01bc35a9b9228
#!/bin/sh
/home/davide/work/llvm-monorepo/build/bin/opt @$1 /home/davide/work/llvm-monorepo/build/bin/unopt.ll -o - | /home/davide/work/llvm-monorepo/build/bin/lli | grep ^1
ret_sane=$?
/home/davide/work/llvm-monorepo/build/bin/opt-broken @$1 /home/davide/work/llvm-monorepo/build/bin/unopt.ll -o - | /home/davide/work/llvm-monorepo/build/bin/lli | grep ^-1
ret_broken=$?
[[ $ret_sane == 0 && $ret_broken == 0 ]] && exit 0
exit 1
@dcci
dcci / floating.c
Last active Jul 13, 2016
Floating point is fun
View floating.c
#include <math.h>
#include <stdio.h>
int main(void) {
// pow(x, 0.5) -> sqrt(x)
printf("%f %f\n", pow(-0.0, 0.5), sqrt(-0.0));
return (0);
}
@dcci
dcci / gist:f83538d46dbcde9457bc663a2218c97e
Created Jun 23, 2016
Replacing malloc() on Windows.
View gist:f83538d46dbcde9457bc663a2218c97e
#include <limits.h>
#include <malloc.h>
#include <new.h>
#include <windows.h>
#include <stddef.h>
#include <stdio.h>
namespace {
const size_t kWindowsPageSize = 4096;
const size_t kMaxWindowsAllocation = INT_MAX - kWindowsPageSize;
View gist:c737c11cc58c0c13bffac3dab30c6002
*** Dumping AST Record Layout
0 | class llvm::DILocalVariable
0 | class llvm::DIVariable (base)
0 | class llvm::DINode (base)
0 | class llvm::MDNode (base)
0 | class llvm::Metadata (base)
0 | const unsigned char SubclassID
1:0-1 | unsigned int Storage
2 | unsigned short SubclassData16
4 | unsigned int SubclassData32
View gist:e69cad69179e23069267f4f986be0975
[davide@localhost bin]$ g++ blah.cpp -o blah
blah.cpp: In function ‘int main()’:
blah.cpp:10:9: error: ‘union’ tag used in naming ‘struct G<int>’ [-fpermissive]
union G<int> foo;
^
blah.cpp:4:7: note: ‘struct G<int>’ was previously declared here
class G {
^
[davide@localhost bin]$ cat blah.cpp
#include <stdio.h>
You can’t perform that action at this time.