diff options
| author | Thomas Bauereiss | 2019-03-25 18:56:46 +0000 |
|---|---|---|
| committer | Thomas Bauereiss | 2019-03-26 16:13:02 +0000 |
| commit | 02af1340fe4dcd5da307c9bec6c42982a1f9d969 (patch) | |
| tree | ee1cde9e4b1863fa6f340f98d6c7667e047b202b /src | |
| parent | d9b592b89bd2c47622aa9dbcd0843936322322e3 (diff) | |
Constant-fold __size calls if possible
Diffstat (limited to 'src')
| -rw-r--r-- | src/constant_propagation.ml | 19 |
1 files changed, 16 insertions, 3 deletions
diff --git a/src/constant_propagation.ml b/src/constant_propagation.ml index 1a39b2a1..6caa5ecd 100644 --- a/src/constant_propagation.ml +++ b/src/constant_propagation.ml @@ -622,8 +622,16 @@ let const_props defs ref_vars = (interpreter-based) constant folding. Boolean connectives are special-cased to support short-circuiting when one argument has a suitable value (even if the other one is not constant). + Moreover, calls to a __size function (in particular generated by sizeof + rewriting) with a known-constant return type are replaced by that constant; + e.g., (length(op : bits(32)) : int(32)) becomes 32 even if op is not constant. *) and const_prop_try_fn env (id, args) (l, annot) = + let exp = E_aux (E_app (id, args), (l, annot)) in + let rec is_overload_of f = + Env.get_overloads f env + |> List.exists (fun id' -> Id.compare id id' = 0 || is_overload_of id') + in match (string_of_id id, args) with | "and_bool", ([E_aux (E_lit (L_aux (L_false, _)), _) as e_false; _] | [_; E_aux (E_lit (L_aux (L_false, _)), _) as e_false]) -> @@ -631,9 +639,14 @@ let const_props defs ref_vars = | "or_bool", ([E_aux (E_lit (L_aux (L_true, _)), _) as e_true; _] | [_; E_aux (E_lit (L_aux (L_true, _)), _) as e_true]) -> e_true - | _ -> - let exp = (E_aux (E_app (id, args), (l, annot))) in - if List.for_all Constant_fold.is_constant args then const_fold exp else exp + | _, _ when List.for_all Constant_fold.is_constant args -> + const_fold exp + | _, [arg] when is_overload_of (mk_id "__size") -> + (match destruct_atom_nexp env (typ_of exp) with + | Some (Nexp_aux (Nexp_constant i, _)) -> + E_aux (E_lit (mk_lit (L_num i)), (l, annot)) + | _ -> exp) + | _ -> exp and can_match_with_env env (E_aux (e,(l,annot)) as exp0) cases (substs,ksubsts) assigns = let rec findpat_generic check_pat description assigns = function |