[CN-Test-Gen] Partial evaluation

Will eventually be pulled out to be more generally usable, see rems-project#447

backend/cn/lib/indexTerms.ml

@@ -1099,3 +1099,97 @@ let nth_array_to_list_facts (binders_terms : (t_bindings * t) list) =
             None)
         arr_lists)
     nths
+
+
+let rec map_term_pre (f : t -> t) (it : t) : t =
+  let (IT (it_, bt, here)) = f it in
+  let loop = map_term_pre f in
+  let it_ : t' =
+    match it_ with
+    | Const _ | Sym _ | Nil _ | SizeOf _ | OffsetOf _ -> it_
+    | Unop (op, it') -> Unop (op, loop it')
+    | Binop (op, it1, it2) -> Binop (op, loop it1, loop it2)
+    | ITE (it_if, it_then, it_else) -> ITE (loop it_if, loop it_then, loop it_else)
+    | EachI (range, it') -> EachI (range, loop it')
+    | Tuple its -> Tuple (List.map loop its)
+    | NthTuple (i, it') -> NthTuple (i, loop it')
+    | Struct (tag, xits) -> Struct (tag, List.map_snd loop xits)
+    | StructMember (it', member) -> StructMember (loop it', member)
+    | StructUpdate ((it_struct, member), it_value) ->
+      StructUpdate ((loop it_struct, member), loop it_value)
+    | Record xits -> Record (List.map_snd loop xits)
+    | RecordMember (it', member) -> RecordMember (loop it', member)
+    | RecordUpdate ((it_struct, member), it_value) ->
+      RecordUpdate ((loop it_struct, member), loop it_value)
+    | Constructor (constr, xits) -> Constructor (constr, List.map_snd loop xits)
+    | MemberShift (it', tag, member) -> MemberShift (loop it', tag, member)
+    | ArrayShift { base; ct; index } ->
+      ArrayShift { base = loop base; ct; index = loop index }
+    | CopyAllocId { addr; loc } -> CopyAllocId { addr = loop addr; loc = loop loc }
+    | Cons (it_head, it_tail) -> Cons (loop it_head, loop it_tail)
+    | Head it' -> Head (loop it')
+    | Tail it' -> Tail (loop it')
+    | NthList (i, xs, d) -> NthList (loop i, loop xs, loop d)
+    | ArrayToList (arr, i, len) -> ArrayToList (loop arr, loop i, loop len)
+    | Representable (ct, it') -> Representable (ct, loop it')
+    | Good (ct, it') -> Good (ct, loop it')
+    | Aligned { t; align } -> Aligned { t = loop t; align = loop align }
+    | WrapI (ct, it') -> WrapI (ct, loop it')
+    | MapConst (bt', it') -> MapConst (bt', loop it')
+    | MapSet (it_m, it_k, it_v) -> MapSet (loop it_m, loop it_k, loop it_v)
+    | MapGet (it_m, it_key) -> MapGet (loop it_m, loop it_key)
+    | MapDef (sbt, it') -> MapDef (sbt, loop it')
+    | Apply (fsym, its) -> Apply (fsym, List.map loop its)
+    | Let ((x, it_v), it_rest) -> Let ((x, loop it_v), loop it_rest)
+    | Match (it', pits) -> Match (loop it', List.map_snd loop pits)
+    | Cast (bt', it') -> Cast (bt', loop it')
+    | HasAllocId it' -> HasAllocId (loop it')
+  in
+  IT (it_, bt, here)
+
+
+let rec map_term_post (f : t -> t) (it : t) : t =
+  let (IT (it_, bt, here)) = it in
+  let loop = map_term_post f in
+  let it_ : t' =
+    match it_ with
+    | Const _ | Sym _ | Nil _ | SizeOf _ | OffsetOf _ -> it_
+    | Unop (op, it') -> Unop (op, loop it')
+    | Binop (op, it1, it2) -> Binop (op, loop it1, loop it2)
+    | ITE (it_if, it_then, it_else) -> ITE (loop it_if, loop it_then, loop it_else)
+    | EachI (range, it') -> EachI (range, loop it')
+    | Tuple its -> Tuple (List.map loop its)
+    | NthTuple (i, it') -> NthTuple (i, loop it')
+    | Struct (tag, xits) -> Struct (tag, List.map_snd loop xits)
+    | StructMember (it', member) -> StructMember (loop it', member)
+    | StructUpdate ((it_struct, member), it_value) ->
+      StructUpdate ((loop it_struct, member), loop it_value)
+    | Record xits -> Record (List.map_snd loop xits)
+    | RecordMember (it', member) -> RecordMember (loop it', member)
+    | RecordUpdate ((it_struct, member), it_value) ->
+      RecordUpdate ((loop it_struct, member), loop it_value)
+    | Constructor (constr, xits) -> Constructor (constr, List.map_snd loop xits)
+    | MemberShift (it', tag, member) -> MemberShift (loop it', tag, member)
+    | ArrayShift { base; ct; index } ->
+      ArrayShift { base = loop base; ct; index = loop index }
+    | CopyAllocId { addr; loc } -> CopyAllocId { addr = loop addr; loc = loop loc }
+    | HasAllocId it' -> HasAllocId (loop it')
+    | Cons (it_head, it_tail) -> Cons (loop it_head, loop it_tail)
+    | Head it' -> Head (loop it')
+    | Tail it' -> Tail (loop it')
+    | NthList (i, xs, d) -> NthList (loop i, loop xs, loop d)
+    | ArrayToList (arr, i, len) -> ArrayToList (loop arr, loop i, loop len)
+    | Representable (ct, it') -> Representable (ct, loop it')
+    | Good (ct, it') -> Good (ct, loop it')
+    | Aligned { t; align } -> Aligned { t = loop t; align = loop align }
+    | WrapI (ct, it') -> WrapI (ct, loop it')
+    | MapConst (bt', it') -> MapConst (bt', loop it')
+    | MapSet (it_m, it_k, it_v) -> MapSet (loop it_m, loop it_k, loop it_v)
+    | MapGet (it_m, it_key) -> MapGet (loop it_m, loop it_key)
+    | MapDef (sbt, it') -> MapDef (sbt, loop it')
+    | Apply (fsym, its) -> Apply (fsym, List.map loop its)
+    | Let ((x, it_v), it_rest) -> Let ((x, loop it_v), loop it_rest)
+    | Match (it', pits) -> Match (loop it', List.map_snd loop pits)
+    | Cast (bt', it') -> Cast (bt', loop it')
+  in
+  f (IT (it_, bt, here))

backend/cn/lib/mucore.ml

@@ -432,3 +432,20 @@ type 'TY file =
     lemmata : (Sym.t * (Locations.t * ArgumentTypes.lemmat)) list;
     call_funinfo : (Sym.t, Sctypes.c_concrete_sig) Pmap.map
   }
+
+let empty_file : 'TY file =
+  { main = None;
+    tagDefs = Pmap.empty Sym.compare;
+    globs = [];
+    funs = Pmap.empty Sym.compare;
+    extern = Pmap.empty Id.compare;
+    stdlib_syms =
+      (let open Set.Make (Sym) in
+       empty);
+    mk_functions = [];
+    resource_predicates = [];
+    logical_predicates = [];
+    datatypes = [];
+    lemmata = [];
+    call_funinfo = Pmap.empty Sym.compare
+  }

backend/cn/lib/mucore.mli

@@ -335,3 +335,5 @@ type 'TY file =
     lemmata : (Sym.t * (Locations.t * ArgumentTypes.lemmat)) list;
     call_funinfo : (Sym.t, Sctypes.c_concrete_sig) Pmap.map
   }
+
+val empty_file : 'TY file