Skip to content

Instantly share code, notes, and snippets.


Block or report user

Report or block comex

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
View hello.c
module Main
main : IO ()
main = putStrLn "Hello world"
View factorial.c
#include <stdint.h>
/*@ logic uint32_t factorial_logic(uint32_t n) =
@ (uint32_t)(
@ (n == 0) ? 1
@ : n * factorial_logic((uint32_t)(n - 1))
@ ); */
/*@ ensures \result == factorial_logic(n); */
static uint32_t factorial_recursive(uint32_t n) {
View prof-41897.html
This file has been truncated, but you can view the full file.
<style media="all" type="text/css">
table {
border-collapse: collapse;
border: 1px solid #CCC;
font-family: Verdana, Arial, Helvetica, sans-serif;
comex / gist:3998384422fad54bcb5b89979a5115a9
Created Nov 28, 2018
filtered log.txt when running LustyJuggler
View gist:3998384422fad54bcb5b89979a5115a9
D, [2018-11-27T14:16:24.014704 #40147] DEBUG -- : {:_class=>Neovim::Session, :_method=>:request, :method_name=>:nvim_get_api_info, :request_id=>2, :blocking=>false, :arguments=>[]}
D, [2018-11-27T14:16:24.020182 #40147] DEBUG -- : {:_class=>Neovim::Session, :_method=>:request, :method_name=>"nvim_command", :request_id=>3, :blocking=>false, :arguments=>["au DirChanged * call rpcrequest(3, 'ruby_chdir', v:event)"]}
D, [2018-11-27T14:16:24.022228 #40147] DEBUG -- : {:_class=>Neovim::Session, :_method=>:request, :method_name=>"nvim_eval", :request_id=>4, :blocking=>false, :arguments=>["bufnr('%')"]}
D, [2018-11-27T14:16:24.022503 #40147] DEBUG -- : {:_class=>Neovim::Session, :_method=>:request, :method_name=>"nvim_get_current_buf", :request_id=>5, :blocking=>false, :arguments=>[]}
D, [2018-11-27T14:16:24.022851 #40147] DEBUG -- : {:_class=>Neovim::Session, :_method=>:request, :method_name=>"nvim_get_current_win", :request_id=>6, :blocking=>false, :arguments=>[]}
D, [2018-11-27T14:16:24.029881 #40147] DEBUG -- : {
// Prove that
// ∀p. ∀q. (p ∨ q)
// implies
// ∀p. ∀q. ¬(¬p ∧ ¬q)
pub fn foo(fa1: ForAll<ForAll<Or<DB2, DB3>>>) -> ForAll<ForAll<Not<And<Not<DB4>, Not<DB5>>>>> {
map!(fa1, |fa2: ForAll<_>| {
map!(fa2, |or: Or<_, _>| {
View results
'dummy' is just two rdtscps in a row plus some shifting instructions generated to interpret the value.
smolset_lookup_simd: cycles=26.260086
smolset_lookup_naive_linear: cycles=34.332955
smolset_lookup_linear_unrollable: cycles=33.906475
smolset_lookup_linear_manualunroll: cycles=32.245281
smolset_lookup_binary_manualunroll: cycles=47.629102
smolset_lookup_naive_binary: cycles=41.811521
View ipdtest.cpp
#include <stdlib.h>
#include <stdio.h>
#include "OVR_CAPI.h"
int main()
ovrResult result = ovr_Initialize(NULL);
if (OVR_FAILURE(result)) {
ovrErrorInfo errorInfo;
View from X86ISelLowering.cpp
// LowerUINT_TO_FP_i64 - 64-bit unsigned integer to double expansion.
SDValue X86TargetLowering::LowerUINT_TO_FP_i64(SDValue Op,
SelectionDAG &DAG) const {
// This algorithm is not obvious. Here it is what we're trying to output:
movq %rax, %xmm0
punpckldq (c0), %xmm0 // c0: (uint4){ 0x43300000U, 0x45300000U, 0U, 0U }
subpd (c1), %xmm0 // c1: (double2){ 0x1.0p52, 0x1.0p52 * 0x1.0p32 }
#ifdef __SSE3__
haddpd %xmm0, %xmm0
comex / fetchsymbols.c
Created May 8, 2015
4 year old code to talk to a DeveloperDiskImage service
View fetchsymbols.c
#include "MobileDevice.h"
#include <assert.h>
#include <unistd.h>
#include <sys/socket.h>
#define bswap32 __builtin_bswap32
static uint32_t read32(int fd) {
uint32_t ret;
assert(read(fd, &ret, sizeof(ret)) == sizeof(ret));
return bswap32(ret);
comex / wormdump.c
Created Apr 9, 2015
Some old broken code in case it helps anyone
View wormdump.c
#include <sys/socket.h>
#include <sys/ioctl.h>
#include <sys/kern_event.h>
#include <stdio.h>
#include <stdint.h>
#include <stdbool.h>
#include <stdlib.h>
#include <assert.h>
#include <string.h>
#include <net/ethernet.h>
You can’t perform that action at this time.