\myheading{Arithmetical shift bit twiddling hack}

Prove that \verb|((x+0x80000000) >>u n) - (0x80000000 >>u n)| 
works like arithmetical shift (\verb|bvashr| function in SMT-LIB or \verb|SAR| x86 instruction).

See: Henry Warren 2ed: "2-7 Shift Right Signed from Unsigned".

Also, check if I implemented signed shift right correctly in my MK85:

% FIXME: move this to the MK85 section

\begin{lstlisting}[style=customc]
// direction=false for shift left
// direction=true for shift right
// arith=true is for bvashr (only for shifting right)

// for 8-bit left shifter, this is:
// X=ITE(cnt&1, X<<1, X)
// X=ITE((cnt>>1)&1, X<<2, X)
// X=ITE((cnt>>2)&1, X<<4, X)
// i.e., if the bit is set in cnt, shift X by that amount of bits, or do nothing otherwise

struct SMT_var* gen_shifter_real (struct ctx* ctx, struct SMT_var* X, struct SMT_var* cnt, bool direction, bool arith)
{
        int w=X->width;

        struct SMT_var* in=X;
        struct SMT_var* out;
        struct SMT_var* tmp;

        // bit vector must have width=2^x, i.e., 8, 16, 32, 64, etc
        // FIXME better func name:
        assert (popcount64c (w)==1);

        int bits_in_selector=mylog2(w);

        for (int i=0; i<bits_in_selector; i++)
        {
                if (direction==false)
                        tmp=gen_shift_left(ctx, in, 1<<i);
                else
                        tmp=gen_shift_right(ctx, in, 1<<i, arith ? MSB_of_SMT_var(X) : ctx->var_always_false->SAT_var);

                out=create_internal_variable(ctx, "tmp", TY_BITVEC, w);

                add_Tseitin_ITE_BV (ctx, cnt->SAT_var+i, tmp->SAT_var, in->SAT_var, out->SAT_var, w);

                in=out;
        };
        // if any bit is set in high part of "cnt" variable, result is 0
        // i.e., if a 8-bit bitvector is shifted by cnt>8, give a zero
        struct SMT_var *disable_shifter=create_internal_variable(ctx, "...", TY_BOOL, 1);
        add_Tseitin_OR_list(ctx, cnt->SAT_var+bits_in_selector, w-bits_in_selector, disable_shifter->SAT_var);

        // 0x80 >>s cnt, where cnt>8, must be 0xff! so fill result with MSB(input)
        struct SMT_var *default_val;
        if (arith==false)
                default_val=gen_const(ctx, 0, w);
        else
                default_val=gen_repeat_from_SAT_var(ctx, MSB_of_SMT_var(X), 1, w);

        return gen_ITE(ctx, disable_shifter, default_val, in);
};

struct SMT_var* gen_shifter (struct ctx* ctx, struct SMT_var* X, struct SMT_var* cnt, bool direction, bool arith)
{
        int w=X->width;

        // FIXME: better func name:
        if (popcount64c (w)!=1)
        {
                // X is not in 2^n form, so extend it
                // RATIONALE: input must be in $2^n$ form, so the shift count will be $n$
                //printf ("%s() width=%d\n", __FUNCTION__, w);
                int new_w=1<<(mylog2(w)+1);
                //printf ("%s() extending it to width=%d\n", __FUNCTION__, new_w);
                X=gen_zero_extend(ctx, X, new_w-w);
                cnt=gen_zero_extend(ctx, cnt, new_w-w);
        }

        struct SMT_var* rt=gen_shifter_real(ctx, X, cnt, direction, arith);

        if (popcount64c (w)!=1)
        {
                // if X is not in 2^n form
                rt=gen_extract (ctx, rt, 0, w);
        };

        return rt;
};

struct SMT_var* gen_BVASHR (struct ctx* ctx, struct SMT_var* X, struct SMT_var* cnt)
{
        return gen_shifter (ctx, X, cnt, true, true);
};
\end{lstlisting}
( \url{\MKURL} )

In other words, we prove equivalence of the expression above and my implementation.

\lstinputlisting[style=customsmt]{proofs/bvashr.smt}