kouzdra (kouzdra) wrote,
kouzdra
kouzdra

Ну и чтобы завершить sawологию

Пара слов по тому примеру
После того как стало понятно, что основа совинной методы - агрессивное разворачивание кода, в общем-то стало понятно и "как оно это доказывает":

Пример
uint32_t ffs_imp(uint32_t i) {
    char n = 1;
    if (!(i & 0xffff)) { n += 16; i >>= 16; }
    if (!(i & 0x00ff)) { n += 8;  i >>= 8; }
    if (!(i & 0x000f)) { n += 4;  i >>= 4; }
    if (!(i & 0x0003)) { n += 2;  i >>= 2; }
    return (i) ? (n+((i+1) & 0x01)) : 0;
}
превращается в прямолинейный и в общем похожий код (функция (ite c a b) - это if c then a else b):
let { x@1 = Prelude.bitvector 0x20
      x@2 = Prelude.bitvector 0x8
      x@3 = Prelude.bvNat 0x20 0x0
      x@4 = Prelude.bvNat 0x20 0x1
    }
 in \(arg_0 : x@1) ->
      let { x@5 = Prelude.bvEq 0x20 x@3
                    (Prelude.bvAnd 0x20 (Prelude.bvNat 0x20 0xffff) arg_0)
            x@6 = Prelude.bvShr 0x20 arg_0 0x10
            x@7 = Prelude.ite x@1 x@5 x@6 arg_0
            x@8 = Prelude.bvEq 0x20 x@3
                    (Prelude.bvAnd 0x20 (Prelude.bvNat 0x20 0xff) x@7)
            x@9 = Prelude.bvShr 0x20 x@7 0x8
            x@10 = Prelude.ite x@1 x@8 x@9 x@7
            x@11 = Prelude.bvEq 0x20 x@3
                     (Prelude.bvAnd 0x20 (Prelude.bvNat 0x20 0xf) x@10)
            x@12 = Prelude.bvShr 0x20 x@10 0x4
            x@13 = Prelude.ite x@1 x@11 x@12 x@10
            x@14 = Prelude.bvEq 0x20 x@3
                     (Prelude.bvAnd 0x20 (Prelude.bvNat 0x20 0x3) x@13)
            x@15 = Prelude.bvShr 0x20 x@13 0x2
            x@16 = Prelude.ite x@2 x@5 (Prelude.bvNat 0x8 0x11)
                     (Prelude.bvNat 0x8 0x1)
            x@17 = Prelude.ite x@2 x@8
                     (Prelude.slice Prelude.Bool 0x18 0x8 0x0
                        (Prelude.bvAdd 0x20 (Prelude.bvNat 0x20 0x8)
                           (Prelude.bvSExt 0x18 0x7 x@16)))
                     x@16
            x@18 = Prelude.ite x@2 x@11
                     (Prelude.slice Prelude.Bool 0x18 0x8 0x0
                        (Prelude.bvAdd 0x20 (Prelude.bvNat 0x20 0x4)
                           (Prelude.bvSExt 0x18 0x7 x@17)))
                     x@17
          }
       in Prelude.slice Prelude.Bool 0x18 0x8 0x0
            (Prelude.ite x@1
               (Prelude.ite Prelude.Bool x@14 (Prelude.bvEq 0x20 x@3 x@15)
                  (Prelude.ite Prelude.Bool x@11 (Prelude.bvEq 0x20 x@3 x@12)
                     (Prelude.ite Prelude.Bool x@8 (Prelude.bvEq 0x20 x@3 x@9)
                        (Prelude.ite Prelude.Bool x@5
                           (Prelude.bvEq 0x20 x@3 x@6)
                           (Prelude.bvEq 0x20 x@3 arg_0)))))
               x@3
               (Prelude.bvAdd 0x20
                  (Prelude.bvSExt 0x18 0x7
                     (Prelude.ite x@2 x@14
                        (Prelude.slice Prelude.Bool 0x18 0x8 0x0
                           (Prelude.bvAdd 0x20 (Prelude.bvNat 0x20 0x2)
                              (Prelude.bvSExt 0x18 0x7 x@18)))
                        x@18))
                  (Prelude.bvAnd 0x20 x@4
                     (Prelude.bvAdd 0x20 x@4
                        (Prelude.ite x@1 x@14 x@15 x@13)))))

Остальные примерно также - скажем цикл
uint32_t ffs_ref(uint32_t word) {
    int i = 0;
    if(!word)
        return 0;
    for(int cnt = 0; cnt < 32; cnt++)
        if(((1 << i++) & word) != 0)
            return i;
    return 0; // not reached
}

Разворачивается в хтонически выглядящую, но вполне понятную жуть:
let { x@1 = Prelude.bvNat 0x40 0x0
      x@2 = Prelude.bitvector 0x8
      x@3 = Prelude.bvNat 0x8 0x0
}
in
\(arg_0 : Prelude.bitvector 0x20) ->
let { x@4 = Prelude.bvUExt 0x20 0x20 arg_0 } in
Prelude.ite
x@2 Prelude.bvEq 0x20 (Prelude.bvNat 0x20 0x0) arg_0) x@3
(Prelude.ite
 x@2 (Prelude.bvEq 0x40 x@1 (Prelude.bvAnd 0x40 (Prelude.bvNat 0x40 0x1) x@4))
 (Prelude.ite
  x@2 (Prelude.bvEq 0x40 x@1(Prelude.bvAnd 0x40 (Prelude.bvNat 0x40 0x2) x@4))
  (Prelude.ite
   x@2 (Prelude.bvEq 0x40 x@1 (Prelude.bvAnd 0x40 (Prelude.bvNat 0x40 0x4) x@4))
   (Prelude.ite
    x@2 (Prelude.bvEq 0x40 x@1(Prelude.bvAnd 0x40 (Prelude.bvNat 0x40 0x8) x@4))
    ...
    (Prelude.bvEq 0x40 x@1 (Prelude.bvAnd 0x40 (Prelude.bvNat 0x40 0x20000000) x@4))
    (Prelude.ite 
     x@2 (Prelude.bvEq
	  0x40 x@1 (Prelude.bvAnd 0x40 (Prelude.bvNat (Prelude.bvNat 0x8 0xd)) (Prelude.bvNat 0x8 0xc))
	  (Prelude.bvNat 0x8 0xb))
     (Prelude.bvNat 0x8 0xa))
    ...
    (Prelude.bvNat 0x8 0x4))
   (Prelude.bvNat 0x8 0x3))
  (Prelude.bvNat 0x8 0x2))
 (Prelude.bvNat 0x8 0x1))

Проверка эквивалентности двух пусть и весьма навороченных но вполне примитивных формул понятно что вполне в пределах возможностей нынешних доказывалок (главное что умножений и делений нет).

Единственный вопрос котоырй у меня оставался - я некоторое время не понимал, как она справляется с этим вариантом:
uint8_t musl (uint32_t x)
{
  static const char debruijn32[32] = {
    0, 1, 23, 2, 29, 24, 19, 3, 30, 27, 25, 11, 20, 8, 4, 13,
    31, 22, 28, 18, 26, 10, 7, 12, 21, 17, 9, 6, 16, 5, 15, 14
  };
  return x ? debruijn32[(x&-x)*0x076be629 >> 27]+1 : 0;
}

Пока не осознал, что на деле там всего 32 варианта надо разобрать. Что и разбирается обширным if-ом на 32 ветки.

Так что ничего сложного.

Опять же - для желающих посмотреть полные тексты:
ffs.c
ffs.saw
ffs.saw_tree
Tags: saw, verification, Компутерщина, Языки программирования
Subscribe

  • Post a new comment

    Error

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

    When you submit the form an invisible reCAPTCHA check will be performed.
    You must follow the Privacy Policy and Google Terms of use.
  • 0 comments