diff options
| author | Xavier Leroy <xavier.leroy@inria.fr> | 2017-06-12 09:16:10 +0200 |
|---|---|---|
| committer | Xavier Leroy <xavier.leroy@inria.fr> | 2017-06-12 09:16:10 +0200 |
| commit | 446cff1087ffe40d9b19b616162212ca83677515 (patch) | |
| tree | 59ff4611eb11ea7eaccadf0e703baf2696ddb7ce /exportclight/Clightgen.ml | |
| parent | e1de6a1c3c5cbf4c6551d3442e3c4e49145709fb (diff) | |
| download | compcert-kvx-446cff1087ffe40d9b19b616162212ca83677515.tar.gz compcert-kvx-446cff1087ffe40d9b19b616162212ca83677515.zip | |
clightgen: add option -normalize to ensure that memory loads never occur "deep" inside expressions
For example, with this option,
tmp = *(x + 0) + *(x + 1)
in the original Clight is rewritten to
tmp1 = *(x + 0)
tmp2 = *(x + 1)
tmp = tmp1 + tmp2
with two temporaries tmp1 and tmp2 introduced to name the intermediate results of memory loads.
Squashed commit of the following:
commit 3fb69dae567b1305383b74ce1707945f91369a46
commit 0071654b77a239c00bcbb92a5845447b2c4e9d2a
commit c220ed303d9f3f36cc03c347a77b065a9362c0e7
Diffstat (limited to 'exportclight/Clightgen.ml')
| -rw-r--r-- | exportclight/Clightgen.ml | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml index eddb36e2..4af90179 100644 --- a/exportclight/Clightgen.ml +++ b/exportclight/Clightgen.ml @@ -23,6 +23,10 @@ open Frontend let stdlib_path = ref Configuration.stdlib_path +(* clightgen-specific options *) + +let option_normalize = ref false + (* From CompCert C AST to Clight *) let compile_c_ast sourcename csyntax ofile = @@ -30,7 +34,10 @@ let compile_c_ast sourcename csyntax ofile = match SimplExpr.transl_program csyntax with | Errors.OK p -> begin match SimplLocals.transf_program p with - | Errors.OK p' -> p' + | Errors.OK p' -> + if !option_normalize + then Clightnorm.norm_program p' + else p' | Errors.Error msg -> print_error stderr msg; exit 2 @@ -79,6 +86,7 @@ let usage_string = Recognized source files:\n\ \ .c C source file\n\ Processing options:\n\ +\ -normalize Normalize the generated Clight code w.r.t. loads in expressions\n\ \ -E Preprocess only, send result to standard output\n"^ prepro_help ^ "Language support options (use -fno-<opt> to turn off -f<opt>) :\n\ @@ -124,7 +132,8 @@ let cmdline_actions = Exact "-version", Unit print_version_and_exit; Exact "--version", Unit print_version_and_exit; (* Processing options *) - Exact "-E", Set option_E;] + Exact "-E", Set option_E; + Exact "-normalize", Set option_normalize] (* Preprocessing options *) @ prepro_actions @ (* Language support options -- more below *) |