1. C++ / Говнокод #20095

    0

    1. 01
    2. 02
    3. 03
    4. 04
    5. 05
    6. 06
    7. 07
    8. 08
    9. 09
    10. 10
    11. 11
    12. 12
    13. 13
    14. 14
    15. 15
    16. 16
    17. 17
    18. 18
    19. 19
    20. 20
    21. 21
    22. 22
    23. 23
    24. 24
    25. 25
    26. 26
    27. 27
    28. 28
    29. 29
    30. 30
    31. 31
    32. 32
    33. 33
    34. 34
    35. 35
    36. 36
    37. 37
    38. 38
    39. 39
    40. 40
    41. 41
    42. 42
    43. 43
    44. 44
    45. 45
    46. 46
    47. 47
    48. 48
    49. 49
    50. 50
    51. 51
    52. 52
    53. 53
    54. 54
    55. 55
    56. 56
    57. 57
    58. 58
    59. 59
    60. 60
    61. 61
    62. 62
    63. 63
    64. 64
    65. 65
    66. 66
    67. 67
    68. 68
    69. 69
    //...
          /* See if this is something like X * C - X or vice versa or
    	 if the multiplication is written as a shift.  If so, we can
    	 distribute and make a new multiply, shift, or maybe just
    	 have X (if C is 2 in the example above).  But don't make
    	 something more expensive than we had before.  */
    
          if (SCALAR_INT_MODE_P (mode))
    	{
    	  rtx lhs = op0, rhs = op1;
    
    	  wide_int coeff0 = wi::one (GET_MODE_PRECISION (mode));
    	  wide_int coeff1 = wi::one (GET_MODE_PRECISION (mode));
    
    	  if (GET_CODE (lhs) == NEG)
    	    {
    	      coeff0 = wi::minus_one (GET_MODE_PRECISION (mode));
    	      lhs = XEXP (lhs, 0);
    	    }
    	  else if (GET_CODE (lhs) == MULT
    		   && CONST_SCALAR_INT_P (XEXP (lhs, 1)))
    	    {
    	      coeff0 = std::make_pair (XEXP (lhs, 1), mode);
    	      lhs = XEXP (lhs, 0);
    	    }
    	  else if (GET_CODE (lhs) == ASHIFT
    		   && CONST_INT_P (XEXP (lhs, 1))
                       && INTVAL (XEXP (lhs, 1)) >= 0
    		   && INTVAL (XEXP (lhs, 1)) < GET_MODE_PRECISION (mode))
    	    {
    	      coeff0 = wi::set_bit_in_zero (INTVAL (XEXP (lhs, 1)),
    					    GET_MODE_PRECISION (mode));
    	      lhs = XEXP (lhs, 0);
    	    }
    
    	  if (GET_CODE (rhs) == NEG)
    	    {
    	      coeff1 = wi::minus_one (GET_MODE_PRECISION (mode));
    	      rhs = XEXP (rhs, 0);
    	    }
    	  else if (GET_CODE (rhs) == MULT
    		   && CONST_INT_P (XEXP (rhs, 1)))
    	    {
    	      coeff1 = std::make_pair (XEXP (rhs, 1), mode);
    	      rhs = XEXP (rhs, 0);
    	    }
    	  else if (GET_CODE (rhs) == ASHIFT
    		   && CONST_INT_P (XEXP (rhs, 1))
    		   && INTVAL (XEXP (rhs, 1)) >= 0
    		   && INTVAL (XEXP (rhs, 1)) < GET_MODE_PRECISION (mode))
    	    {
    	      coeff1 = wi::set_bit_in_zero (INTVAL (XEXP (rhs, 1)),
    					    GET_MODE_PRECISION (mode));
    	      rhs = XEXP (rhs, 0);
    	    }
    
    	  if (rtx_equal_p (lhs, rhs))
    	    {
    	      rtx orig = gen_rtx_PLUS (mode, op0, op1);
    	      rtx coeff;
    	      bool speed = optimize_function_for_speed_p (cfun);
    
    	      coeff = immed_wide_int_const (coeff0 + coeff1, mode);
    
    	      tem = simplify_gen_binary (MULT, mode, lhs, coeff);
    	      return (set_src_cost (tem, mode, speed)
    		      <= set_src_cost (orig, mode, speed) ? tem : 0);
    	    }
    	}

    https://gcc.gnu.org/viewcvs/gcc/trunk/gcc/simplify-rtx.c?view=markup&pathrev=232689#l2062 здоровенная такая функция из недр GCC, в которой делаются оптимизации, это сродни символьным вычислениям вообще говоря
    https://godbolt.org/g/vcEqe7 но похоже эта хрень работает плохо, не смогло оно выявить тождественность умножения сдвигами и обычного умножения, сведя операции к return 1 в случае функции test1. Но я естественно находил и примеры кода, которые GCC смог успешно "редуцировать" своим оптимизатором, а clang тупил. Говно тут в том, что вместо того, чтобы впилить нормальную систему символьных вычислений, там нагородили какого-то ебучего говна... Хотя может быть я чего-то не понимаю в компиляторах. Надо будет дракона почитать

    Запостил: j123123, 30 Мая 2016

    Комментарии (66) RSS

    • > сведя операции к return 1 в случае функции test12
      fix

      Вообще, этот Register transfer language из gcc https://gcc.gnu.org/onlinedocs/gccint/Arithmetic.html тут описан, ну собственно сами эти арифметические операции
      Ответить
      • https://gcc.gnu.org/bugzilla/show_bug.cgi?id=71343 вот багрепорт еще мой
        Ответить
    • > https://godbolt.org/g/vcEqe7 но похоже эта хрень работает плохо, не смогло оно выявить тождественность умножения сдвигами и обычного умножения, сведя операции к return 1 в случае функции test1.

      > Хотя может быть я чего-то не понимаю в компиляторах.

      Ты чего-то в программировании не понимаешь - если ты думаешь что test() и test2() тождественны.

      Хотя в нынешние времена компилеры начали undefined/unspecified behavior/platform dependent пользоватся как разрешением делать все что угодно.
      Ответить
      • А где они там недождественны? Обрати внимание, что используется unsigned
        Ответить
        • > А где они там недождественны?

          После пяти минут думания - да они тождественны.

          У меня в голове они не тождественны, потому что сдвиг определен в платформе, а умножение в арифметике. И как следствие портабельно и/или платформ-депендент на результат в случае переполнения полагаться нельзя. Но с другой стороны, платформ где что-то может сломаться я не встречал и не слышал.
          Ответить
      • Баг кстати подтвердили
        Confirmed and eventually not helped by factoring *4 early:
        
          return (a << 2) + (b << 2) == (a + b) * 4;
        
        adjusted testcase for that:
        
        unsigned int test12(unsigned int a , unsigned int b)
        {
          unsigned int tem1 = a * 4;
          unsigned int tem2 = b * 4;
          return ((a << 2) + (b << 2)) ==  tem1 + tem2;
        }
        
        also fails to optimize.  In the end this is a missed canonicalization though
        semantically shifts are not always equal to multiplication (they are for
        unsigned arithmetic).
        Ответить
        • на самом деле смешно что они это вообще оптимизируют.

          напомнило: читал что какие-то чудаки пытаются к LLVM/Clang какой solver прикрутить что бы арифметику/этц анализировать/оптимизировать.
          Ответить
          • >на самом деле смешно что они это вообще оптимизируют.

            А почему смешно? Вполне логично ожидать, что такие вещи надо бы заоптимизировать

            >напомнило: читал что какие-то чудаки пытаются к LLVM/Clang какой solver прикрутить что бы арифметику/этц анализировать/оптимизировать.

            Так правильно делают. Но мне LLVM не по нраву, как впрочем и GCC. Читая исходные коды компиляторов, создается впечатление, что вместо того, чтобы определить некий фундамент, например декларативно описать скажем арифметику Пеано и сделать некую универсальную инфраструктуру для символьных вычислений, которая бы даже не была завязана на биты как мельчайшие "ячейки", регистры и проч. а была бы как можно в большей степени универсальной(применимой например для оптимизаци при синтезе логических схем из VDHL и Verilog для FPGA учитывая особенности конкретной ПЛИС-ины), они решают некие частные проблемы (как вот этот пример из simplify_binary_operation_1 в этом говокоде), вручную выписывая правила упрощения. Да, есть еще и dataflow архитектуры, в которых понятия регистров просто нет. https://habrahabr.ru/post/209732/#comment_8710245 с мультиклетом кстати облом вышел, когда под него хотели Clang или GCC адаптировать, архитектура нестандартная слишком, видите ли
            Ответить
            • > > на самом деле смешно что они это вообще оптимизируют.

              > А почему смешно? Вполне логично ожидать, что такие вещи надо бы заоптимизировать

              Вполне логично ожидать, что неговно разраб говна писать не будет, в ожидании что компилер за него это говно сможет разгрести.
              Ответить
              • говно там может быть вызвано какими-нибудь макросами, например. Скажем, кто-то объявил макрос
                #ifdef  someshit
                #define SHIT(a) ((a << 2) + (b << 2))
                #else
                ...
                #endif

                и кто-то им воспользовался
                unsigned int a, b;
                // ...
                b = SHIT(a) - (a * 4 + b * 4);

                почему б тут это не заоптимизировать?
                Ответить
                • повторюсь: "неговно разраб говна писать не будет".

                  да, было бы неплохо если бы компилер магически все мог просекать. нет, я не ожидаю что что-то сильно в ближайшее десятилетие изменится.

                  было бы неплохо если бы какие прикладники что-то типа хаскеля или julia или даже пролога для нормального программирования сделали. а то все это счастье прозябает в своей глубокой математической нише. С/С++ синтакс, SSA, optionally lazy, optionally dynamically/weakly typed и managed. для начала без GC - но и без прямого доступа к памяти. и посмотреть насколько далеко такая концепция - без переизобретания велосипедов - улететь сможет.
                  Ответить
                  • >повторюсь: "неговно разраб говна писать не будет".

                    А если например разрабу по долгу службы доведется иметь дело с подобным говном написанным говноразрабами, а вычищать его слишком долго и дорого, к тому же сроки поджимают?
                    Ответить
                    • медленно уверенно чистить.

                      сроки всегда поджимают. потому что если не поджимают, то какое-то монументальное манаджериал говно на тебя скоро неминуемо свалится.

                      поэтому надо поддержку кода всегда в разработку включать, что бы твои эстимэйты, включали также пару другую часов для чистки. в худшем случае - в секрете от начальства.
                      Ответить
                  • Где это может пригодиться кроме макросов: у нас в проекте куча сгенерированого кода типа трифта, протобуфера, REST'а, RPC, NFS, DHCP и тому подобных оберток над АПИ другой части программы. Такой код писать вручную - бесполезная трата времени програмиста, но почему бы его так же автоматически не оптимизировать?
                    Кроме этого: если пользоваться замечательными языками типа С/С++, то получается дохрена бойлерплейта, который тоже не хочется писать вручную (например, реализовать каждому энумератору метод to_string).

                    Не писать же оптимизатор прямо в кодогенераторе.
                    Ответить
                    • > Не писать же оптимизатор прямо в кодогенераторе.

                      я еще не разу не видел генератора который бы такое Г генерил.

                      с другой стороны, почти все генераторы что-то уже оптимизируют и производят оптимальный код по дезайну: yacc/lex, fsm генераторы, и тот же protobuf. (а враперы они врапперы - там редко что-то соптимизировать можно.)

                      в особенности yacc/lex: у них почти основная цель существования, это генерация оптимального парсера/лексера.

                      ЗЫ
                      > реализовать каждому энумератору метод to_string

                      когда услышал что в С11 добавляют enum'ы - возрадовался. а потом присмотрелся: эти м*даки опять to_string() забыли...
                      Ответить
                      • yacc - фантастическое говно генеририует всилу своей ограниченности. Его код оооочень сильно нуждается в оптимизации. Вообще с кодогенерацией yacc стоит вопрос не "как лучше сгенерировать", а "ну пожалуйста, ну запустись". Хз почему им так любят пользоваться. Возможно потому что он устанавливается легко, или потому что люди которые всю жизнь писали на С/С++ привыкли страдать.
                        Ответить
                        • может быть потому что люди умеют yacc, а ты нет
                          Ответить
                        • "Его код оооочень сильно нуждается в оптимизации."

                          ты вообще в yacc/bison выхлоп заглядывал? там основная часть не код - а соптимизированые таблицы переходов парсера. большая часть кода - это тот код который пользователь сам в автомат добавил. yacc/bison почти исключительно генератор этих таблиц.
                          Ответить
                          • В код - да, заглядывал. Сам по себе факт наличия таблиц ни о какой оптимизации не говорит. Парсер просто так генерирует код, вот и все. Никак эти таблицы не оптимизированые по сравнению с, например, написаными вручную. (В большинстве случаев вручуну написаный парсер использующий такой же алгоритм будет работать быстрее, иногда в разы).

                            Почему так получается: лево-рекурсивные и право-рекурсивные парсеры не определяют порядка в котором правила нужно пробовать применять. И парсер генерирует эти таблицы как угодно. Естесственно, вручную написаный парсер не будет страдать такими недостатками. Но это только вершина айсберга. На самом деле для большинства языков можно было бы пользоваться PEG / DCG, где нет двусмысленности и не нужно ебаться с шифт-редьюс конфликтами. Но это все еще на поверхности. Самая большая проблема говна типа yacc и ANTLR и их аналогов в том, что в их языки не заложена возможность метапрограммирования, нет нормальной возможности сохранить состояние парсера на момент применения правила, нет возможности параметризировать правила. Поэтому АСТ которое эти парсеры создают просто уебищное, и работать с ним нормально невозможно без существенной доработки. Вобщем, это говно хорошо подходит тем, для кого препроцессор Си может заменить макросы с метапрограмированием.
                            Ответить
                            • > АСТ которое эти парсеры создают
                              Не знаю как оригинальный yacc и antlr, но bison вообще не умеет создавать ast (оно создаётся юзером в блоках { ... }).
                              Ответить
                              • Это везде так, более менее, но смысл в другом. Ввод который попадает в эти блоки - максимально бесполезный. Т.е. ничего не известно об этом вводе. В самом простом случае - это, конечно, строка, но, предположим, у нас есть два правила, и мы хотим в третьем использовать результаты этих двух правил - язык не позволяет как-то даже намекнуть на то, что за неведомая херня прилетит в этот блок. Ну а такие вещи как полиморифизм, типа кода правила соеденены "или"...

                                Ну и кроме того, во многих языках АСТ лучше строить не буквально, а с пониманием синтаксиса. Например, если тип переменной встречается через несколько строк от объявления переменной, или когда использование встречается раньше объявления. Для этого желательно иметь доступ к глобальному состоянию парсера и к создаваемой структуре, чтобы внятно проинформировать об ошибке / создать логически вменяемое представление, а не такое, где потом еще хз как искать что где объявлено.
                                Ответить
                                • Там типы же можно задавать у правил и нетерминалов.

                                  А вот с глобальным состоянием - да, проблема. Полное дерево соберётся только в конце, а до этого - просто лес из никак не связанных друг с другом кусков. Впрочем, этим же все восходящие парсеры страдают?
                                  Ответить
                                  • Типы типа
                                    %union { }
                                    %type <x> y

                                    ? Ну он их сам не создает, их нужно самому придумывать как создать. Т.е для сравнения:

                                    foo(d(X)) --> [X], { code_type(X, alpha) }.

                                    Сразу там где нужно, объявили тип, объявили правило для его заполнения, при этом, обявленый тип не мешает никому, и, главное, это тип известен и понятен парсеру, т.е. он на том же языке, что и парсер.

                                    %code {
                                      struct s {
                                        char d;
                                      }
                                    }
                                    %union {
                                      struct s y;
                                    }
                                    %type <s> some_y
                                    
                                    some_y : { /* make sure $1 is alphanumeric... */ } ;


                                    Тип, на самом деле "прозрачен" для парсера (он нихера о его структуре не знает), привязан к другому языку (т.е. на самом деле не yacc, а все та же сишка / сиплюсплюс). Ну и все прелести ручного управления памятью опять же на лицо.
                                    И последнее, в первом варианте, если тип X не буква - все правило отменяется, и пробуется другое. А в yacc - только закат солнца вручную. Если нужен backtracking - нужно городить глобальные переменные, что-то туда запоминать, парсить недораспарсившиеся куски вручную... вобщем пиздец.
                                    Ответить
                                    • я не спец по всем этим алгоритмам парсинга, но по-моему вы пытаетесь конечный автомат переизобрести.

                                      потому что как только в контексте заходит речь о backtracking, это значит что вы что-то очень сильно не правильно делаете. или как называли это светилы прошлого - cancer of semicolon.
                                      Ответить
                                      • Конечный автомат с backtracking вроде не дружит, ибо нет памяти.
                                        Ответить
                                        • "Конечный автомат с backtracking вроде не дружит, ибо нет памяти."

                                          Он концептуально не дружит. Backtracking/этц нужны если у тебя синтакс не однозначный.

                                          Я не знаю чем wvxvw страдает (и он очевидно страдает на пару уровней глубже чем я, мне до него далеко) но по-моему личному опыту если у тебя синтакс не однозначный, то как извращайся, все равно говно получится, потому что даже однозначно специфицировать/задокументировать сложно.
                                          Ответить
                                          • wvxvw страдает потому что он пиздабол. Но пиздабол он настолько хитрый, что все кругом думают что чем до него далеко. А на самом деле он просто хуйню несет с умным видом.

                                            нахуй backtracking для построения AST в данном случае?
                                            Ответить
                                            • > А на самом деле он просто хуйню несет с умным видом.

                                              Абсолютно согласен. Тут я придерживаюсь мнения, выраженного Резерфордом:

                                              "Если учёный не может объяснить уборщице, которая убирается у него в лаборатории, смысл своей работы, то он сам не понимает, что он делает."

                                              @wvxvw же склонен ссылаться на авторитеты и отвечать в духе "Да это же просто моноид в категории эндофункторов, но вы, быдло, всё равно ничего не поймёте, пока не прочитаете книжки A, B и C."
                                              На деле же это мистификации, его можно подловить на незнании элементарнейших вещей, что происходило не раз.
                                              Ответить
                                          • > Он концептуально не дружит. Backtracking/этц нужны если у тебя синтакс не однозначный.
                                            О да... парсеров контекстнонезависимых языков без бэктрекинга просто не бывает. Вопрос не в том, есть он или нет, а можно ли им управлять или нет. yacc - беспомощное говно, т.как у него очень мало возможностей, и все за него нужно дописывать на языке который меньше всего пригоден для работы с граматиками, строками и вообще всем, что нужно для парсера.

                                            Пример, леворекурсивная грамматика: S -> AB | C, A -> a, B -> b, C -> ac. Этот язык не просто однозначный, он вообще регулярный и даже конечный, и тем не менее грамматика нуждается в бектрекинге (не обязательно, можно было другую грамматику написать, но для примера подойдет). Т.е. парсер с вероятностью 50% выберет правило S -> AB, раскроет A -> a, а потом увидит, что следующий символ c, и должен будет вернуться назад и попробовать правило C -> ac.

                                            Конечные автоматы тут как бы вообще не при делах. Я думал это просто эвфемизм такой.
                                            Ответить
                                            • > S -> AB | C, A -> a, B -> b, C -> ac. Этот язык не просто однозначный, он вообще регулярный и даже конечный, и тем не менее грамматика нуждается в бектрекинге

                                              Грамматика кривая. Потому что что у тебя до терминала а можно дойти разными путями.

                                              Или с другой стороны: Как ды думаешь, для чего в языках программирования существуют ключевые слова и пунктуация?

                                              Вот именно для этого и существуют: что бы из тупого парсинга не делать какую-то проблему с экспоненциальной сложностью (или какая там сложность у бэктрэкинга).
                                              Ответить
                                              • И что, что до терминала можно дойти разными путями? В большинстве нетривиальных языков програмирования (т.е. не брейнфак), это норма жизни, иначе на том же yacc вместо 10К строк будет 100К строк write-only говна.

                                                Зачем это может понадобиться? Например, если мне нужно правило которое что-то делает с "а", если за ним идет "б", "в", "г", но не "д", чтобы не писать S -> A | B | C, A -> aa { f(a) }, B -> ab { f(a) }, C -> ac { g(a) }, а S -> AB | C, A -> a { f(a) }, B -> a | b | c, C -> ad. Но, с недопарсерами о таком уровне комфорта можно только мечтать.
                                                Ответить
                                        • опять ты за свое!
                                          почитай про НЕдетерменированный автомат!
                                          почитай про http://www.regular-expressions.info/catastrophic.html

                                          что там по твоемуу? машина тьюринга?
                                          Ответить
                                          • Хуест, НКА все еще КА.
                                            Ответить
                                            • ай умница!
                                              А теперь пиздуй читать как на НКА реализуют бектрекинг:
                                              http://www.cs.may.ie/staff/jpower/Courses/Previous/parsing/node4.html

                                              >>Otherwise we must backtrack to the last state in which we had to choose between two or more transitions, and try selecting a different one.


                                              И напиши на доске читыре раза "бектрекинг реализуется на КА. бектрекинг реализуется на КА.бектрекинг реализуется на КА.бектрекинг реализуется на КА"
                                              Ответить
                                              • Подожди, что ты имеешь в виду под бектрекингом? Что-то вроде (\d+)+ ?
                                                Ответить
                                                • да, такую штуку можно реализовать на НКА
                                                  Вот на ДКА наверное нельзя
                                                  Ответить
                                                  • Для сохранения (\d+) требуется (бесконечная) память, т.к. поток входных символов бесконечен. Число же состояний КА конечно.
                                                    На НКА можно было бы реализовать, если бы повторялась не строка из исходного текста.
                                                    Ответить
                                                    • Ты почитал ссылку?

                                                      Каждый раз когда мы упираемся в несвопадение паттерна, мы возвращаемся на последнюю развилку и идем другим путем. Достаточно на каждой развилке хранить информацию о последнем пути. Время будет расти как-то очень плохо (экспонента будет наверное), но будет работать.

                                                      Другой вариант пойти по всем путям одновременно, разменять время на память.
                                                      Ответить
                                                      • >Ты почитал ссылку?
                                                        Нет.

                                                        >Достаточно на каждой развилке хранить информацию о последнем пути
                                                        Где?

                                                        Еще раз: входная строка бесконечная, количество состояний конечное.
                                                        Ответить
                                                        • >>Нет.
                                                          так почитай
                                                          Ответить
                                                          • Давай ты сначала на мой вопрос постом выше ответишь. Или ты сам не понял того на что ссылку даешь?
                                                            Ответить
                                                            • И тишина.
                                                              Ответить
                                                            • Я не понимаю что ты хочешь услышать.

                                                              Разумеется у любой физической реализации чего угодно есть какие-то ограничения. У машины тьюринга в теории бесконечная память, а на деле нет. У недетерминированного конечного автомата в теории может быть бесконечное число выходов для одного входа, а на практике меньше. Значит, при реализации ты отдводишь на переход N байт, и говоришь что твои регулярки не умеют строки длине миллиарда символов.
                                                              Ответить
                                                              • http://govnokod.ru/20095#comment330241
                                                                >да, такую штуку можно реализовать на НКА
                                                                Пожалуйста, нарисуй мне КА для поиска (\d+)+
                                                                Ответить
                                                                • > (\d+)+
                                                                  И как эта странная регулярка заматчится, к примеру, со строкой "12345"? Что будет захвачено?
                                                                  Ответить
                                                                  • Эта регулярка заматчит, например, 123123123. Не очень удачный пример вышел. Ну пусть будет (\d+){2,}
                                                                    Ответить
                                                                    • ={}=

                                                                      =()=
                                                                      Ответить
                                                                    • Хуестиньо, бамп!
                                                                      Ответить
                                                                    • > Пожалуйста, нарисуй мне КА для поиска (\d+)+
                                                                      > Ну пусть будет (\d+){2,}

                                                                      Пусть на нас движутся икс танков... Нет, икс — это очень мало. Лучше так: пусть на нас движутся игрек танков.
                                                                      Ответить
                                                                    • Ну или давайте так: (\S )+ , т.е. повторяющееся слово
                                                                      Ответить
                                                                      • Гуестиньо, все, сдулся?
                                                                        Ответить
                                                                      • Бамп отсосу анонимуса
                                                                        Ответить
                                                                        • > отсосу анонимуса
                                                                          Фу, Сёма! Предлагай свои услуги на соответствующих ресурсах, а не здесь.
                                                                          Ответить
                                                                          • Кроме "сам дурак" воспиталка ничему не научила? А чего ты вообще отзвякиваешь? Тебя кто-то звал? Я с гуестиньо разговариваю.
                                                                            Ответить
                                                                  • Заматчится в зависимости от того, что именно ожидается от парсера. Если нужно только один какой-то результат, то тут недостаточно данных чтобы его выбрать / существуют неявные соглашения о том, какой результат выбирать.
                                                                    Если компилятору не нужно думать об обобщенных регулярных выражениях, лукахедах и т.п, тогда это оптимизируется в \d+.
                                                                    Ответить
                                                                • \d+ - это "много цифр"

                                                                  (\d+)+ - это "много-много цифр"
                                                                  Ответить
                            • Это всё потому, что у них гомоикон нет.
                              Ответить
            • > определить некий фундамент, например декларативно описать скажем арифметику Пеано и сделать некую универсальную инфраструктуру для символьных вычислений [...] вручную выписывая правила упрощения.

              последний раз когда я баловался с frama-c, на С проекте 80К строк, я её убил после двух часов. потому что ждать достало. (слышал что народ так же солверы убивает потому что память заканчивается. мне с моими 24ГБ просто "повезло".)
              Ответить
              • за меня OOM killer убъет, если что. А frama-c только лишь доказывает какие-то там контракты, производит анализ значений, но не пытается этим что-либо заоптимизировать. Если надо доказывать корректность алгоритма, обслуживающего какие-нибудь АЭС или прошивки из-под авионики, можно и на кластер раскошелиться
                Ответить
                • у frama-c плагиновая архитектура. если память не изменяет, солверы ставятся вместе с frame, но по умолчанию отключены. если не ошибаюсь, там так же есть и более дешевые/быстрые аналайзеры, выхлоп которых вроде бы достаточен для солверов. но я глубоко не копался: frama был первый софт такого характера я видел, и тему полностью я еще не просёк (мат части не хватает).
                  Ответить
                  • >солверы ставятся вместе с frame
                    Ставятся они отдельно. Разве что alt-ergo в комплекте идет. Да и он необязателен вроде как; связано это наверное с тем, что и то и другое на окамле написано, и оно легче интегрируется. Интересно кстати, зачем это все писать на окамле?

                    Там код на Си преобразовывается в некий язык, понятный этим решателям. why3 например умеет с кучей решателей работать через "драйверы", а frama-c умеет транслировать сишный код и прилагаемый к нему контракт в некие теоремы на языке который понимает why3 и который преобразует это уже в конкретные языки из-под конкретных SMT солверов. Там я тоже проблемы находил https://lists.gforge.inria.fr/pipermail/frama-c-discuss/2016-March/005064.html и в багтрекер frama-c что-то репортил...
                    Ответить
                    • другими словами - тогда я вообще framа не понял. (в смысле: анализ и ACSL - да, все остальное - с твоих слов нет.)

                      ЗЫ а до why3 я вообще не дошел.
                      Ответить
                      • Я под why3 свои теоремы пробовал писать даже. Там нет ничего такого уж сложного, в чем нельзя было б разобраться программисту
                        Ответить
    • > Хотя может быть я чего-то не понимаю в компиляторах.

      можешь почитать старые дезайн доки гцц:

      ftp://gcc.gnu.org/pub/gcc/summit/2003/

      в частности про "Tree SSA" - это пред-пред-инфраструктура оптимайзера.
      Ответить
    • Дракон уже не отражает современного состояния компилеров :((
      Ответить

    Добавить комментарий