Theory struct_consecutive_init

(*
 * Copyright (c) 2022 Apple Inc. All rights reserved.
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

theory struct_consecutive_init imports
  "AutoCorres2_Main.AutoCorres_Main"
begin


install_C_file "struct_consecutive_init.c"


text ‹Capture C-Ideom to initialize a struct value by a sequence of assignments.
Even when executed within a while loop the dependency of the the initial (unspecified)
value of ▩‹p0› is removed.
In the translation from Simpl to L1 subsequent assignments to the same local variable
are combined and simplified to a constructor application. 
And thus liveness analysis (in translation from L1 to L2) will remove the 
dependency of the inner while loop on ▩‹p0›. Additionally in the optimization phase
of L2 will remove the now superfluous assignment to a unspecified value.

Note that it also works for nested structs. But not for partial initialisation. This would 
require a liveness analysis on the level of struct components and not only on the complete struct.
 ›


autocorres [] "struct_consecutive_init.c"

context l1_corres_in_loop
begin
thm l1_in_loop'_def
thm l1_in_loop'_corres
thm l1_opt_in_loop'_def
end

context l1_definition_string_of_vars
begin
thm l1_opt_string_of_vars'_def
end


context struct_consecutive_init_all_impl
begin

thm nested'_def
thm in_loop_partial'_def [of n m k]
thm in_loop'_def
thm string_of_vars'_def
thm string_of_vars_explode'_def
lemma "in_loop' n m k ≡ 
  do { whileLoop (λi s. i ≤ n)
      (λi. do {modify (G_''_update (λold. 0));
              guard (λs. 0 ≤ 2147483649 + i);
              guard (λs. i ≤ INT_MAX - 1);
              return (i + 1)
           })
      (sint 0);
      gets (λs. sint (G_'' s))
  }"
  by (simp add: in_loop'_def)

lemma "in_loop_nested' n m k ≡ do { whileLoop (λi s. i ≤ n)
                              (λi. do {modify (G_''_update (λold. 0));
                                      guard (λs. 0 ≤ 2147483649 + i);
                                      guard (λs. i ≤ INT_MAX - 1);
                                      return (i + 1)
                                   })
                             0;
                            gets (λs. sint (G_'' s))
                         }"
  by (simp add: in_loop_nested'_def)


lemma "in_loop_partial' n m k ≡ do {p0 <- unknown;
                             whileLoop (λ(i, p0) a. i ≤ n)
                               (λ(i, p0). do {condition (λs. i = 2)
                                               (modify (G_''_update (λold. 0)))
                                               (modify (G_''_update (λold. 0x17)));
                                             guard (λs. 0 ≤ 2147483649 + i);
                                             guard (λs. i ≤ INT_MAX - 1);
                                             return (i + 1, a_C_update (λ_. 0) p0)
                                          })
                              (0, p0);
                             gets (λs. sint (G_'' s))
                          }
"
  by (simp add: in_loop_partial'_def return_bind cong del: whileLoop_cong)
thm partial_declare_before_use'_def
thm nested'_def
thm nested_partial'_def

end

context ts_definition_crosswise_init
begin
thm ts_def
lemma "crosswise_init' ≡ do {
  i ← owhile (λi s. i ≤ (2::32 word)) (λi. oreturn (i + 1)) 0;
  oreturn ()
}"
  unfolding crosswise_init'_def .

end

context ts_definition_cond_init
begin
thm ts_def [no_vars]
lemma "cond_init' i ≡ if i < 0x2A then POINT_C 0x21 0x2C else POINT_C 0x21 0x2A"
  unfolding ts_def .
end

context ts_definition_cond_init1
begin
thm ts_def [no_vars]
lemma "cond_init1' i ≡ if i < 0x2A then POINT_C 0x21 0x2C else POINT_C 0x21 0x2A"
  unfolding ts_def .
end

context ts_definition_cond_init_while
begin
thm ts_def [no_vars]
lemma "cond_init_while' i ≡ do {
  (i, y) ←
    owhile (λ(i, x) s. i < 0x64)
     (λ(i, x).
         oreturn
          (case if i < 0x2A
                then (POINT_C (UCAST(32 → 32 signed) i + 3) (UCAST(32 → 32 signed) i),
                      POINT_C (UCAST(32 → 32 signed) i + 2) (UCAST(32 → 32 signed) i))
                else (POINT_C (UCAST(32 → 32 signed) x + 2) (UCAST(32 → 32 signed) i),
                      POINT_C (UCAST(32 → 32 signed) i + 3) (UCAST(32 → 32 signed) i)) of
           (dst, src) ⇒
             (i + 1,
              x + i + SCAST(32 signed → 32) (a_C src) + SCAST(32 signed → 32) (b_C dst) + SCAST(32 signed → 32) (b_C src) +
              SCAST(32 signed → 32) (a_C dst))))
     (i, 0);
  oreturn y
}"
  unfolding ts_def .
end

context ts_definition_cond_init_while4
begin
thm ts_def [no_vars]
lemma "cond_init_while4' i ≡ do {
  (i, y) ←
    owhile (λ(i, x) s. i < 0x64)
     (λ(i, x).
         oreturn
          (case if i < 0x2A
                then (POINT_C (UCAST(32 → 32 signed) i + 6) (UCAST(32 → 32 signed) i),
                      POINT_C (UCAST(32 → 32 signed) i + 4) (UCAST(32 → 32 signed) i),
                      POINT_C (UCAST(32 → 32 signed) i + 3) (UCAST(32 → 32 signed) i),
                      POINT_C (UCAST(32 → 32 signed) i + 2) (UCAST(32 → 32 signed) i))
                else (POINT_C (UCAST(32 → 32 signed) i + 7) (UCAST(32 → 32 signed) i),
                      POINT_C (UCAST(32 → 32 signed) i + 5) (UCAST(32 → 32 signed) i),
                      POINT_C (UCAST(32 → 32 signed) x + 2) (UCAST(32 → 32 signed) i),
                      POINT_C (UCAST(32 → 32 signed) i + 3) (UCAST(32 → 32 signed) i)) of
           (four, three, dst, src) ⇒
             (i + 1,
              x + i + SCAST(32 signed → 32) (a_C src) + SCAST(32 signed → 32) (b_C dst) +
              SCAST(32 signed → 32) (b_C src) +
              SCAST(32 signed → 32) (a_C dst) +
              SCAST(32 signed → 32) (a_C three) +
              SCAST(32 signed → 32) (b_C three) +
              SCAST(32 signed → 32) (a_C four) +
              SCAST(32 signed → 32) (b_C four))))
     (i, 0);
  oreturn y
}"
  unfolding ts_def .
end

context ts_definition_cond_init_while_nested
begin
thm ts_def [no_vars]
lemma "cond_init_while_nested' i ≡ do {
  (i, y) ←
    owhile (λ(i, x) s. i < 0x64)
     (λ(i, x).
         oreturn
          (case if i < 0x2A
                then (i + 1,
                      x + i + SCAST(32 signed → 32) (UCAST(32 → 32 signed) i + 2) + SCAST(32 signed → 32) (UCAST(32 → 32 signed) i + 3) +
                      SCAST(32 signed → 32) (UCAST(32 → 32 signed) i) +
                      SCAST(32 signed → 32) (UCAST(32 → 32 signed) i) +
                      SCAST(32 signed → 32) (UCAST(32 → 32 signed) i + 4) +
                      SCAST(32 signed → 32) (UCAST(32 → 32 signed) i))
                else (i + 1,
                      x + i + SCAST(32 signed → 32) (UCAST(32 → 32 signed) i + 3) + SCAST(32 signed → 32) (UCAST(32 → 32 signed) i + 4) +
                      SCAST(32 signed → 32) (UCAST(32 → 32 signed) i) +
                      SCAST(32 signed → 32) (UCAST(32 → 32 signed) i) +
                      SCAST(32 signed → 32) (UCAST(32 → 32 signed) i + 5) +
                      SCAST(32 signed → 32) (UCAST(32 → 32 signed) i)) of
           (x, xa) ⇒ (x, xa)))
     (i, 0);
  oreturn y
}"
  unfolding ts_def .
end

end