ModelCoder是一款由迪捷软件自主研发，支持多种嵌入式系统建模并可以自动生成高安全可靠的C代码的软件设计和开发工具。ModelCoder支持同步数据流以及状态机等嵌入式模型，其从模型生成代码的过程经过了形式化验证，以保证生成过程的正确无误性，能够用于飞行控制系统，航空电子系统，核电的DCS等多个安全关键领域的嵌入式软件的设计和开发。
在ModelCoder的核心代码生成器L2c的形式化验证证明过程中，有很多难点。其中之一就是最后一层CtempGen的证明。虽然经过层层化简，已将同步数据流程序Lustre化简到LustreC，其语法语义已经大幅简化；但LustreC与C的语法语义依然有较大的差异。尤其是二者的环境定义差异大，这就给CtempGen层的语义保持证明带来了较大的挑战。而其中能否完成证明的关键就在于二者环境匹配的定义。
LustreC语义的环境定义
LustreC的环境主要包括全局常量环境gc、存储节点本地变量的环境te、存储节点输入参数变量的ta和存储输出参数的e等四部分组成。每一部分都是被定义为locenv。locenv是一个树形存储空间，通过变量id作为存储的索引值，存储每个变量对应的mvl值及其类型。
Definition locenv:= PTree.t (mvl*type).
C语义的环境定义
C的环境主要包括全局环境geC、存储节点本地变量地址的环境eC、存储输入参数的环境leC、存储输出参数的环境teC和存储数据的内存m。
全局环境geC被定义为genv，其中存储着C程序的函数、全局常量和类型。
Definition genv := Genv.t fundef type.
存储节点本地变量地址的环境eC被定义为env，是一个由变量名索引的树形结构，每个叶子节点上存储着该变量在内存中的地址和该变量的类型。
Definition env := PTree.t (block * type).
存储输入参数的环境leC和存储输出参数的环境teC都被定义为temp_env，也是一个由变量名索引的树形结构，每个叶子节点上存储着该变量的值和该变量的类型
Definition temp_env := PTree.t (val*type).
存储数据的内存m被定义为mem，mem是由地址索引的内存块。每个内存块的大小为地址块对应的变量的类型的大小，每个内存块中由偏移映射到memval值。
CtempGen之前各层，已经将Lustre节点的输入输出变量包装到输入输出结构体中，每个输出结构体中还包含子节点的调用实例。所以在C函数执行时定义存储输入结构体的地址为bi，存储输出结构体的地址为bo。
全局常量环境匹配
全局常量的环境匹配定义了LustreC的全局常量环境gc和C的全局环境geC、内存m匹配。
Definition globconsts_match(gc: locenv)(geC: genv)(m: mem): Prop :=
forall id mv ty, gc ! id = Some (mv,ty) ->
(** 如果常量id在LustreC的全局常量环境gc中存储内存段mv和类型ty *)
exists l, Genv.find_symbol geC id = Some l
(** 则存在地址块l，在C的全局环境中能找到id对应的地址块l *)
/\ Plt l bi
(** 全局常量对应的地址块l小于主节点输入结构体所在地址块bi *)
/\ Mem.loadbytes m l 0 (Z_of_nat (length mv)) = Some mv.
(** 利用地址块l和mv的长度从C的内存m中读取的内存段等于mv *)
节点本地变量环境匹配
节点本地变量环境匹配定义了LustreC的节点局部环境te和C的地址环境eC、内存m匹配。
Definition locvars_match(te: locenv)(eC: env)(m: mem)(bs: block)(bl: list (block*(int*type))) : Prop :=
forall id mv ty, te!id = Some (mv,ty) ->
(** 如果变量id在LustreC的局部环境te中存储内存段mv和类型ty *)
exists b, eC!id = Some (b, ty)
(** 则在C的地址环境eC中存储有该id在C内存中的地址块b和类型ty。*)
/\ Ple bs b
(** 地址块b大于等于起始地址块bs *)
/\ ~ In b (map (@fst block (int*type)) bl)
(** 地址块b不在节点输出结构体地址块bl中。*)
/\ Mem.loadbytes m b 0 (sizeof ty) = Some mv.
(** 利用地址块b和类型ty从C的内存m中读取的内存段等于mv。*)
Definition locvars_none(te: locenv)(eC: env): Prop :=
forall id, te ! id = None -> eC ! id = None.
(** 变量不在LustreC的局部环境te中，也不在C的地址环境eC中 *)
节点输入变量环境匹配
节点输入变量环境匹配定义了LustreC的节点输入变量环境ta和C的局部环境leC、内存m匹配。
Definition locargs_match(ta: locenv)(leC: temp_env)(m: mem)(bs: block)(bl: list (block*(int*type))) : Prop :=
forall id mv ty, ta!id = Some (mv,ty) ->
(** 如果变量id在LustreC的输入变量环境ta中存储内存段mv和类型ty *)
exists v vc, load_mvl ty mv Int.zero v
(** 存在LustreC的值v，利用类型ty可从内存段mv中读取值v *)
/\ leC!id = Some (vc,trans_ptype ty)
(** 存在C的值vc，在C的局部环境leC中存储有该id的值vc和类型 *)
/\ arg_blocks_range bs bl vc ty
(** 起始块bs，节点输出结构体地址块bl、C的值vc和类型ty满足arg_blocks_range的性质 *)
/\ val_match m ty v vc.
(** LustreC的值v和C的值vc在内存m中匹配 *)
节点输出变量环境匹配
节点输出变量环境匹配定义了LustreC的节点输出变量环境e和C的返回值环境teC、内存m匹配。
Definition locrets_match(e: locenv)(teC: temp_env)(m: mem)(bl: list (block*(int*type))) : Prop :=
forall id mv ty, e!id = Some (mv,ty) ->
(** 如果变量id在LustreC的自定义环境e中存储内存段mv和类型ty *)
exists l o, teC!id = Some (Vptr l (Ptrofs.of_int o),Tpointer ty)
(** 则在C的返回值环境teC中存储有该id的指针值和类型ty *)
/\ In (l,(o,ty)) bl
(** id在C环境中的指针值在节点输出结构体地址块bl中 *)
/\ Int.unsigned o + Z_of_nat (length mv) <= Int.max_signed
(** 偏移o和内存段mv长度之和小于最大符号数 *)
/\ Mem.loadbytes m l (Int.unsigned o) (sizeof ty) = Some mv
(**利用地址块l、偏移o和类型ty从C的内存m中读取的内存段等于mv *)
/\ Mem.range_perm m l (Int.unsigned o) (Int.unsigned o + sizeof ty) Cur Writable
(** 地址块l、偏移o和类型ty对应的内存m中的位置可写 *)
/\ (alignof ty | Int.unsigned o).
(** 偏移o能整除类型ty的对齐数 *)
由于C的变量的值最终存储与内存m中，所以环境匹配定义中的难点在于：既要使得LustreC中不同类型的变量与C中对应的变量在环境中匹配，又要确保不同类型的变量之间相互隔离。这样才能保证在证明过程中，在内存中修改某个变量的值，既不影响同类型其他变量的值，也不影响不同类型变量的值。
网友评论