dcci

Inductive ev : nat -> Prop :=
| ev_0 : ev 0
| ev_SS : forall n : nat, ev n -> ev (S (S n)).


Theorem ev_4 : ev 4.
Proof.
  apply ev_SS.
  apply ev_SS.
  apply ev_0.

dcci

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.

dcci

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

dcci

#include <cassert>
#include <cstdint>

enum Register_count {
  gpr_registers_count = 0,
  fpr_registers_count,
  msa_registers_count,
  register_set_count
};

dcci

 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.

dcci

[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/

dcci

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

#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

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

dcci

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