改进lambda代码OCaml会产生断言

Pas*_*uoq 10 ocaml

我想改进为"断言"OCaml 3.12.1构造生成的lambda代码.这是一个例子:

let f x =
    assert (x = 4);
    assert (2 + x = 6);
    assert (x - x = 0);
    exit x
Run Code Online (Sandbox Code Playgroud)

上面的文件longfilename.ml代表了我希望改进lambda代码生成的大型OCaml模块.它编译为:

$ ocamlopt -S longfilename.ml
$ cat longfilename.s
...
    .data
    .quad   3072
_camlLongfilename__2:
    .quad   L100007
    .quad   9
    .quad   9
    .quad   2300
L100007: .L100007:
    .ascii  "longfilename.ml"
    .byte   0
    .data
    .quad   3072
_camlLongfilename__3:
    .quad   L100006
    .quad   7
    .quad   9
    .quad   2300
L100006: .L100006:
    .ascii  "longfilename.ml"
    .byte   0
    .data
    .quad   3072
_camlLongfilename__4:
    .quad   L100005
    .quad   5
    .quad   9
    .quad   2300
L100005: .L100005:
    .ascii  "longfilename.ml"
    .byte   0
...
Run Code Online (Sandbox Code Playgroud)

以上是非常多余的.每个断言可能来自的源文件的名称是重复的.罪魁祸首似乎是bytecomp/translcore.ml:

let assert_failed loc =
  (* [Location.get_pos_info] is too expensive *)
  let fname = match loc.Location.loc_start.Lexing.pos_fname with
              | "" -> !Location.input_name
              | x -> x
  in
  let pos = loc.Location.loc_start in
  let line = pos.Lexing.pos_lnum in
  let char = pos.Lexing.pos_cnum - pos.Lexing.pos_bol in
  Lprim(Praise, [Lprim(Pmakeblock(0, Immutable),
          [transl_path Predef.path_assert_failure;
           Lconst(Const_block(0,
              [Const_base(Const_string fname);
               Const_base(Const_int line);
               Const_base(Const_int char)]))])])
;;
Run Code Online (Sandbox Code Playgroud)

从表面上看,它似乎足以给出一个名称 Const_base(Const_string fname),并使用编译时哈希表来存储和重用它.对于模块内优化,更改可能是可管理的(只要在每个编译单元重置散列表).

我在这里有点超出我的深度,特别是"在每个编译单元重置"部分.任何提示?

gas*_*che 8

OCaml编译器中已经有一种机制可以共享一些常量:查看asmcomp/compilenv.ml及其使用,尤其是structured_constants值的使用asmcomp/cmmgen.ml.我不熟悉这个代码,所以我不确定为什么你的特定用例没有被共享,但似乎在lambda代码Const_base (Const_string foo)Const_immstring foo; 之间存在差异.后者是共享的,也许前者不是.

我不知道预期的语义是什么immstring.编译器内部似乎使用它来编译方法标签(bytecomp/translclass.ml),但是没有暴露给输入语言.

(我怀疑区别是因为字符串是可变的,因此共享用户可见的字符串将是可观察的并且改变程序行为.但字符串常量已经被提升,因此用户已经可以观察到语义不一致的共享.增加用户可见字符串的共享可能仍会因兼容性中断而被拒绝.)

看一下这些直接字符串由常量发射代码(asmcomp/cmmgen.ml:emit_constant)处理的方式,它们就像通常的字符串一样表示,所以也许你可以修改编译器来使用immstringin assert_failed并且事情会起作用.

[编辑OP]

改变Const_base (Const_string fname)Const_immstring fname虽然稍微不兼容,但允许OCaml自行编译,编译Frama-C并且新的Frama-C通过其回归测试.在原始示例中,效果如下,这正是所需的结果:

$ cat longfilename.s 
...
    .data
    .quad   3072
_camlLongfilename__2:
    .quad   L100005
    .quad   9
    .quad   9
    .data
    .quad   3072
_camlLongfilename__3:
    .quad   L100005
    .quad   7
    .quad   9
    .data
    .quad   3072
_camlLongfilename__4:
    .quad   L100005
    .quad   5
    .quad   9
    .quad   2300
L100005: .L100005:
    .ascii  "longfilename.ml"
    .byte   0
Run Code Online (Sandbox Code Playgroud)