c - 如何控制 Frama-C 中基本算术类型的大小？

Question

在 Frama-C 中，是否可以自由指定基本类型的大小？

我的目标 TMS320F2808 DSP 具有 16 位字节。char、short 和 int 类型都是一个字节，long 类型是两个。

到目前为止，如果可能的话，我无法看到如何为 Frama-C 指定这些尺寸。

Answer 1

您可能已经发现了该选项-machdep。该命令frama-c -machdep显示一个列表：

$ frama-c -machdep help
[kernel] supported machines are x86_64 x86_32 ppc_32 x86_16.

不幸的是， 的值CHAR_BIT不是 machdep 参数之一。相反，值 8 在 Frama-C 的许多地方被硬编码为CHAR_BIT. 添加对大于 8 of 的值的支持CHAR_BIT是一项微不足道但重复的编程任务：必须简单地识别所有这些位置并修改它们以供使用Bit_utils.sizeofchar()。事实上，已经有人这样做了，所以这绝对是可行的，但这种变化从未回馈给 Frama-C 开发（欢迎来到开源软件的世界）。

完成上述操作后，使用 和 创建新架构CHAR_BIT == 16将sizeof(int) == 1是sizeof(long) == 2一个相对简单的操作。

如何进行更改

我使用以下命令获得了潜在更改站点的第一个列表。这会找到所有出现的数字8：

$ grep -rI \\W8\\W src/*/*.ml
src/ai/base.ml: 8 (* FIXME: CHAR_BIT *), (String.length s)
src/aorai/aorai_register.ml: (* Step 8 : clearing tables which information has been
src/aorai/ltllexer.ml: | 8 ->
src/aorai/promelalexer.ml: | 8 ->
src/aorai/promelalexer_withexps.ml: | 8 ->
src/aorai/yalexer.ml: | 8 ->
src/gui/design.ml: 高度 * 8 / 5 (* 16/10 ratio *)
src/gui/gtk_form.ml: val table = GPack.table ~rows:2 ~col_spacings:8 ~packing ()
src/gui/gtk_helper.ml: ~fallback:"#既不是 UTF-8 也不是语言环境也不是 ISO-8859-15#"
src/gui/gtk_helper.ml: ~to_codeset:"UTF-8"
src/gui/source_manager.ml:(* 尝试将源文件转换为 UTF-8 或语言环境。*)
src/内核/stmts_graph.ml：| 块_-> [`形状`框；`字体大小 8]
src/lib/binary_cache.ml:let cache_size () = 1 lsl (8 + MemoryFootprint.get ())
src/lib/bitvector.ml：如果 ba [I 8]
源代码/逻辑/描述.ml：| IPPredicate(kind,kf,ki,_) -> [I 8;F kf;K ki] @ kind_order kind
src/logic/property.ml: Hashtbl.hash (8, Kf.hash f, Kinstr.hash ki, hash_bhv_loop b)
src/逻辑/property_status.ml：| Never_tried -> [`样式`粗体; `宽度 0.8 ]
src/memory_state/offsetmap.ml：让 char_width = 8 in
src/misc/bit_utils.ml: Int_Base.inject (Int.of_int (warn_if_zero ty (bitsSizeOf ty) / 8))
src/pdg/ctrlDpds.ml: (2) 如果 (c) (3) y = 3; (4) 转到 L；否则 (5) z = 8;
src/pdg/ctrlDpds.ml：（8）L：返回x；
src/pdg/ctrlDpds.ml: (1) -> (2) -> (6) -> (8)
src/printer/cil_printer.ml: Integer.pred (Integer.of_int (8 * (Cil.bytesSizeOfInt k)))
src/printer/cil_printer.ml：当 List.length il >= 8 -> true 时 CompoundInit (_, il)
src/project/state_builder.ml: debug ~level:8 "updating" p;
src/value/builtins_nonfree.ml：Value_parameters.debug “%a 上的 find_ival(8) 返回 %a”
src/value/builtins_nonfree.ml:let int_hrange = Int.two_power_of_int (8 * Cil.theMachine.Cil.theMachine.sizeof_int -1)
src/value/builtins_nonfree_print_c.ml: let step = if iso then 1 else (Integer.to_int modu) / 8 in
src/value/builtins_nonfree_print_c.ml: 让 start = ref ((Integer.to_int bk) / 8) in
src/value/builtins_nonfree_print_c.ml：让 ek = ek / 8 in
src/value/eval_exprs.ml: let offs_bytes = fst (Cil.bitsOffset typ_exp offs) / 8 in
src/value/eval_terms.ml: [i * 8 * sizeof(*tlv)] *)
src/value/value_parameters.ml：（默认为 8；实验性）"
src/wp/Cint.ml: in let hsb p = let n = p lsr 8 in if n = 0 then hsb.(p) else 8 + hsb.(n)
src/wp/GuiPanel.ml: 让 options = GPack.hbox ~spacing:8 ~packing () in
src/wp/GuiPanel.ml: 让 control = GPack.table ~columns:4 ~col_spacings:8 ~rows:2 ~packing () in
src/wp/Matrix.ml: 让 buffer = Buffer.create 8 in
src/wp/cil2cfg.ml：| VblkIn (Bloop s,_) -> (8, s.sid)
src/wp/ctypes.ml: | 8 -> 如果已签名，则为 SInt64，否则为 UInt64
src/wp/ctypes.ml: | 8 -> 浮点64
src/wp/ctypes.ml: | size -> WpLog.not_yet_implemented "%d-bits floats" (8*size)
src/wp/ctypes.ml: 让 m = Array.create 8 None in
src/wp/ctypes.ml: (Cil.bitsSizeOf ctype / 8)
src/wp/ctypes.ml: (Cil.bitsSizeOf ctype / 8)
src/wp/driver.ml: | 8 ->
src/wp/rformat.ml: | 8 ->
src/wp/script.ml: | 8 ->

第一个显然是真阳性，第二个显然是假阳性。在第一种情况下，上下文需要一个 type 的值int。最简单的改变是：

索引：src/ai/base.ml
==================================================== ==================
--- src/ai/base.ml（修订版 24517）
+++ src/ai/base.ml（工作副本）
@@ -116,7 +116,7 @@
   让你，l =
     匹配 s
     | CSString s ->
- 8 (* FIXME: CHAR_BIT *), (String.length s)
+ bitsSizeOf charType, (String.length s)
     | CSWstring s ->
    bitsSizeOf theMachine.wcharType, (List.length s)
   在

在上面的列表中，模式Cil.bitsSizeOf … / 8是8代表的确定标志CHAR_BIT，但在其他情况下，它需要查看源代码并理解意图。

困难来自常数 8 可能采取的不同形式。您可能还会遇到8L，相同的常量但类型为int64. 当该常数表示字符的宽度时，可以将其替换为Int64.of_int (bitsSizeOf charType). 在 src/ai/base.ml 中有一个：

索引：src/ai/base.ml
==================================================== ==================
--- src/ai/base.ml（修订版 24517）
+++ src/ai/base.ml（工作副本）
@@ -156,12 +156,12 @@
     （有趣_x->
        试试 Scanf.sscanf x "%Li-%Li"
          （有趣的最小最大->
- 让 mul8 = Int64.mul 8L in
+ 让 mul_CHAR_BIT = Int64.mul (Int64.of_int (bitsSizeOf charType))
             MinValidAbsoluteAddress.set
- (Abstract_interp.Int.of_int64 (mul8 min));
+ (Abstract_interp.Int.of_int64 (mul_CHAR_BIT min));
             MaxValidAbsoluteAddress.set
               （Abstract_interp.Int.of_int64
- (Int64.pred (mul8 (Int64.succ max)))))
+ (Int64.pred (mul_CHAR_BIT (Int64.succ max)))))
        与 End_of_file | Scanf.Scan_failure _ | 失败 _ as e ->
          Kernel.abort "Invalid -absolute-valid-range integer-integer: 每个整数可以是十进制、十六进制 (0x, 0X)、八进制 (0o) 或二进制 (0b) 表示法，并且必须保持 64 位。一个正确的例子是 -absolute-valid-range 1-0xFFFFFF0。@\n错误是 %S@。"
            (Printexc.to_string e))

但是，影响最后一个更改会导致 Frama-C 在使用命令行选项时崩溃-absolute-valid-range，因为当前初始化事物的顺序（前端尚未准备好回答有关char解释命令行参数时的大小的问题）。所以这个特殊的改变必须推迟，并且必须注意该选项将继续假设 8 位字符，直到 Frama-C 重新架构一点。

除了intand int64，Frama-C 还使用多精度（已分配）整数。该类型的常数 8 通常被发现为Int.eight。这个可以替换为对 的调用Bit_utils.sizeofchar，因为此函数返回一个多精度整数。还应检查代码是否有 3 个班次。

Answer 2

Frama-C 使用了machdep的概念，它描述了底层硬件架构。默认情况下没有为您的案例提供合适的 machdep，有时您可以自己制作并将其用于您的分析。不幸的是，这里不是这种情况，因为您无法更改char.

这个答案的其余部分对原始问题没有帮助，因为char目前在 Frama-C 中无法自定义大小。它留给那些想为奇异架构配置 Frama-C 但大小char不是 8 位的人

对于半香草架构，默认的 machdep 不够用，您可以创建一个machdep_custom.ml包含以下内容的文件：

module Mach = struct

  (* Contents of e.g. file cil/src/machdep_x86_32.ml properly modified for your
     architecture. The MSVC configuration is never used by Frama-C, no need
     to edit it (but it must be included). *)

  open Cil_types

  let gcc = {
    version_major    = 1;
    version_minor    = 0;
    version          = "custom machdep";
    (* All types but char and long long are 16 bits *)
    sizeof_short     = 2;
    sizeof_int       = 2;
    sizeof_long      = 2;
    sizeof_longlong  = 4;
  (* [...] *)
  }

end

let () = File.new_machdep "custom" (module Mach: Cil.Machdeps)

这将注册您自己的 machdep。您的所有分析都必须开始添加-load-script machdep_custom.ml -machdep custom到您的命令行。

由于技术原因，在 Frama-C 中，至少一种类型必须是 32 位。在此示例中，您不可能拥有sizeof(long long)=2.