comex

## foo.cc
#include <stdio.h>
#include <threads.h>
#include <stdatomic.h>

#include "librace.h"
#include "model-assert.h"

std::atomic_int x;
std::atomic_int side_channel;
std::atomic_int tests_synchronization;

## hello.c
/*
source:

module Main

main : IO ()
main = putStrLn "Hello world"

*/

## 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) {

## prof-41897.html

<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01//EN" "http://www.w3.org/TR/html4/strict.dtd">
<html>
<head>
  <style media="all" type="text/css">
    table {
      border-collapse: collapse;
      border: 1px solid #CCC;
      font-family: Verdana, Arial, Helvetica, sans-serif;

## 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 -- : {

## foo.rs
// 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<_, _>| {
            or.de_morgan()
        })
    })

## results
'dummy' is just two rdtscps in a row plus some shifting instructions generated to interpret the value.

clang-800.0.42.1:

                     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

## 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;
	    ovr_GetLastErrorInfo(&errorInfo);

## 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

## 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);