<commit_before>{- |
Module      : Verifier.SAW.Simulator.ANF.Vector
Copyright   : Galois, Inc. 2016
License     : BSD3
Maintainer  : <EMAIL>
Stability   : experimental
Portability : portable

Operations on big-endian vectors of ANF formulas.
-}

module Verifier.SAW.Simulator.ANF.Vector
  ( eq, ule, ult, sle, slt
  , neg, add, sub, mul
  , udiv, urem, sdiv, srem
  , pmul, pmod, pdiv
  , integer
  ) where

import Verifier.SAW.Simulator.ANF.Base (ANF)
import qualified Verifier.SAW.Simulator.ANF.Base as ANF

import Data.Bits
import Data.Vector (Vector)
import qualified Data.Vector as V

type ANFV = Vector ANF

-- | Bitvector equality
eq :: ANFV -> ANFV -> ANF
eq x y = V.foldr ANF.conj ANF.true (V.zipWith ANF.iff x y)

-- | Unsigned less-than-or-equal
ule :: ANFV -> ANFV -> ANF
ule xv yv = go (V.toList xv) (V.toList yv)
  where
    go (x : xs) (y : ys) =
      let z = go xs ys
      in ANF.xor (ANF.conj y z) (ANF.conj (ANF.compl x) (ANF.xor y z))
    go _ _ = ANF.true

-- | Unsigned less-than
ult :: ANFV -> ANFV -> ANF
ult x y = ANF.compl (ule y x)

-- | Signed less-than-or-equal
sle :: ANFV -> ANFV -> ANF
sle = error "unimplemented: sle"

-- | Signed less-than
slt :: ANFV -> ANFV -> ANF
slt = error "unimplemented: slt"

-- | Big-endian bitvector increment with carry
increment :: [ANF] -> (ANF, [ANF])
increment [] = (ANF.true, [])
increment (x : xs) = (ANF.conj x c, ANF.xor x c : ys)
  where (c, ys) = increment xs

-- | Two's complement bitvector negation
neg :: ANFV -> ANFV
neg x = V.fromList (snd (increment (map ANF.compl (V.toList x))))

-- | 1-bit full adder
full_adder :: ANF -> ANF -> ANF -> (ANF, ANF)
full_adder a b c = (carry, ANF.xor (ANF.xor a b) c)
  where carry = ANF.xor (ANF.conj a b) (ANF.conj (ANF.xor a b) c)

-- | Big-endian ripple-carry adder
ripple_carry_adder :: [ANF] -> [ANF] -> ANF -> (ANF, [ANF])
ripple_carry_adder [] _ c = (c, [])
ripple_carry_adder _ [] c = (c, [])
ripple_carry_adder (x : xs) (y : ys) c = (c'', z : zs)
  where (c', zs) = ripple_carry_adder xs ys c
        (c'', z) = full_adder x y c'

-- | Two's complement bitvector addition
add :: ANFV -> ANFV -> ANFV
add x y =
  V.fromList (snd (ripple_carry_adder (V.toList x) (V.toList y) ANF.false))

-- | Two's complement bitvector subtraction
sub :: ANFV -> ANFV -> ANFV
sub x y =
  V.fromList (snd (ripple_carry_adder (V.toList x) (map ANF.compl (V.toList y)) ANF.true))

mul :: ANFV -> ANFV -> ANFV
mul x y = V.foldl f zero y
  where
    zero = V.replicate (V.length x) ANF.false
    f acc c = V.zipWith (ANF.mux c) (add acc2 x) acc2
      where acc2 = V.drop 1 (acc V.++ V.singleton ANF.false)

udiv :: ANFV -> ANFV -> ANFV
udiv = error "unimplemented: udiv"

urem :: ANFV -> ANFV -> ANFV
urem = error "unimplemented: urem"

sdiv :: ANFV -> ANFV -> ANFV
sdiv = error "unimplemented: sdiv"

srem :: ANFV -> ANFV -> ANFV
srem = error "unimplemented: srem"

-- | Polynomial multiplication. Note that the algorithm works the same
-- no matter which endianness convention is used. Result length is
-- @max 0 (m+n-1)@, where @m@ and @n@ are the lengths of the inputs.
pmul :: ANFV -> ANFV -> ANFV
pmul x y = V.generate (max 0 (m + n - 1)) coeff
  where
    m = V.length x
    n = V.length y
    coeff k = foldr ANF.xor ANF.false
      [ ANF.conj (x V.! i) (y V.! j) | i <- [0 .. k], let j = k - i, i < m, j < n ]

-- | Polynomial mod with symbolic modulus. Return value has length one
-- less than the length of the modulus.
-- This implementation is optimized for the (common) case where the modulus
-- is concrete.
pmod :: ANFV -> ANFV -> ANFV
pmod x y = findmsb (V.toList y)
  where
    findmsb :: [ANF] -> ANFV
    findmsb [] = V.replicate (V.length y - 1) ANF.false -- division by zero
    findmsb (c : cs)
      | c == ANF.true = usemask cs
      | c == ANF.false = findmsb cs
      | otherwise = V.zipWith (ANF.mux c) (usemask cs) (findmsb cs)<commit_msg>Implement signed comparisons and div/mod in ANF backend<commit_after>{- |
Module      : Verifier.SAW.Simulator.ANF.Vector
Copyright   : Galois, Inc. 2016
License     : BSD3
Maintainer  : <EMAIL>
Stability   : experimental
Portability : portable

Operations on big-endian vectors of ANF formulas.
-}

module Verifier.SAW.Simulator.ANF.Vector
  ( eq, ule, ult, sle, slt
  , neg, add, sub, mul
  , udiv, urem, sdiv, srem
  , pmul, pmod, pdiv
  , integer
  ) where

import Verifier.SAW.Simulator.ANF.Base (ANF)
import qualified Verifier.SAW.Simulator.ANF.Base as ANF

import Data.Bits
import Data.Vector (Vector)
import qualified Data.Vector as V

type ANFV = Vector ANF

-- | Bitvector equality
eq :: ANFV -> ANFV -> ANF
eq x y = V.foldr ANF.conj ANF.true (V.zipWith ANF.iff x y)

-- | Unsigned less-than-or-equal
ule :: ANFV -> ANFV -> ANF
ule xv yv = go (V.toList xv) (V.toList yv)
  where
    go (x : xs) (y : ys) =
      let z = go xs ys
      in ANF.xor (ANF.conj y z) (ANF.conj (ANF.compl x) (ANF.xor y z))
    go _ _ = ANF.true

-- | Unsigned less-than
ult :: ANFV -> ANFV -> ANF
ult x y = ANF.compl (ule y x)

swap_sign :: ANFV -> ANFV
swap_sign x
  | V.null x = x
  | otherwise = V.singleton (ANF.compl (V.head x)) V.++ V.tail x

-- | Signed less-than-or-equal
sle :: ANFV -> ANFV -> ANF
sle x y = ule (swap_sign x) (swap_sign y)

-- | Signed less-than
slt :: ANFV -> ANFV -> ANF
slt x y = ult (swap_sign x) (swap_sign y)

-- | Big-endian bitvector increment with carry
increment :: [ANF] -> (ANF, [ANF])
increment [] = (ANF.true, [])
increment (x : xs) = (ANF.conj x c, ANF.xor x c : ys)
  where (c, ys) = increment xs

-- | Two's complement bitvector negation
neg :: ANFV -> ANFV
neg x = V.fromList (snd (increment (map ANF.compl (V.toList x))))

-- | 1-bit full adder
full_adder :: ANF -> ANF -> ANF -> (ANF, ANF)
full_adder a b c = (carry, ANF.xor (ANF.xor a b) c)
  where carry = ANF.xor (ANF.conj a b) (ANF.conj (ANF.xor a b) c)

-- | Big-endian ripple-carry adder
ripple_carry_adder :: [ANF] -> [ANF] -> ANF -> (ANF, [ANF])
ripple_carry_adder [] _ c = (c, [])
ripple_carry_adder _ [] c = (c, [])
ripple_carry_adder (x : xs) (y : ys) c = (c'', z : zs)
  where (c', zs) = ripple_carry_adder xs ys c
        (c'', z) = full_adder x y c'

-- | Two's complement bitvector addition
add :: ANFV -> ANFV -> ANFV
add x y =
  V.fromList (snd (ripple_carry_adder (V.toList x) (V.toList y) ANF.false))

-- | Two's complement bitvector subtraction
sub :: ANFV -> ANFV -> ANFV
sub x y =
  V.fromList (snd (ripple_carry_adder (V.toList x) (map ANF.compl (V.toList y)) ANF.true))

mul :: ANFV -> ANFV -> ANFV
mul x y = V.foldl f zero y
  where
    zero = V.replicate (V.length x) ANF.false
    f acc c = V.zipWith (ANF.mux c) (add acc2 x) acc2
      where acc2 = V.drop 1 (acc V.++ V.singleton ANF.false)

-- | Unsigned bitvector division
udiv :: ANFV -> ANFV -> ANFV
udiv x y = fst (udivrem x y)

-- | Unsigned bitvector remainder
urem :: ANFV -> ANFV -> ANFV
urem x y = snd (udivrem x y)

-- | Signed bitvector division
sdiv :: ANFV -> ANFV -> ANFV
sdiv x y = fst (sdivrem x y)

-- | Signed bitvector remainder
srem :: ANFV -> ANFV -> ANFV
srem x y = snd (sdivrem x y)

udivrem :: ANFV -> ANFV -> (ANFV, ANFV)
udivrem dividend divisor = divStep 0 ANF.false initial
  where
    n :: Int
    n = V.length dividend

    -- Given an n-bit dividend and divisor, 'initial' is the starting value of
    -- the 2n-bit "remainder register" that carries both the quotient and remainder;
    initial :: ANFV
    initial = integer n 0 V.++ dividend

    divStep :: Int -> ANF -> ANFV -> (ANFV, ANFV)
    divStep i p rr | i == n = (q `shiftL1` p, r)
      where (r, q) = V.splitAt n rr
    divStep i p rr = divStep (i+1) b (V.zipWith (ANF.mux b) (V.fromList s V.++ q) rs)
      where rs = rr `shiftL1` p
            (r, q) = V.splitAt n rs
            -- Subtract the divisor from the left half of the "remainder register"
            (b, s) = ripple_carry_adder (V.toList r) (map ANF.compl (V.toList divisor)) ANF.true

    shiftL1 :: ANFV -> ANF -> ANFV
    shiftL1 v e = V.tail v `V.snoc` e

sdivrem :: ANFV -> ANFV -> (ANFV, ANFV)
sdivrem = error "sdivrem"

-- | Polynomial multiplication. Note that the algorithm works the same
-- no matter which endianness convention is used. Result length is
-- @max 0 (m+n-1)@, where @m@ and @n@ are the lengths of the inputs.
pmul :: ANFV -> ANFV -> ANFV
pmul x y = V.generate (max 0 (m + n - 1)) coeff
  where
    m = V.length x
    n = V.length y
    coeff k = foldr ANF.xor ANF.false
      [ ANF.conj (x V.! i) (y V.! j) | i <- [0 .. k], let j = k - i, i < m, j < n ]

-- | Polynomial mod with symbolic modulus. Return value has length one
-- less than the length of the modulus.
-- This implementation is optimized for the (common) case where the modulus
-- is concrete.
pmod :: ANFV -> ANFV -> ANFV
pmod x y = findmsb (V.toList y)
  where
    findmsb :: [ANF] -> ANFV
    findmsb [] = V.replicate (V.length y - 1) ANF.false -- division by zero
    findmsb (c : cs)
      | c == ANF.true = usemask cs
      | c == ANF.false = findmsb cs
      | otherwise = V.zipWith (ANF.mux c) (usemask cs) (findmsb cs)
{'fraction_non_alphanumeric': 0.1436500888099467, 'fraction_numerical': 0.004440497335701598, 'mean_word_length': 2.669653767820774, 'pattern_counts': {'":': 0, '<': 11, '<?xml version=': 0, '>': 89, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
{'dir': 'git-commits-cleaned', 'id': '3940869', 'n_tokens_mistral': 3796, 'n_tokens_neox': 3563, 'n_words': 1220}