LINUX.ORG.RU

Архитектура системы верификации кода драйверов Linux

 , ,


0

2

В статье "Архитектура Linux Driver Verification" (PDF, 700 Кб) представлено описание применимости метода статического анализа кода для проверки корректности драйверов устройств для платформы Linux. Представленный метод позволяет выявить ошибки на основании анализа исходных текстов, без непосредственного выполнения кода. В отличие от традиционных методов тестирования статический анализ кода позволяет проследить сразу все пути выполнения программы, в том числе, редко встречающиеся и сложно воспроизводимые при динамическом тестировании.

Проект Linux Driver Verification является открытым и развивается при участии организации Linux Foundation, Института системного программирования Российской Академии Наук (ИСП РАН) и Федерального агентства РФ по науке и инновациям. Наработки проекта распространяются в рамках лицензии Apache. Дополнительно подготовлен online-сервис для проверки драйверов. Список выявленных при помощи LDV проблем можно посмотреть на данной странице.

>>> Источник

★★★★★

Проверено: Shaman007 ()

Ответ на: комментарий от tailgunner

> Чего вы прицепились к проверке указателя на NULL? Это банальщина.

потому и прицепился, что это банальщина, епрст! разве не понятно?!

*даже* для этой банальщины выдумывают паттерн матчинг и специальный синтаксис для него

а что будет, если продолжить *этот* подход дальше? если отвечать с некоторым пафосом и некоторой натяжкой — получим тот тупик, куда движутся современные языки программирования

Изобразите

кое-что я могу изобразить с помощью зависимых типов, а вот насчет запрета kmalloc(*, GFP_KERNEL) надо подумать

www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от tailgunner

>> switch( !!a + !!b + !!c + !!d )

Вот лично я не понял, что проверяет эта «простая и ясная» проверка.

код *считает* количество ненулевых указателей среди a b c d, и в зависимости от этого выполняет одну из веток свича

корректность/проверка этого кода состоит в том, что

1. в любой ветке не разыменовываются нулевые указатели

2. при всех вариантах нулевых и не-нулевых указателей функция таки возвратит целое (т.е. все варианты рассмотрены)

www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от quasimoto

ыыы! твои простыни невозможно читать

у меня конкретный вопрос: можно ли как-то сделать, чтобы в паттерн-матчинге было не 16 веток, а 5 как у меня?

www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от www_linux_org_ru

у меня конкретный вопрос: можно ли как-то сделать, чтобы в паттерн-матчинге было не 16 веток, а 5 как у меня?

Во-первых, да. Смотри пост, там где test a b c d = ... Похоже на сишный же код? Во-вторых, и тут простыня про паттерн-матчинг и его незначительную роль, а ну я об этом писал уже :)

quasimoto ★★★★ ()
Ответ на: комментарий от www_linux_org_ru

*даже* для этой банальщины выдумывают паттерн матчинг и специальный синтаксис для него

а что будет, если продолжить *этот* подход дальше?

получим тот тупик, куда движутся современные языки программирования

Я тут подумал, что это за эмоция у меня возникает глядя на такое непонимание со стороны людей, которые, вроде бы, любят и статические системы типов и верификацию времени компиляции? Не иначе как facepalm :)

quasimoto ★★★★ ()
Ответ на: комментарий от quasimoto

Не совсем понял этот пример (что мы тут верифицируем?).

1. в любой ветке не разыменовываются нулевые указатели

2. при всех вариантах нулевых и не-нулевых указателей функция таки возвратит целое (т.е. все варианты рассмотрены)

и еще желательно

3. тут нет unreachable code

в качестве аналога, видимо, предлагается намного более простая вещь чем у тебя — пусть у нас вместо возможно-нулевых-указателей есть объекты класс Option[int] (если мы рассматриваем скалу) или MayBe Int (если хаскель)

задача: у нас есть 4 объекта АлгТД MayBe Int

нам надо сделать разные действия в зависимости от количества среди них Nothing (или Just, не важно)

при этом 1, 2, 3 должно проверяться компилятором

допустим, что is_just проверяет на то, что у нас Just, и выдает целое 0 или целое 1

тогда написать

case is_just(a) + is_just(b) + is_just(c) + is_just(d) of
    0 -> x
    1 -> x -- f1 ...
    2 -> x -- f2 ...
    3 -> x -- f3 ...
    4 -> x +. a +. b +. c +. d

мы, как я понимаю, не можем, т.к. x +. a +. b +. c +. d будет типа MayBe Int, так?

з.ы. если бы у нас были шаблоны в хаскеле, то is_just мог бы выдавть MySuperBoolean<1>, дальше сумма объектов MySuperBoolean<3> и MySuperBoolean<1> имела бы тип MySuperBoolean<3+1>, и мы бы поимели полноту матчинга — но заданный чуть выше вопрос это не снимает

www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от quasimoto

> Не иначе как facepalm :)

я так и не понял, как у тебя получается убрать MayBe, и более того, мне кажется так, как ты это делаешь, это сделать в принципе невозможно

www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от www_linux_org_ru

1. в любой ветке не разыменовываются нулевые указатели

Указатели как maybe-подобный тип + тотальные функции = нулевые указатели никогда не разыменовываются.

2. при всех вариантах нулевых и не-нулевых указателей функция таки возвратит целое (т.е. все варианты рассмотрены)

И GHC и agda умеют выводить тотальность. GHC кидает ворнинги (при -Wall), а agda вообще запрещает частичные функции.

3. тут нет unreachable code

В аппликативном программировании нет unreachable code как класса.

предлагается намного более простая вещь чем у тебя ... MayBe Int

У меня как раз это (там есть комментарий про изоморфизм с Maybe Integer, лишняя специфичность тут не помешает).

тогда написать

Лучше так:

countNull :: [Ptr] -> W
countNull = sum . map fn
  where
    fn :: Ptr -> W
    fn = (cast :: B -> W) . (cast :: Ptr -> B)

test a b c d =
  let x = Ptr 777 in
  case countNull [a, b, c, d] of
    0 -> x
    1 -> x
    2 -> x
    3 -> x
    4 -> x +. a +. b +. c +. d

мы, как я понимаю, не можем, т.к. x +. a +. b +. c +. d будет типа MayBe Int, так?

Как я это написал - определил операцию (+.) для типа Ptr. Но не очень думал - какова семантика bad_pointer + (good_pointer x)?

А вообще, смысл конструкции (a + b), где a и b - указатели на int в студию. Я понимаю там сдвиг указателя данное количество байт вверх/вниз, но это.

-- | Pointer arithmetic.
class PtrArith t where
  -- | Shift of a pointer.
  (+.) :: t -> N -> t
  -- | Etc.
  -- ...

instance PtrArith Ptr where
  Null  +. _ = Null
  Ptr x +. y
    | x + y < maxOf word = Ptr $ x + y
    | otherwise          = Null

если бы у нас были шаблоны в хаскеле

Зачем в хаскеле шаблоны? Параметрический полиморфизм, ad-hoc полиморфизм, макросы - всё это покрывается естественными для хаскеля средствами.

quasimoto ★★★★ ()
Ответ на: комментарий от quasimoto

> Как я это написал - определил операцию (+.) для типа Ptr. Но не очень думал - какова семантика bad_pointer + (good_pointer x)?

это ключевой момент (и не нужно простыней, да)

дело в том, что когда у нас is_just(a) + is_just(b) + is_just(c) + is_just(d) == 4, то тогда *все* они хорошие указатели, и *каждый* из них можно превратить в int — bad_pointer-ов вообще нет

вопрос только в том, как ты это объяснишь компилятору хаскеля

www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от www_linux_org_ru

это ключевой момент (и не нужно простыней, да)

Ну так какой ответ на цитируемый вопрос?

Если в сишке можно писать { int *a, *b; a + b } это не значит, что у этого a + b есть нормальная семантика. Я могу себе представить такие хорошие функции:

+ : Prt → ℤ → Ptr   -- shift
- : Ptr → Ptr → ℤ   -- offset

и всё.

дело в том, что когда у нас is_just(a) + is_just(b) + is_just(c) + is_just(d) == 4 то тогда *все* они хорошие указатели

Это довольно странный способ узнать об этом, но, кажется, ты хочешь доказать такое высказывание:

sum : {n m : ℕ} → Vec Bool n → (m ≤ n)

quasimoto ★★★★ ()
Ответ на: комментарий от www_linux_org_ru

бугага

Ах в этом смысле.

if (нашёл целые корни уравнения (x^n + y^n = z^n)) {
    ...
} else {
    ...
}

и давай теперь требуй инструмент статического анализа, который отсечёт unreachable code ;)

quasimoto ★★★★ ()
Ответ на: комментарий от www_linux_org_ru

а еще посмотри внимательно — у меня х это не указатель, а целое

Это я понимаю (shift указателя), но не a + b + c + d. Смысл?

quasimoto ★★★★ ()
Ответ на: комментарий от quasimoto

> Ах в этом смысле.

и давай теперь требуй инструмент статического анализа, который отсечёт unreachable code ;)

киса лол, эпичный слив. Может пояснишь, какие другие смыслы есть?

anonymous ()
Ответ на: комментарий от anonymous

Может пояснишь, какие другие смыслы есть?

Я подумал было на требование от функций быть тотальными. Т.е. покрытие кодом всех вариантов у данного вариантного типа. Ну и невозможность написать код который бы не был аппликацией/абстракцией/локальной специальной формой.

quasimoto ★★★★ ()
Ответ на: комментарий от quasimoto

> Я подумал было на требование от функций быть тотальными. Т.е. покрытие кодом всех вариантов у данного вариантного типа. Ну и невозможность написать код который бы не был аппликацией/абстракцией/локальной специальной формой.

Т.е. покрытие кодом всех вариантов у данного вариантного типа.

Опиши, что ты имел ввиду, на примере функции «const» в прелюдии хаскеля

anonymous ()
Ответ на: комментарий от anonymous

Что я имел ввиду не имеет отношения к unreachable code, т.е. = моя тупость, в данном случае.

quasimoto ★★★★ ()
Ответ на: комментарий от quasimoto

>> запрет использования kmalloc(*, GFP_KERNEL) из прерывания

Вот как раз, два параметрических типа IO и STM с линейными монадическими интерфейсами не могут смешиваться

Ты знаешь много умных слов, браво. Именно поэтому я просил тебя _изобразить_ решения задач, а не сказать «в Хаскелле это как два байта переслать».

У си не позволяет, по чисто историческим причинам (теоретически, нет причин по которым си не мог бы быть безопасным и иметь мощные типы).

Естественно, ты можешь придумать маленькое расширение Си или правило верификации (см. статью).

теоретически, нет причин по которым си не мог бы быть безопасным и иметь мощные типы

*короткая презрительная ругань* Когда уже кто-нибудь из теоретиков спустится с небес и хотя бы попробует сделать юзабельный безопасный Си?

tailgunner ★★★★★ ()
Ответ на: комментарий от www_linux_org_ru

> код *считает* количество ненулевых указателей среди a b c d, и в зависимости от этого выполняет одну из веток свича

Это как раз понятно (и случаи 0 и 4 тоже понятны). Но в 3 из 5 веток нельзя сделать никакого полезного вывода о поступивших аргументах.

Чего вы прицепились к проверке указателя на NULL? Это банальщина.

потому и прицепился, что это банальщина, епрст! разве не понятно?!

Непонятно. Это слишком тривиально, чтобы на этом примере продемострировать что-то полезное.

*даже* для этой банальщины выдумывают паттерн матчинг и специальный синтаксис для него

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

кое-что я могу изобразить с помощью зависимых типов,

Изобрази хоть что-нибудь полезное, а то этот топик стремительно скатывается в CS-мастурбацию.

tailgunner ★★★★★ ()
Ответ на: комментарий от tailgunner

> Это как раз понятно (и случаи 0 и 4 тоже понятны). Но в 3 из 5 веток нельзя сделать никакого полезного вывода о поступивших аргументах.

пусть нулевые указатели означают отсутствие экспериментальных данных, а ненулевые — их наличие (и само данное)

дальше, в зависимости от количества экспериментальных данных, мы, с должным запасом в сторону надежности, вычисляем *a+*b+*c+*d

например, если известно всего одно из них, скажем с, то надежно (надежно с точки зрения дальнейшего применения) можно считать, что сумма по крайней мере не меньше чем *с/10 + *с/5 + *с + *с/5

и так далее — т.е. каждая из функций f1, f2, f3 это такая приличная портянка с разбором случаев и комментариями, почему мы так решили, поэтому нам желательно сделать одну функцию f (в моем примере), которая будет наглядно отсылать к ним

конечно, пример высосан из пальца, но это не значит, что его не нужно рассматривать

*даже* для этой банальщины выдумывают паттерн матчинг и специальный синтаксис для него

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

1. я там недалеко упомянул про пафос и натяжки

2. «не для этого» — да, и это заставляет меня иметь пока не окончательное мнение

3. АлгТД недалеко ушли от этого узкого частного случая

Непонятно. Это слишком тривиально, чтобы на этом примере продемострировать что-то полезное.

я не собирался тут демонстрировать что-то полезное для тебя, а обсудить *подход* бласта как альтернативу подхода скалы и хаскеля

Изобрази хоть что-нибудь полезное, а то этот топик стремительно скатывается в CS-мастурбацию.

1. не скатывается — квазимото известен тем, что постит простыни, когда надо задать вопрос, но это терпимо

2. изображать надо на чем-то; в с++ нет зависимых типов, но если (... простынка...) то можно считать, что они есть (компилятор будет это проверять, ... опять длинная простынка ...)

изобразать видимо надо, причем несколькими способами, только я это буду делать медленно и задумчиво

www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от quasimoto

Это я понимаю (shift указателя), но не a + b + c + d. Смысл?

а ты си знаешь?

у меня там было сложение не указателей, а значений по указателю

читай внимательно: x + *a + *b + *c + *d имеет тип «целое число», а не «указатель на целое»

Это довольно странный способ узнать об этом, но, кажется, ты хочешь доказать такое высказывание: sum : {n m : ℕ} → Vec Bool n → (m ≤ n)

я хочу, чтобы компилятор мог сам до этого догадаться, или, в крайнем случае, я его сравнительно просто к этому подтолкнул

и обязательно он должен давать ошибки на варианты:

  switch( !!a + !!b + !!c + !!d ) {
    case 0: return x;
    case 1: return f1(x, a, b, c, d);
    case 2: return f2(x, a, b, c, d);
    case 4: return f3(x, a, b, c, d); 
    case 3: return x + *a + *b + *c + *d; // null pointer access
  }
  switch( !!a + !!b + !!c + !!d ) { // incomplete switch
    case 0: return x;
    case 1: return f1(x, a, b, c, d);
    case 2: return f2(x, a, b, c, d);
    case 4: return x + *a + *b + *c + *d;
  }
  switch( !!a + !!b + !!c + !!d ) {
    case 0: return x;
    case 1: return f1(x, a, b, c, d);
    case 2: return f2(x, a, b, c, d);
    case 3: return f3(x, a, b, c, d);
    case 4: return x + *a + *b + *c + *d;
    case 5: return x + 1; // unreachable
  }

www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от www_linux_org_ru

> зависимости от количества экспериментальных данных, мы, с должным запасом в сторону надежности, вычисляем *a+*b+*c+*d

Если не проверишь их на NULL - сегфолт, если проверишь - твой неконвенционный switch не нужен.

каждая из функций f1, f2, f3 это такая приличная портянка с разбором случаев и комментариями

ну и что ты сэкономил своим switch?

Изобрази хоть что-нибудь полезное, а то этот топик стремительно скатывается в CS-мастурбацию.

1. не скатывается — квазимото известен тем, что постит простыни, когда надо задать вопрос, но это терпимо

Когда он делает это в темах «о языках вообще» - ладно, там люди понимающие. А здесь топик для приземленных драйверописателей. Если сказал «да, это можно» - приведи пример. Как говориться, картинка стоит тысячи слов.

2. изображать надо на чем-то; в с++ нет зависимых типов

Ну так придумай их.

tailgunner ★★★★★ ()
Ответ на: комментарий от quasimoto

опять же, надо чтобы можно было написать

int f1(int x, int* a, int* b, int* c, int* d)
{
  return x + ( !!a ? *a : !!b ? *b : !!c ? *c : *d )*3/2 ;
}

здесь, очевидно, откуда попало f1 вызывать нельзя, т.к. не проверяется, что d ненулевой (и даже если бы проверялось, не ясно, что выдавать, если он нулевой), однако если f1 сделать допустим вложенной функцией в f, или сделать модуль, который экспортирует только f, но не f1, то компилятор должен быть доволен

www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от tailgunner

> Когда он делает это в темах «о языках вообще» - ладно, там люди понимающие. А здесь топик для приземленных драйверописателей.

нет уж

здесь топик для тех, кто хочет, чтобы в их «языках вообще» тоже можно было получить тот профит, который доступен приземленным драйверописателям, если они юзают бласт и LDV

Если сказал «да, это можно» - приведи пример.

присоединяюсь к твоему пожеланию увидеть примеры на хаскеле

www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от www_linux_org_ru

> присоединяюсь к твоему пожеланию увидеть примеры на хаскеле

Я не желаю видеть примеры на Хаскеле. Я желаю видеть примеры на Си, возможно, расширенном зависимыми типами, или на Си и языке внешнего верификатора. Трёп на остальных языках рассматривается, но не убеждает.

tailgunner ★★★★★ ()
Ответ на: комментарий от quasimoto

> if (нашёл целые корни уравнения (x^n + y^n = z^n)) { и давай теперь требуй инструмент статического анализа, который отсечёт unreachable code

у нас же SMT-solver; варианты:

1. выдавать варнинг или ошибку, пока теорию, необходимую для этого уравнения, в SMT-solver не добавят

2. выдавать варнинг или ошибку, пока then-часть не помечена как «возможно недостижимая»

3. нашёл_целые_корни_уравнения это частичная функция?

3.1. если да, то у нее не хватает аргумента «таймаут, после которого надо перестать искать», и вообще, частичные функции должны отмечаться с соответствующими последствиями для верификации

3.2. если нет, то скорее всего из ее статического анализа видно, что она выдает и true и false

www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от tailgunner

> Ну так придумай их.

есть у меня такой вариант, причем давно придуман, + к этому в случае нерекурсивных функций преобразование в с++, где плюсовый компилятор проверяет то, что должны проверять зависимые типы, но рассказывать долго

бласт я видел давно, не оценил (т.к. его подход другой, чем обычно в ЯП), и забыл

потом я решил, что идея SMT-solver-а это то что надо, и тут, как видишь, бласт снова попался на глаза (правда, остается открытым вопрос, как его «согласовать» с общепринятой системой типов, с теми же АлгТД например)

поэтому я не горю желанием сейчас рассказывать свой вариант зависимых типов

www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от tailgunner

ну и что ты сэкономил своим switch?

вот как это выглядело бы на си с паттерн-матчингом:

int h( maybe<int> a,  maybe<int> b,  maybe<int> c,  maybe<int> d)
{
  int x = g();

  switch( a ) {
    case Nothing:
      switch(b) {
        case Nothing:
          switch(c) {
            case Nothing:
              switch(d) {
                case Nothing: return x;
                case Just(dd): return h1(x, dd);
              }
            case Just(cc):
              switch(d) {
                case Nothing: return h1(x, cc);
                case Just(dd): return h2(x, cc, dd);
              }
          }
        case Just(bb):
          switch(c) {
            case Nothing:
              switch(d) {
                case Nothing: return h1(x, bb);
                case Just(dd): return h2(x, bb, dd);
              }
            case Just(cc):
              switch(d) {
                case Nothing: return h2(x, bb, cc);
                case Just(dd): return h3(x, bb, cc, dd);
              }
          }
      }
    case Just(aa):
      switch(b) {
        case Nothing:
          switch(c) {
            case Nothing:
              switch(d) {
                case Nothing: return h1(x, aa);
                case Just(dd): return h2(x, aa, dd);
              }
            case Just(cc):
              switch(d) {
                case Nothing: return h2(x, aa, cc);
                case Just(dd): return h3(x, aa, cc, dd);
              }
          }
        case Just(bb):
          switch(c) {
            case Nothing:
              switch(d) {
                case Nothing: return h2(x, aa, bb);
                case Just(dd): return h3(x, aa, bb, dd);
              }
            case Just(cc):
              switch(d) {
                case Nothing: return h3(x, aa, bb, cc);
                case Just(dd): return x + aa + bb + cc + dd;
              }
          }
      }
  }
}

отдельные функции h1,h2,h3 немного упрощаются, но это не оправдывает усложения функции h

int f1(int x, int* a, int* b, int* c, int* d)
{
  int not_null = !!a ? *a : !!b ? *b : !!c ? *c : *d;
  return x + not_null * 3 / 2 ;
}
int h1(int x, int not_null)
{
  return x + not_null * 3 / 2 ;
}
www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от www_linux_org_ru

Ты реально ненавидишь паттерн-матчинг.

switch (a, b, c, d) {
case NULL, NULL, NULL, NULL:
        break;
case true, true, true, true:
        break;
case _, _, _, _:
        break;
}

Заметь, что в одной ветке используется NULL, а в другой true - значение указателя преобразуется к логическому, как и положено в Си. Если тебе не нравится идея преобразования:

switch (a != NULL, b != NULL, c != NULL, d != NULL) {
case true, true, true, true:
        break;
case false, false, false, false:
        break;
case _, _, _, _:
        break;
}
tailgunner ★★★★★ ()
Ответ на: комментарий от www_linux_org_ru

> вариантов должно быть 5, и точка

Ну, если нужно _всё в точности_ как у тебя, и напиши так, как сам написал, в чем проблема? То, что ты изначально написал - тоже примитивный паттерн-матчинг, кстати.

tailgunner ★★★★★ ()
Ответ на: комментарий от tailgunner

Ты реально ненавидишь паттерн-матчинг.

возможно, я не умею его готовить :-)

int h( maybe<int> a,  maybe<int> b,  maybe<int> c,  maybe<int> d)
{
  int x = g();

  switch( a; b; c; d ) {
    case Nothing; Nothing; Nothing; Nothing : return x;
    case Just(aa); Nothing; Nothing; Nothing :
    case Nothing; Just(aa); Nothing; Nothing :
    case Nothing; Nothing; Just(aa); Nothing :
    case Nothing; Nothing; Nothing; Just(aa) : return h1(x, aa);
    case Just(aa); Just(bb); Nothing; Nothing :
    case Just(aa); Nothing; Just(bb); Nothing :
    case Just(aa); Nothing; Nothing; Just(bb) :
    case Nothing; Just(aa); Just(bb); Nothing :
    case Nothing; Just(aa); Nothing; Just(bb) :
    case Nothing; Nothing; Just(aa); Just(bb) : return h2(x, aa, bb);
    /* тут мне лень было выписывать 4 варианта правильно*/
    case Just(aa); Nothing; Nothing; Nothing :
    case Nothing; Just(aa); Nothing; Nothing :
    case Nothing; Nothing; Just(aa); Nothing :
    case Nothing; Nothing; Nothing; Just(aa) : return h3(x, aa, bb, cc);
    case Just(aa); Just(bb); Just(cc); Just(dd) : return x+aa+bb+cc+dd;
}
www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от tailgunner

> Ну, если нужно _всё в точности_ как у тебя, и напиши так, как сам написал, в чем проблема? То, что ты изначально написал - тоже примитивный паттерн-матчинг, кстати.

я не понял, где в твоем решении должны вызываться функции h1, h2, h3, и с какими аргументами; свой вариант с твоей идеей я чуть выше запостил

www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от tailgunner

> switch (a, b, c, d)

запятая в си это еще и оператор, поэтому я использовал у себя в примере ";", хотя конечно там просится запятая

www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от www_linux_org_ru

>> Ты реально ненавидишь паттерн-матчинг.

возможно, я не умею его готовить :-)

Ты его именно ненавидишь. Иначе я никак не могу объяснить, что вместо того, чтобы матчить сумму ряда признаков, ты матчишь весь ряд - при том, что для тебя имеет смысл только агрегированное значение.

tailgunner ★★★★★ ()
Ответ на: комментарий от tailgunner

потом мне не нравится провал сквозь ветки, так что это можно было бы записать например так

int h( maybe<int> a,  maybe<int> b,  maybe<int> c,  maybe<int> d)
{
  int x = g(),

  switch( a, b, c, d ) {
    case (Nothing, Nothing, Nothing, Nothing) : return x;
    case (Just(aa), Nothing, Nothing, Nothing),
         (Nothing, Just(aa), Nothing, Nothing),
         (Nothing, Nothing, Just(aa), Nothing),
         (Nothing, Nothing, Nothing, Just(aa)): return h1(x, aa);
    case (Just(aa), Just(bb), Nothing, Nothing),
         (Just(aa), Nothing, Just(bb), Nothing),
         (Just(aa), Nothing, Nothing, Just(bb)),
         (Nothing, Just(aa), Just(bb), Nothing),
         (Nothing, Just(aa), Nothing, Just(bb)),
         (Nothing, Nothing, Just(aa), Just(bb)): return h2(x, aa, bb);
    case (Nothing, Just(aa), Just(bb), Just(cc)),
         (Just(aa), Nothing, Just(bb), Just(cc)),
         (Just(aa), Just(bb), Nothing, Just(cc)),
         (Just(aa), Just(bb), Just(cc), Nothing): return h3(x, aa, bb, cc);
    case (Just(aa), Just(bb), Just(cc), Just(dd)): return x+aa+bb+cc+dd;
}

есть ли вариант лучше?

www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от tailgunner

> Ты его именно ненавидишь. Иначе я никак не могу объяснить, что вместо того, чтобы матчить сумму ряда признаков, ты матчишь весь ряд - при том, что для тебя имеет смысл только агрегированное значение.

непонимаю — я же с самого начала сделал свитч по сумме

напиши свой вариант в любом синтаксисе, только чтобы в нем вызывались h1, h2, h3

www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от www_linux_org_ru

> я же с самого начала сделал свитч по сумме

Видимо, ты не считаешь switch паттерн-матчингом.

напиши свой вариант в любом синтаксисе, только чтобы в нем вызывались h1, h2, h3

Зачем? Пойнт в том, что если тебе нужно матчить сумму - так и делай. И получишь свой изначальный switch, но в синтаксической обертке какого-нибудь паттерн-матчинга.

tailgunner ★★★★★ ()
Ответ на: комментарий от tailgunner

> И получишь свой изначальный switch, но в синтаксической обертке какого-нибудь паттерн-матчинга.

мне кажется. если и получу, то монстра; если ты считаешь иначе — попробуй выкати тут иной вариант

www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от tailgunner

>> я же с самого начала сделал свитч по сумме

Видимо, ты не считаешь switch паттерн-матчингом.

он отличается от обычного паттерн-матчинга тем, что на первый взгляд строка case 4: ... кажется разыменовывающей нулевые указатели, а после анализа — не кажется

бласт такое (ну или аналогичное) умеет, а вот то, что обычно называют паттерн-матчингом — похоже что не умеет

www_linux_org_ru ★★★★★ ()
Ответ на: комментарий от www_linux_org_ru
match one_if_notnull(a) + one_if_notnull(b) + one_if_notnull(c) + one_if_notnull(d) with
0 -> (* whatever *);
1 -> (* whatever *);
2 -> (* whatever *);
3 -> (* whatever *);
end

Функцию one_if_notnull, я надеюсь, писать не нужно? В Си ты ее использовал в виде !!.

Видимо, ты не считаешь switch паттерн-матчингом.

он отличается от обычного паттерн-матчинга

...только своей примитивностью

тем, что на первый взгляд строка case 4: ... кажется разыменовывающей нулевые указатели, а после анализа — не кажется

Паттерн матчинг здесь не причем.

tailgunner ★★★★★ ()
Ответ на: комментарий от www_linux_org_ru

>мы, как я понимаю, не можем, т.к. x +. a +. b +. c +. d будет типа MayBe Int, так?

scala> val l = Some(1) :: None :: Some(2) :: Nil;
l: List[Option[Int]] = List(Some(1), None, Some(2))

scala> l.flatMap(x=>x).foldLeft(0)(_ + _);
res1: Int = 3

r ★★★★★ ()
Вы не можете добавлять комментарии в эту тему. Тема перемещена в архив.