1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
|
open Errors
open Identifiers
module C = Collections
module T = Types
module V = Values
module E = Expressions
module A = CfimAst
open SymbolicAst
let synthesize_symbolic_expansion (sv : V.symbolic_value)
(seel : V.symbolic_expansion option list) (exprl : expression list option) :
expression option =
match exprl with
| None -> None
| Some exprl ->
let ls = List.combine seel exprl in
(* Match on the symbolic value type to know which can of expansion happened *)
let expansion =
match sv.V.sv_ty with
| T.Bool -> (
(* Boolean expansion: there should be two branches *)
match ls with
| [
(Some (V.SeConcrete (V.Bool true)), true_exp);
(Some (V.SeConcrete (V.Bool false)), false_exp);
] ->
ExpandBool (true_exp, false_exp)
| _ -> failwith "Ill-formed boolean expansion")
| T.Integer int_ty ->
(* Switch over an integer: split between the "regular" branches
and the "otherwise" branch (which should be the last branch) *)
let branches, otherwise = C.List.pop_last ls in
(* For all the regular branches, the symbolic value should have
* been expanded to a constant *)
let get_scalar (see : V.symbolic_expansion option) : V.scalar_value
=
match see with
| Some (V.SeConcrete (V.Scalar cv)) ->
assert (cv.V.int_ty = int_ty);
cv
| _ -> failwith "Unreachable"
in
let branches =
List.map (fun (see, exp) -> (get_scalar see, exp)) branches
in
(* For the otherwise branch, the symbolic value should have been left
* unchanged *)
let otherwise_see, otherwise = otherwise in
assert (otherwise_see = None);
(* Return *)
ExpandInt (int_ty, branches, otherwise)
| T.Adt (_, _, _) -> (
(* An ADT expansion can lead to branching: check if this is the case *)
match ls with
| [] -> failwith "Ill-formed ADT expansion"
| [ (see, exp) ] ->
(* No branching *)
ExpandNoBranch (Option.get see, exp)
| ls ->
(* Branching: it is necessarily an enumeration expansion *)
let get_variant (see : V.symbolic_expansion option) :
T.VariantId.id option * V.symbolic_value list =
match see with
| Some (V.SeAdt (vid, fields)) -> (vid, fields)
| _ -> failwith "Ill-formed branching ADT expansion"
in
let exp =
List.map
(fun (see, exp) ->
let vid, fields = get_variant see in
(vid, fields, exp))
ls
in
ExpandEnum exp)
| T.Ref (_, _, _) -> (
(* Reference expansion: there should be one branch *)
match ls with
| [ (Some see, exp) ] -> ExpandNoBranch (see, exp)
| _ -> failwith "Ill-formed borrow expansion")
| T.TypeVar _ | Char | Never | Str | Array _ | Slice _ ->
failwith "Ill-formed symbolic expansion"
in
Some (Expansion (sv, expansion))
let synthesize_symbolic_expansion_no_branching (sv : V.symbolic_value)
(see : V.symbolic_expansion) (expr : expression option) : expression option
=
let exprl = match expr with None -> None | Some expr -> Some [ expr ] in
synthesize_symbolic_expansion sv [ Some see ] exprl
let synthesize_function_call (call_id : call_id) (type_params : T.ety list)
(args : V.typed_value list) (dest : V.symbolic_value)
(expr : expression option) : expression option =
match expr with
| None -> None
| Some expr ->
let call = { call_id; type_params; args; dest } in
Some (FunCall (call, expr))
let synthesize_regular_function_call (fun_id : A.fun_id)
(call_id : V.FunCallId.id) (type_params : T.ety list)
(args : V.typed_value list) (dest : V.symbolic_value)
(expr : expression option) : expression option =
synthesize_function_call (Fun (fun_id, call_id)) type_params args dest expr
let synthesize_unary_op (unop : E.unop) (arg : V.typed_value)
(dest : V.symbolic_value) (expr : expression option) : expression option =
synthesize_function_call (Unop unop) [] [ arg ] dest expr
let synthesize_binary_op (binop : E.binop) (arg0 : V.typed_value)
(arg1 : V.typed_value) (dest : V.symbolic_value) (expr : expression option)
: expression option =
synthesize_function_call (Binop binop) [] [ arg0; arg1 ] dest expr
let synthesize_aggregated_value (aggr_v : V.typed_value)
(expr : expression option) : expression option =
match expr with
| None -> None
| Some expr -> Some (Meta (Aggregate aggr_v, expr))
let synthesize_end_abstraction (abs : V.abs) (expr : expression option) :
expression option =
match expr with
| None -> None
| Some expr -> Some (EndAbstraction (abs, expr))
|
