ymherklotz

int foo() {
    int i, j, k;
    int a = 3, b = 5;
 L0: for (i=0; i<3; i++)
        a += f(i);
 L1: for (j=0; j<4; j++) {
        a += g(j);
    L2: for (k=0; k<3; k++)
            b += h(k);  // instead of h(j, k)
    }

ymherklotz

1:(input (#1:(and #2:(>= 1 op_2))))
2:(input (#3:(and #4:(= 1 op_19))))
3:(input (#5:(and #6:(= 1 op_29))))
4:(input (#7:(and #8:(>= 1 op_31))))
5:(input (#9:(and #10:(>= 1 op_42))))
6:(input (#11:(and #12:(= 1 op_55))))
7:(input (#13:(= op_42 #14:(- op_1))))
8:(input (#15:(= 0 op_45)))
9:(input (#16:(ite #17:(< 1 #18:(+ 0 op_45)) #19:(= 1 op_46) #20:(= #18 op_46))))
10:(input (#21:(ite #22:(< 1 #23:(+ #24:(- 1 op_1) op_46)) #25:(= 1 op_47) #26:(= 0 op_47))))

ymherklotz

#include <iostream>
#include <fstream>
#include <sstream>
#include <vector>

using namespace std;

struct node {
    string a;
    string b;

ymherklotz

{-# Language TypeApplications #-}

module Main where

import Control.Monad.State.Strict

type S a = State [a] a

-- Long form without abstraction

ymherklotz

module Main where

import Control.Monad (when)
import Data.Foldable (fold)

-- Initial version (You should always add types, mostly just for you not because the compiler needs
-- them.)  Then you see that the function doesn't do anything except side-effects, because it
-- returns IO (), which means a side effect without a return value.

-- Int -> IO (): means it takes an int and returns IO ().

ymherklotz

int f (int A[1000], int B[1000]) {
    for (int i = 0; i < 1000; i++) {
        if (i % 2) {
            A[i] = B[i];
        }
    }
    for (int i = 0; i < 1000; i++) {
        if (! (i % 2)) {
            A[i] = B[i];
        }

ymherklotz

f(x16, x8) {
   46:	nop
   45:	nop
   44:	x36 = 0
   43:	nop
   42:	nop
   41:	x34 = μ(x38, x36)
     nop
   40:	x140 = x34
   39:	x156 = x140 >>x 1

ymherklotz

/* Initial design */
module top(input i,
           output reg o);
   reg tmp;
   always @* begin
      o = tmp;
      tmp = i;
   end
endmodule

ymherklotz

From Coq Require Import PeanoNat.
From bbv Require Import Word.

Record value : Type :=
  mkvalue {
    vsize: nat;
    vword: word vsize
  }.

Definition unify_word (sz1 sz2 : nat) (w1 : word sz2): sz1 = sz2 -> word sz1.

ymherklotz