octalgo.octalgo.static

Require Import fintrees.
Require Import syntax.
Require Import occurrences.
Require Import subs.
Require Import pmatch.
Require Import bSemantics.
Require Import tSemantics.
Require Import monotonicity.
Require Import soundness.
Require Import norec_sem.

Require Import bigop_aux.
Require Import utils.
Require Import finseqs.

Set Implicit Arguments.

Static analysis of a Datalog program

Section analysis.

program to analyze

Variable p : program.

default term and variable for the nth function

Variable dt : term.
Variable dv : 'I_n.

The actual analysis

Section rules.

Definition bigcup_tup {m} {A : finType} (t : m .-tuple {set A }) : {set A } :=
\bigcup_(x <- tval t ) x.

Definition bigcup_cart {m} {A : finType} (s : {set m .-tuple {set A }}) : {set {set A }} :=
[set bigcup_tup y | y : m .-tuple {set A } in s ].

prev is the set of tocs already visited v is the analyzed variable count is the fuel, used for termination The analysis is returned as a DNF, encoded as a set of set of uniq_seqs of toccs. The "outer set" represents the disjunction, whereas the "inner sets" are the conjunctions

Fixpoint analyze_var_prev (prev : (tocs p)) (v : 'I_n) (count : nat) : {set {set (dbranch p )}} :=
  match count with | 0 ⇒ set0 | count.+1 ⇒

    let occs := occsInProgram p v :\: prev in
    let analyze_pi (prev : tocs p) (o : t_occ p) :=

        match p_at o with

         | None ⇒ set0
         | Some f ⇒
            match predtype f with
              | Edb ⇒ [set [set unil ]]
| Idb ⇒ let arec := [set (analyze_var_prev prev (get_cl_var dt dv cl (t_ind o))) count | cl in p & hsym_cl cl == f]
                        in \bigcup_(x in arec ) x
          end
        end
    in
      let all_add_o (dt : {set {set (dbranch p )}}) (o : t_occ p) : {set {set (dbranch p )}}:=
        [set [set pucons o br | br in pred_of_set ct ] | ct in dt ]
      in
      let arec := [seq all_add_o (analyze_pi (occ |: prev) occ) occ | occ <- enum occs ]
    in bigcup_cart (gen_cart_prod arec) end.

Definition analyze_var (v : 'I_n) (count : nat) :=
  analyze_var_prev set0 v count.

End rules.

Completeness results on the analysis

Section completeness.

default t_occ for the nth function (should not be necessary with tnth_map)

Variable docc : t_occ p.

the content of any sequence in the result of an analysis is disjoint

from the given set of previously visited toccs

Lemma analyze_disj (prev : (tocs p)) (v : 'I_n) (count : nat) :
  [∀ ct in analyze_var_prev (prev : (tocs p )) (v : 'I_n) (count : nat),
    [∀ br in pred_of_set ct ,
      [disjoint [set x | x \in (useq br )] & prev ]]].

The analysis is monotonous wrt. its fuel

Lemma analyze_incr prev v (m1 m2 : nat) :
m1 ≤ m2 → analyze_var_prev prev v m1 \subset analyze_var_prev prev v m2.

default ground atom and predicate for the nth function

Variable gat_def : gatom.
Variable df : symtype.

Core result: any no recursion trace is captured by the analysis

Lemma no_rec_capt def prev (tr : trace_sem_trees gat_def) (i : interp) (m : nat) cl s v :
vars_not_shared p
→ prog_safe p
→ prog_safe_hds p
→ safe_edb i
→ only_variables_in_heads p
→ tr \in sem_t p gat_def def m i
→ ABroot (val tr) = inl (RS cl s)
→ v \in tail_vars (body_cl cl)
→ unrec_trace_gen dt dv prev (val tr) v (ABheight (val tr)).+1 \in analyze_var_prev prev v (ABheight (val tr)).

Any no recursion trace is captured in by the analysis with bounded fuel

and empty prev

Theorem no_rec_capt_nf def (tr : trace_sem_trees gat_def) (i : interp) (m : nat) cl s v :
vars_not_shared p
→ prog_safe p
→ prog_safe_hds p
→ safe_edb i
→ only_variables_in_heads p
→ tr \in sem_t p gat_def def m i
→ ABroot (val tr) = inl (RS cl s)
→ v \in tail_vars (body_cl cl)
→ unrec_trace p dt dv (val tr) v (ABheight (val tr)).+1 \in analyze_var v #|rul_gr_finType |.

End completeness.

End analysis.