Skip to content
Snippets Groups Projects

Compare revisions

Changes are shown as if the source revision was being merged into the target revision. Learn more about comparing revisions.

Source

Select target project
No results found

Target

Select target project
  • burkhart.wolff/Isabelle_C
1 result
Show changes
Commits on Source (47)
Expand all Hide whitespace changes
Inline Side-by-side
Showing
with 1734 additions and 336 deletions
.gitignore
View file @ 4f8f5226
......@@ -8,3 +8,5 @@ C11-BackEnds/Clean_wrapper/output/document
C11-BackEnds/Clean_wrapper/output/document.pdf
C11-FrontEnd/generated/document
C11-FrontEnd/generated/document.pdf
*.thy~
*.thy#
\ No newline at end of file
C11-BackEnds/Clean/examples/Quicksort.thy
View file @ 4f8f5226
......@@ -88,6 +88,7 @@ section\<open>Clean Encoding of the Global State of Quicksort\<close>
global_vars (state)
A :: "int list"
B :: "int list list"
function_spec swap (i::nat,j::nat) \<comment> \<open>TODO: the hovering on parameters produces a number of report equal to the number of \<^ML>\<open>Proof_Context.add_fixes\<close> called in \<^ML>\<open>Function_Specification_Parser.checkNsem_function_spec\<close>\<close>
pre "\<open>i < length A \<and> j < length A\<close>"
......@@ -97,6 +98,15 @@ defines " \<open> tmp := A ! i\<close> ;-
\<open> A := list_update A i (A ! j)\<close> ;-
\<open> A := list_update A j tmp\<close> "
function_spec update_2d_array (i::nat,j::nat, val:: int) \<comment> \<open>TODO: the hovering on parameters produces a number of report equal to the number of \<^ML>\<open>Proof_Context.add_fixes\<close> called in \<^ML>\<open>Function_Specification_Parser.checkNsem_function_spec\<close>\<close>
pre "\<open>i < length A \<and> j < length A\<close>"
post "\<open>\<lambda>res. length A = length(old A) \<and> res = ()\<close>"
local_vars tmp :: int
defines "
\<open> B := list_update B (i+1) (list_update (B!i) j val)\<close>"
find_theorems update_2d_array
find_theorems update_2d_array_core
function_spec partition (lo::nat, hi::nat) returns nat
pre "\<open>lo < length A \<and> hi < length A\<close>"
......@@ -116,6 +126,9 @@ defines " \<open>pivot := A ! hi \<close> ;- \<open>i := lo \<close> ;- \<
call\<^sub>C swap \<open>(i, j)\<close> ;-
return\<^bsub>local_partition_state.result_value_update\<^esub> \<open>i\<close>"
find_theorems partition
term partition
thm partition_core_def
......@@ -137,6 +150,10 @@ thm quicksort_def
thm quicksort_pre_def
thm quicksort_post_def
find_theorems quicksort_core
section\<open>Possible Application Sketch\<close>
lemma quicksort_correct :
......
C11-BackEnds/Clean/src/Clean.thy
View file @ 4f8f5226
......@@ -323,8 +323,8 @@ subsection\<open> The Assignment Operations (embedded in State-Exception Monad)
text\<open>Based on the global variable states, we define \<^term>\<open>break\<close>-aware and \<^term>\<open>return\<close>-aware
version of the assignment. The trick to do this in a generic \<^emph>\<open>and\<close> type-safe way is to provide
the generated accessor and update functions (the ``lens'' representing this global variable,
cf. \<^cite>\<open>"Foster2009BidirectionalPL" and "DBLP:journals/toplas/FosterGMPS07" and
"DBLP:conf/ictac/FosterZW16"\<close>) to the generic assign operators. This pair of accessor and update
cf. \cite{"Foster2009BidirectionalPL" and "DBLP:journals/toplas/FosterGMPS07" and
"DBLP:conf/ictac/FosterZW16"} to the generic assign operators. This pair of accessor and update
carries all relevant semantic and type information of this particular variable and \<^emph>\<open>characterizes\<close>
this variable semantically. Specific syntactic support~\<^footnote>\<open>via the Isabelle concept of
cartouche: \<^url>\<open>https://isabelle.in.tum.de/doc/isar-ref.pdf\<close>\<close> will hide away the syntactic overhead
......@@ -591,6 +591,9 @@ fun mk_Some t = let val some = \<^const_name>\<open>Option.option.Some\<close>
fun dest_listTy (Type(\<^type_name>\<open>List.list\<close>, [T])) = T;
fun is_listTy t = case t of (Type(\<^type_name>\<open>List.list\<close>, [T])) => true
| _ => false
fun mk_hdT t = let val ty = fastype_of t
in Const(\<^const_name>\<open>List.hd\<close>, ty --> (dest_listTy ty)) $ t end
......@@ -605,9 +608,13 @@ fun meta_eq_const T = Const (\<^const_name>\<open>Pure.eq\<close>, T --> T --> p
fun mk_meta_eq (t, u) = meta_eq_const (fastype_of t) $ t $ u;
fun mk_pat_tupleabs [] t = t
| mk_pat_tupleabs [(s,ty)] t = absfree(s,ty)(t)
| mk_pat_tupleabs ((s,ty)::R) t = HOLogic.mk_case_prod(absfree(s,ty)(mk_pat_tupleabs R t));
| mk_pat_tupleabs ((s,ty)::R) t = HOLogic.mk_case_prod(absfree(s,ty)(mk_pat_tupleabs R t))
fun mk_pat_tupleabs_wrapper [] t = absfree("unitparam",@{typ unit}) t
| mk_pat_tupleabs_wrapper R t = mk_pat_tupleabs R t
fun read_constname ctxt n = fst(dest_Const(Syntax.read_term ctxt n))
......@@ -891,7 +898,7 @@ fun typ_2_string_raw (Type(s,[TFree _])) = if String.isSuffix "_scheme" s
fun new_state_record0 add_record_cmd is_global_kind (aS, raw_fields) thy =
let val state_index = (Int.toString o length o Symtab.dest)
(StateMgt_core.get_state_field_tab_global thy)
val state_pos = (Binding.pos_of o #1 o hd) raw_fields
val state_pos = (Binding.pos_of o #1 o hd) raw_fields (*This hd is probably the reason why we cant have empty local vars*)
val ((raw_params, binding), res_ty) = case aS of
SOME d => d
| NONE => (([], Binding.make(state_index,state_pos)), NONE)
......@@ -899,8 +906,6 @@ fun new_state_record0 add_record_cmd is_global_kind (aS, raw_fields) thy =
then mk_global_state_name binding
else mk_local_state_name binding
val raw_parent = SOME(typ_2_string_raw (StateMgt_core.get_state_type_global thy))
val _ = writeln("XXXXX " ^ @{make_string} raw_params ^ "CCC " ^ @{make_string} binding
^ @{make_string} raw_fields)
val pos = Binding.pos_of binding
fun upd_state_typ thy = StateMgt_core.upd_state_type_global
(K (parse_typ_'a (Proof_Context.init_global thy) binding)) thy
......@@ -917,8 +922,8 @@ fun new_state_record0 add_record_cmd is_global_kind (aS, raw_fields) thy =
val add_record_cmd = add_record_cmd0 read_fields;
val add_record_cmd' = add_record_cmd0 pair;
val new_state_record = new_state_record0 add_record_cmd
val new_state_record' = new_state_record0 add_record_cmd';
val new_state_record = new_state_record0 add_record_cmd;
val new_state_record'=new_state_record0 add_record_cmd';
fun clean_ctxt_parser b = Parse.$$$ "("
......@@ -1156,13 +1161,13 @@ structure Function_Specification_Parser =
fun define_cond binding f_sty transform_old check_absence_old cond_suffix params read_cond (ctxt:local_theory) =
let val params' = map (fn(b, ty) => (Binding.name_of b,ty)) params
val src' = case transform_old (read_cond ctxt) of
Abs(nn, sty_pre, term) => mk_pat_tupleabs params' (Abs(nn,sty_pre,term))
| _ => error ("define abstraction for result" ^ Position.here \<^here>)
Abs(nn, sty_pre, term) => mk_pat_tupleabs_wrapper params' (Abs(nn,sty_pre,term))
| a => error ("define abstraction for result" ^ (Position.here \<^here>)^(@{make_string}a))
val bdg = Binding.suffix_name cond_suffix binding
val _ = check_absence_old src'
val bdg_ty = HOLogic.mk_tupleT(map (#2) params) --> f_sty HOLogic.boolT
val eq = mk_meta_eq(Free(Binding.name_of bdg, bdg_ty),src')
val args = (SOME(bdg,NONE,NoSyn), (Binding.empty_atts,eq),[],[])
val args = (SOME(bdg,NONE,NoSyn), (Binding.empty_atts,eq),[],[])
in StateMgt.cmd args ctxt end
fun define_precond binding sty =
......@@ -1177,10 +1182,8 @@ structure Function_Specification_Parser =
val bdg_core_name = Binding.name_of bdg_core
val umty = args_ty --> StateMgt.MON_SE_T @{typ "unit"} sty
val eq = mk_meta_eq(Free (bdg_core_name, umty),mk_pat_tupleabs params' body)
val eq = mk_meta_eq(Free (bdg_core_name, umty),mk_pat_tupleabs_wrapper params' body)
val args_core =(SOME (bdg_core, SOME umty, NoSyn), (Binding.empty_atts, eq), [], [])
in StateMgt.cmd args_core
end
......@@ -1199,7 +1202,7 @@ structure Function_Specification_Parser =
val params' = map (fn(b, ty) => (Binding.name_of b,ty)) params
val measure_term = case read_variant_opt of
NONE => Free(bdg_ord_name,args_ty --> HOLogic.natT)
| SOME f => ((f ctxt) |> mk_pat_tupleabs params')
| SOME f => ((f ctxt) |> mk_pat_tupleabs_wrapper params')
val measure = Const(@{const_name "Wellfounded.measure"}, (args_ty --> HOLogic.natT)
--> argsRelSet )
$ measure_term
......@@ -1208,7 +1211,7 @@ structure Function_Specification_Parser =
--> args_ty --> rmty) $
Free(bdg_ord_name, args_ty --> HOLogic.natT)
else Free(Binding.name_of binding, args_ty --> rmty)
val rhs_main = mk_pat_tupleabs params'
val rhs_main = mk_pat_tupleabs_wrapper params'
(Const(@{const_name "Clean.block\<^sub>C"}, umty --> umty --> rmty --> rmty)
$ Const(read_constname ctxt (Binding.name_of push_name),umty)
$ (Const(read_constname ctxt bdg_core_name, args_ty --> umty)
......@@ -1275,17 +1278,19 @@ val _ = Named_Target.theory_map;
#> define_postcond binding ret_ty sty_old params read_post)
in parse_contract
end
|> StateMgt.new_state_record false (SOME (([],binding), SOME ret_type),locals)
|>(let val v = StateMgt.new_state_record false (SOME (([],binding), SOME ret_type),locals)
in v end)
|> theory_map
(fn params => fn ret_ty => fn ctxt =>
let val sty = StateMgt_core.get_state_type ctxt
let
val sty = StateMgt_core.get_state_type ctxt
val args_ty = HOLogic.mk_tupleT (map snd params)
val mon_se_ty = StateMgt_core.MON_SE_T ret_ty sty
val body = read_body ctxt mon_se_ty
val ctxt' =
if #recursive isrec then
Proof_Context.add_fixes
[(binding, SOME (args_ty --> mon_se_ty), NoSyn)] ctxt |> #2
(Proof_Context.add_fixes
[(binding, SOME (args_ty --> mon_se_ty), NoSyn)] ctxt |> #2)
else
ctxt
val body = read_body ctxt' mon_se_ty
......@@ -1397,7 +1402,7 @@ definition while_C_A :: " (('\<sigma>_ext) control_state_scheme \<Rightarrow> bo
\<Rightarrow> (unit, ('\<sigma>_ext) control_state_ext)MON\<^sub>S\<^sub>E"
where "while_C_A Inv f c B \<equiv> while_C c B"
ML\<open>
structure Clean_Term_interface =
......@@ -1407,40 +1412,37 @@ fun mk_seq_C C C' = let val t = fastype_of C
val t' = fastype_of C'
in Const(\<^const_name>\<open>bind_SE'\<close>, t --> t' --> t') $ C $ C' end;
fun mk_seq_assign_C rhs lhs varname vartyp= let
val t1 = fastype_of rhs
val t2 = fastype_of lhs
in Const(\<^const_name>\<open>bind_SE\<close>, t1 --> (vartyp --> t2) --> t2 ) $ rhs $ absfree (varname, vartyp) lhs end;
fun mk_skip_C sty = Const(\<^const_name>\<open>skip\<^sub>S\<^sub>E\<close>, StateMgt_core.MON_SE_T HOLogic.unitT sty)
fun mk_break sty =
Const(\<^const_name>\<open>break\<close>, StateMgt_core.MON_SE_T HOLogic.unitT sty )
fun mk_return_C upd rhs =
let val ty = fastype_of rhs
val (sty,rty) = case ty of
Type("fun", [sty,rty]) => (sty,rty)
| _ => error "mk_return_C: illegal type for body"
val upd_ty = (HOLogic.listT rty --> HOLogic.listT rty) --> sty --> sty
let val (rty, sty) = case fastype_of upd of Type("fun",[Type("fun", [Type(_(*list*),[r_ty]),_]),Type ("fun",[s_ty,_])]) => (r_ty, s_ty)
| _=>error "mk_return_C: illegal type for update func"
val rhs_ty = sty --> rty
val mty = StateMgt_core.MON_SE_T HOLogic.unitT sty
in Const(\<^const_name>\<open>return\<^sub>C\<close>, upd_ty --> rhs_ty --> mty) $ upd $ rhs end
in Const(\<^const_name>\<open>return\<^sub>C\<close>, fastype_of upd --> rhs_ty --> mty) $ upd $ rhs end
fun mk_assign_global_C upd rhs =
let val ty = fastype_of rhs
val (sty,rty) = case ty of
Type("fun", [sty,rty]) => (sty,rty)
| _ => error "mk_assign_global_C: illegal type for body"
val upd_ty = (rty --> rty) --> sty --> sty
let val (rty, sty) = case fastype_of upd of Type("fun",[Type("fun", [r_ty,_]),Type ("fun",[s_ty,_])]) => (r_ty, s_ty)
| _=>error "mk_assign_global_C: illegal type for update func"
val rhs_ty = sty --> rty
val mty = StateMgt_core.MON_SE_T HOLogic.unitT sty
in Const(\<^const_name>\<open>assign_global\<close>, upd_ty --> rhs_ty --> mty) $ upd $ rhs end
in Const(\<^const_name>\<open>assign_global\<close>, fastype_of upd --> rhs_ty --> mty) $ upd $ rhs end
fun mk_assign_local_C upd rhs =
let val ty = fastype_of rhs
val (sty,rty) = case ty of
Type("fun", [sty,rty]) => (sty,rty)
| _ => error "mk_assign_local_C: illegal type for body"
val upd_ty = (HOLogic.listT rty --> HOLogic.listT rty) --> sty --> sty
let val (rty, sty) = case fastype_of upd of Type("fun",[Type("fun", [Type(_(*list*),[r_ty]),_]),Type ("fun",[s_ty,_])]) => (r_ty, s_ty)
| _=>error "mk_assign_local_C: illegal type for update func"
val rhs_ty = sty --> rty
val mty = StateMgt_core.MON_SE_T HOLogic.unitT sty
in Const(\<^const_name>\<open>assign_local\<close>, upd_ty --> rhs_ty --> mty) $ upd $ rhs end
in Const(\<^const_name>\<open>assign_local\<close>, fastype_of upd --> rhs_ty --> mty) $ upd $ rhs end
fun mk_call_C opn args =
let val ty = fastype_of opn
......@@ -1492,17 +1494,19 @@ end;\<close>
section\<open>Function-calls in Expressions\<close>
text\<open>The precise semantics of function-calls appearing inside expressions is underspecified in C,
text\<open>The precise semantics of function-calls appearing inside expressions is under-specified in C,
which is a notorious problem for compilers and analysis tools. In Clean, it is impossible by
construction --- and the type displine --- to have function-calls inside expressions.
construction --- and the type discipline --- to have function-calls inside expressions.
However, there is a somewhat \<^emph>\<open>recommended coding-scheme\<close> for this feature, which leaves this
issue to decisions in the front-end:
\begin{verbatim}
a = f() + g();
\end{verbatim}
@{verbatim [indent=10, indent=70] \<open>a = f() + g();\<close>}
can be represented in Clean by:
\<open>x \<leftarrow> f(); y \<leftarrow> g(); \<open>a := x + y\<close> \<close> or
\<open>x \<leftarrow> g(); y \<leftarrow> f(); \<open>a := y + x\<close> \<close>
@{cartouche [indent=10, indent=70] \<open>x \<leftarrow> f(); y \<leftarrow> g(); \<open>a := x + y\<close> \<close>} or
@{cartouche [indent=10, indent=70] \<open>x \<leftarrow> g(); y \<leftarrow> f(); \<open>a := y + x\<close> \<close>}
which makes the evaluation order explicit without introducing
local variables or any form of explicit trace on the state-space of the Clean program. We assume,
however, even in this coding scheme, that \<^verbatim>\<open>f()\<close> and \<^verbatim>\<open>g()\<close> are atomic actions; note that this
......
C11-BackEnds/Clean/src/MonadSE.thy
View file @ 4f8f5226
......@@ -69,7 +69,7 @@ syntax (xsymbols)
("(2 _ \<leftarrow> _; _)" [5,8,8]8)
translations
"x \<leftarrow> f; g" == "CONST bind_SE f (% x . g)"
definition unit_SE :: "'o \<Rightarrow> ('o, '\<sigma>)MON\<^sub>S\<^sub>E" ("(result _)" 8)
where "unit_SE e = (\<lambda>\<sigma>. Some(e,\<sigma>))"
notation unit_SE ("unit\<^sub>S\<^sub>E")
......
C11-BackEnds/Clean_wrapper/examples/Coder_Documentation.thy 0 → 100644
View file @ 4f8f5226
(*In this file the current limitations of the translation from C to Clean are shown.*)
theory "Coder_Documentation"
imports
"../src/compiler/Clean_Annotation"
"../src/CleanTranslationHook"
begin
section\<open>Architecture remarks\<close>
text\<open>
The function
@{verbatim [indent=10, margin=70]
\<open>handle_declarations::nodeInfo cTranslationUnit -> Context.generic -> Context.generic\<close>}
can be called with the AST of a translation unit to handle all the definitions. Within that, for every
function the \<open>convertStmt\<close> (CleanCoder) is called to create a translation of the function body.
The \<^verbatim>\<open>setup C_Module.C_Term.map_expression\<close> command handles the C-Term-Antiquotation, which is used for the annotations.
The parsing of the annotation is delayed, for the reason that they need a contet within which sigma (and vars)
are already defined. For that reason, they are stored in \<^verbatim>\<open>Data_Clean_Annotations\<close> as functions with the
signature \<^verbatim>\<open>Context.generic \<rightarrow> term\<close>. This functions are then called when the new context is available.
Additionally the position and function names are saved, which are needed for assigning pre- and postconditions to
the functions and assigning invariants and measures to a loop (via positions).
Importantly, the parsing of the expressions still needs the "old" env because it contains informations
about local vars and parameters, therefore this is saved in the beginning of the \<^verbatim>\<open>map_context_annotation_declaration\<close> function.
The environment is then passed by writing it to the \<^verbatim>\<open>Data_Surrounding_Env\<close> GenericData-store.
To prevent Isabelle from coercing types of returned terms \<^verbatim>\<open>Syntax.parse_term\<close> is used instead of \<^verbatim>\<open>Syntax.read_term\<close>.
Furthermore as parameters are represented as free variables, all constants that would be "selected" through
a parameter name need to be hidden ( \<^verbatim>\<open>remove_params_from_proof\<close>).
\<^bold>\<open>Environment\<close>:
The scope of a parameter now is visible in the environment's var table. It is either "Global", "Local" or "Parameter".
Furthermore each identifier has a field \<^verbatim>\<open>functionArgs\<close> which is an optional list of function parameters.
When an identifier has \<^verbatim>\<open>functionArgs = NONE\<close>, then it is a variable. \<^verbatim>\<open>functionArgs=SOME []\<close> corresponds to a parameterless function.
\<^bold>\<open>Nice to know:\<close>
- The environment of the last completely parsed C-context can be retrieved using \<^verbatim>\<open>C_Module.Data_In_Env\<close>.
- Intermediate envs, containing parameters and local vars can be retrieved using \<^verbatim>\<open>C_Env.Data_Lang.get'\<close>.
See C5.thy in the examples of C11-Frontend.
\<close>
section\<open>Limitations\<close>
text\<open>
\<^item> Only two types are currently mapped to isabelle types,
namely \<^verbatim>\<open>int -> int\<close> and \<^verbatim>\<open>unsigned -> int\<close>.
\<^item> Function calls can only occur as statements or on the right hand side of an assignment.
For example \<^verbatim>\<open>a = b + foo();\<close> is not allowed. This must be rewritten as \<open>tmp = foo(); a=b+tmp;\<close>
Clean and is about to be fixed. The current translation should work for this case then.
\<^item> Scoping: refrain from defining variables more than once. A read/write from a local variable
always affects the most recent definition. Scoping using curly braces does not work as in C!
Example:
@{verbatim [indent=10, margin=70]
\<open>int foo(){
int x = 3;
{
int x = 5;
}
return x; // wrongly returns 5
}\<close>}
Also defining global variables twice within one translation unit will result in only one definition,
thus the second definition does not "reset" the value of the variable
\<^item> Method overloading: Do not use function names multiple times, as this will break the whole
translation process in several ways.
\<close>
section\<open>Some examples\<close>
text\<open>See \<open>Coder_Test_T_Units\<close> for more examples:\<close>
C\<open>
int sum_of_array(int arr[], int length){
int i;
int sum;
i = 0;
sum = 0;
while(i < length){
/*@ inv\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>i\<close> \<le> \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>length\<close>\<close> */
/*@ measure\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>nat \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>length-i\<close>\<close> */
sum = sum + arr[i];
i = i+1;
}
return sum;
}
\<close>
(*look at the annotated while loop - it has the inv as first and the measure as snd argument*)
find_theorems sum_of_array_core
text\<open>The following program would not work in C - Clean admits it however, but produces warnings\<close>
C\<open>
int A[5][4];
int swap_rows(unsigned idx1, unsigned idx2){
int tmp[];
tmp = A[idx1];
A[idx1] = A[idx2];
A[idx2] = tmp;
}
\<close>
find_theorems swap_rows_core
text\<open>A fully annotated multiply\<close>
C\<open>
int multiply(int a, int b){
/*@ pre\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>a\<close> \<ge> 0\<close> */
/*@ post\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<lambda>ret::int. ret = \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>a*b\<close>\<close> */
int sum;
int counter;
sum = 0;
counter = 0;
while(counter < a){
/*@ inv\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>counter*b\<close> = \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>sum\<close> \<and> \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>counter\<close> \<le> \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>a\<close>\<close> */
sum = sum + b;
counter = counter + 1;
}
return sum;
}
\<close>
find_theorems multiply
find_theorems multiply_pre
find_theorems multiply_post
text\<open>A recursive function calculating the factorial of \<open>n\<close>\<close>
C\<open>
int factorial_result;
void factorial(int n){
if(n > 1){
factorial(n-1);
factorial_result = multiply(factorial_result, n);
}else{
factorial_result = 1;
}
}\<close>
find_theorems factorial_core
end
C11-BackEnds/Clean_wrapper/examples/Coder_Test_Env_AEnv.thy
View file @ 4f8f5226
section \<open>Accessing the \<open>C-Environment\<close> and Conversions to the \<open>Clean Environment\<close>\<close>
theory "Coder_Test_Env_AEnv"
imports "../src/CleanCoder"
begin
section \<open>Accessors to C-Env\<close>
subsection \<open>Accessors to \<open>C_Env\<close>\<close>
ML\<open>
fun map_option f (SOME X) = SOME(f X)
......@@ -12,7 +14,7 @@ fun map_option f (SOME X) = SOME(f X)
fun lookup_Cid_info (C_env:C_Module.Data_In_Env.T) id = Symtab.lookup(#idents(#var_table C_env)) id
fun is_global_Cid Cenv Cid = map_option (#global o #3) (lookup_Cid_info Cenv Cid);
fun is_global_Cid Cenv Cid = map_option (#scope o #3) (lookup_Cid_info Cenv Cid);
fun is_fun_Cid Cenv Cid = map_option ((fn [C_Ast.CFunDeclr0 _] => true | _ => false)
o (#params o #3))
(lookup_Cid_info Cenv Cid);
......@@ -27,8 +29,9 @@ C11_Ast_Lib.toString_nodeinfo;
C_Ast.SS_base
\<close>
section \<open>Global Variables, Local Variables, and Local Parameters\<close>
subsection\<open>An Environment Spy\<close>
subsection \<open>Global Variables, Local Variables, and Local Parameters\<close>
subsubsection\<open>An Environment Spy\<close>
ML\<open>
val ENV = Unsynchronized.ref (@{C\<^sub>e\<^sub>n\<^sub>v})
......@@ -38,7 +41,6 @@ fun print_env' s _ stack _ env thy =
in thy end
\<close>
ML\<open>open Position\<close>
setup \<open>ML_Antiquotation.inline @{binding print_env'}
(Scan.peek (fn _ => Scan.option Parse.embedded)
>> (fn name => ("print_env' "
......@@ -46,7 +48,7 @@ setup \<open>ML_Antiquotation.inline @{binding print_env'}
| SOME s => "(SOME \"" ^ s ^ "\")")
^ " " ^ ML_Pretty.make_string_fn)))\<close>
subsection\<open>Accessing the C_Env in an Example\<close>
subsection\<open>Accessing the \<open>C_Env\<close> in an Example\<close>
C \<comment> \<open>Nesting ML code in C comments\<close> \<open>
int a(int b){int c;
......@@ -64,8 +66,6 @@ val b_res = lookup_Cid_info (!ENV) "b";
val c_res = lookup_Cid_info (!ENV) "c"
\<close>
(* Problematic : *)
C \<comment> \<open>Nesting ML code in C comments\<close> \<open>
int a (int b){int b;
return b;
......@@ -80,9 +80,7 @@ lookup_Cid_info (!ENV) "b"
section \<open>Global Declarations via CEnv and via the Clean API\<close>
subsection \<open>Global Declarations via \<open>C_Env\<close> and via the Clean API\<close>
text \<open>
First, we translate the expressions;
......@@ -104,8 +102,9 @@ ML\<open>val sigma_i = StateMgt.get_state_type_global @{theory}\<close>
declare [[C\<^sub>r\<^sub>u\<^sub>l\<^sub>e\<^sub>0 = "translation_unit"]]
declare [[C\<^sub>e\<^sub>n\<^sub>v\<^sub>0 = last]]
C\<open> int a[10+12][34][] = 1;
short int f(int x [][], long double y)
C\<open>int a[10+12][34][] = 1;
\<close>
C\<open> short int f(int x [][], long /* double */ y)
{int y; x=x;
/*@@ \<approx>setup \<open>@{print_env'}\<close> */
/*@@ highlight */}
......@@ -142,8 +141,6 @@ val [((Some (CDeclr0 (_,t,_,_,_)),_),_)] = B'
end
\<close>
ML\<open>(#ret o #3 o the)(lookup_Cid_info env_expr "f" );\<close>
ML\<open>
C11_TypeSpec_2_CleanTyp.conv_CDerivedDecl_typ;C_Ast.CFunDeclr0;
val S = hd ((#params o #3 o the)(lookup_Cid_info env_expr "f" ));
......@@ -152,7 +149,6 @@ val S' = C11_TypeSpec_2_CleanTyp.conv_CDerivedDecl_typ [S] sigma_i
(* and the whole thing a bit more abstract with "a" and "f" *)
ML\<open>
map_option (C11_TypeSpec_2_CleanTyp.conv_GlobalIdDescr_typ o #3) (lookup_Cid_info env_expr "a" );
(* map_option (conv_GlobalIdDescr_typ o #3) (lookup_Cid_info env_expr "f" ); *)
map_option (C11_TypeSpec_2_CleanTyp.conv_GlobalIdDescr_typ o #3) (lookup_Cid_info env_expr "x" );
map_option (C11_TypeSpec_2_CleanTyp.conv_GlobalIdDescr_typ o #3) (lookup_Cid_info env_expr "y" );
\<close>
......
C11-BackEnds/Clean_wrapper/examples/Coder_Test_StmtTUnits.thy
View file @ 4f8f5226
......@@ -14,7 +14,7 @@ C\<open>int global1;\<close>
ML\<open>
local open C_AbsEnv in
val (identifiers, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
val (identifiers, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier identifiers
end
\<close>
......@@ -24,7 +24,7 @@ C\<open>int global2[];
ML\<open>
local open C_AbsEnv in
val (identifiers, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
val (identifiers, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier identifiers
end
\<close>
......@@ -34,7 +34,7 @@ unsigned int global6, global7;\<close>
ML\<open>
local open C_AbsEnv in
val (identifiers, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
val (identifiers, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier identifiers
end
\<close>
......@@ -46,7 +46,7 @@ int c = foo(a), d;
ML\<open>
local open C_AbsEnv in
val (identifiers, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
val (identifiers, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier identifiers
end\<close>
......@@ -60,7 +60,7 @@ void test() {
ML\<open>
local open C_AbsEnv in
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier nEnv
end\<close>
......@@ -69,7 +69,10 @@ end\<close>
function definition of `identity` *)
local_vars_test (identity "int")
z :: "int"
ML\<open>val sigma_i = StateMgt.get_state_type_global @{theory}\<close>
ML\<open>val sigma_i = StateMgt.get_state_type_global @{theory}
val Type(ty_name, _) = sigma_i
\<close>
C\<open>int identity(int a) {
return a;
......@@ -77,7 +80,7 @@ C\<open>int identity(int a) {
ML\<open>
local open C_AbsEnv in
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier nEnv
val ast_stmt = extractStatement nEnv "identity"
end
......@@ -95,10 +98,12 @@ val lookup=Symtab.lookup state_field p *)
val [S] = (C11_Ast_Lib.fold_cStatement
regroup
(convertStmt false sigma_i nEnv @{theory} )
(convertStmt false sigma_i nEnv @{theory} "" (K (NONE, NONE)))
ast_stmt []);
\<close>
ML\<open>writeln (Syntax.string_of_term_global @{theory} S);\<close>
ML\<open>
(* We create an abstraction over the term: iterate backwards using the param list *)
fun mk_final_term identifiers id t =
......@@ -133,7 +138,7 @@ float add(int a, int b) {
ML\<open>
local open C_AbsEnv in
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier nEnv
val add_ast = @{C11_CTranslUnit}
val ast_stmt = extractStatement nEnv "add"
......@@ -145,12 +150,12 @@ ML\<open>
val [S] = (C11_Ast_Lib.fold_cStatement
regroup
(convertStmt false sigma_i nEnv @{theory} )
(convertStmt false sigma_i nEnv @{theory} "" (K (NONE,NONE)) )
ast_stmt []);
\<close>
ML\<open>
val final_term = mk_final_term identifiers "add" S
val final_term = mk_final_term nEnv "add" S
\<close>
ML\<open>
......@@ -175,7 +180,7 @@ int increment(int a) {
ML\<open>
local open C_AbsEnv in
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier nEnv
val ast_stmt = extractStatement nEnv "increment";
end
......@@ -185,7 +190,7 @@ end
ML\<open>
val [S] = (C11_Ast_Lib.fold_cStatement
regroup
(convertStmt false sigma_i nEnv @{theory})
(convertStmt false sigma_i nEnv @{theory} "" (K(NONE,NONE)))
ast_stmt [])
handle ERROR _ => [S];
\<close>
......@@ -207,7 +212,7 @@ void foo() {
ML\<open>
local open C_AbsEnv in
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier nEnv
val ast_stmt = extractStatement nEnv "foo";
end
......@@ -217,7 +222,7 @@ end
ML\<open>
val [S] = (C11_Ast_Lib.fold_cStatement
regroup
(convertStmt true sigma_i nEnv @{theory} )
(convertStmt true sigma_i nEnv @{theory} "" (K(NONE,NONE)))
ast_stmt []);
\<close>
......@@ -226,7 +231,7 @@ val final_term = mk_final_term identifiers "foo" S
\<close>
ML\<open>
Sign.certify_term @{theory} final_term
Sign.certify_term @{theory} (Syntax.check_term @{context} final_term)
\<close>
ML\<open>
......@@ -251,14 +256,16 @@ local_vars_test (paws "unit")
ML\<open>val sigma_i = StateMgt.get_state_type_global @{theory}\<close>
ML\<open>val init_ident = [C_AbsEnv.Identifier("swap", Position.none, @{typ "unit"}, C_AbsEnv.FunctionCategory(C_AbsEnv.Final, NONE))]\<close>
(* TODO: should also be defined analogously to unsigned int, unsigned long, ... *)
C\<open>
void paws(unsigned int a, unsigned int b) {
void paws(unsigned a, unsigned b) {
swap(a, b);
}\<close>
ML\<open>
local open C_AbsEnv in
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} init_ident Symtab.empty
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} init_ident [] Symtab.empty
val () = List.app printIdentifier nEnv
val ast_stmt = extractStatement nEnv "paws";
end
......@@ -267,7 +274,7 @@ end
ML\<open>
val [S] = (C11_Ast_Lib.fold_cStatement
regroup
(convertStmt true sigma_i nEnv @{theory})
(convertStmt true sigma_i nEnv @{theory} "" (K(NONE,NONE)))
ast_stmt []);
\<close>
......@@ -326,23 +333,28 @@ ML\<open>val init_idents = parse_state_field_tab @{theory}\<close>
C\<open>
int bar(int a, int b) {
int d;
c = 0;
return 0;
}
\<close>
ML\<open>
local open C_AbsEnv in
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} init_idents Symtab.empty
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} init_idents [Identifier("c",@{here},HOLogic.intT, Global)] Symtab.empty
val () = List.app printIdentifier nEnv
val ast_stmt = extractStatement nEnv "bar";
val env = @{C\<^sub>e\<^sub>n\<^sub>v}
end
\<close>
ML\<open>
val [S] = (C11_Ast_Lib.fold_cStatement
regroup
(convertStmt true sigma_i nEnv @{theory})
(convertStmt true sigma_i nEnv @{theory} "" (K(NONE,NONE)))
ast_stmt []);
\<close>
......@@ -351,7 +363,7 @@ val final_term = mk_final_term identifiers "bar" S
\<close>
ML\<open>
Sign.certify_term @{theory} final_term
Sign.certify_term @{theory} (Syntax.check_term @{context} final_term)
\<close>
ML\<open>
......@@ -373,7 +385,7 @@ int factorial(int n) {
ML\<open>
local open C_AbsEnv in
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier nEnv
val ast_stmt = extractStatement nEnv "factorial";
end
......@@ -384,7 +396,7 @@ end
ML\<open>
val [S] = (C11_Ast_Lib.fold_cStatement
regroup
(convertStmt false sigma_i nEnv @{theory} )
(convertStmt false sigma_i nEnv @{theory} "" (K(NONE,NONE)))
ast_stmt [])
handle ERROR _ => (writeln "correct crash: recursion not supported";
[@{term "undefined"}])
......@@ -416,7 +428,7 @@ writeln (Syntax.string_of_term_global @{theory} final_term);
ML\<open>
local open C_AbsEnv in
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier nEnv
end\<close>
......@@ -427,14 +439,14 @@ local_vars_test (is_even "int")
ML\<open>val sigma_i = StateMgt.get_state_type_global @{theory}\<close>
C\<open>
int is_even(unsigned int n) {
int is_even(unsigned n) {
if (n == 0)
return 0;
else
return is_odd(n - 1);
}
int is_odd(unsigned int n) {
int is_odd(unsigned n) {
if (n == 0)
return -1;
else
......@@ -444,7 +456,7 @@ int is_odd(unsigned int n) {
ML\<open>
local open C_AbsEnv in
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier nEnv
val ast_stmt = extractStatement nEnv "is_even";
end
......@@ -454,7 +466,7 @@ end
ML\<open>
val [S] = (C11_Ast_Lib.fold_cStatement
regroup
(convertStmt false sigma_i nEnv @{theory})
(convertStmt false sigma_i nEnv @{theory} "" (K(NONE,NONE)))
ast_stmt [])
handle ERROR _ => (writeln "correct crash: recursion not supported";
[@{term "undefined"}]);
......@@ -486,7 +498,7 @@ int sqrt(int a) {
ML\<open>
local open C_AbsEnv in
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit}
init_idents Symtab.empty
init_idents [] Symtab.empty
val () = List.app printIdentifier nEnv
val ast_stmt = extractStatement nEnv "sqrt";
end
......@@ -495,7 +507,7 @@ end
ML\<open>
val [S] = (C11_Ast_Lib.fold_cStatement
regroup
(convertStmt false sigma_i nEnv @{theory})
(convertStmt false sigma_i nEnv @{theory} "" (K(NONE,NONE)))
ast_stmt []);
\<close>
......@@ -504,7 +516,7 @@ val final_term = mk_final_term identifiers "sqrt" S
\<close>
ML\<open>
Sign.certify_term @{theory} final_term
Sign.certify_term @{theory} (Syntax.check_term @{context} final_term)
\<close>
ML\<open>
......@@ -533,16 +545,17 @@ int allzeros(int t[], int n) {
ML\<open>
local open C_AbsEnv in
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit}
nEnv_0 Symtab.empty
nEnv_0 [] Symtab.empty
val () = List.app printIdentifier nEnv
val ast_stmt = extractStatement nEnv "allzeros";
end
\<close>
(* PROBLEM *)
ML\<open>
val [S] = (C11_Ast_Lib.fold_cStatement
regroup
(convertStmt false sigma_i nEnv @{theory})
(convertStmt false sigma_i nEnv @{theory} "" (K(NONE,NONE)))
ast_stmt []);
\<close>
......@@ -566,7 +579,7 @@ int binarysearch(int t[], int n, int v) {
ML\<open>
local open C_AbsEnv in
val (identifiers, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
val (identifiers, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier identifiers
end\<close>
......@@ -589,7 +602,7 @@ int linearsearch(int x, int t[], int n) {
ML\<open>
local open C_AbsEnv in
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier nEnv
end\<close>
......@@ -635,7 +648,7 @@ printf("Sorted list in ascending order:\n");
ML\<open>
local open C_AbsEnv in
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] Symtab.empty
val (nEnv, callTable) = parseTranslUnitIdentifiers @{C11_CTranslUnit} [] [] Symtab.empty
val () = List.app printIdentifier nEnv
end\<close>
......@@ -690,7 +703,9 @@ fun convertEnv (name,(pos_list,serial,{ global = true , params = [] , ret = Pars
end
\<close>
ML\<open>val (name,(pos_list,serial,{ global = true , params = P as (C_Ast.CFunDeclr0 G::R) , ret = Z })) = nth menv 5;
ML\<open>nth menv 5\<close>
ML\<open>val (name,(pos_list,serial,{ scope = C_Env.Global , functionArgs=_,
params = P as (C_Ast.CFunDeclr0 G::R) , ret = Z })) = nth menv 5;
val curried_w_dummyreturn = C11_TypeSpec_2_CleanTyp.conv_CDerivedDecl_typ P dummyT
val (tyS,ty) = strip_type curried_w_dummyreturn
val uncurried_w_dummyreturn = HOLogic.mk_tupleT tyS --> ty
......@@ -698,18 +713,13 @@ ML\<open>val (name,(pos_list,serial,{ global = true , params = P as (C_Ast.CFunD
ML\<open>nth menv 5;
\<close>
(* So ne scheisse. Der return-type ist zwar im AST sichtbar, aber nicht im globalen (Isabelle_C)
Environment. Da findet sich lediglich : previous in stack. Das verkompliziert die Sache.
Immerhin:
*)
ML\<open>map_filter convertEnv menv\<close>
(* dies ist ein Versuch, ein return in einem globalen Kontext auszufuehren.
Dieser Test macht keinen Sinn.
ML\<open>
val [body] = (C11_Ast_Lib.fold_cStatement
regroup \<comment> \<open>real rearrangements of stack for statement compounds\<close>
(convertStmt false (StateMgt_core.get_state_type @{context}) nEnv_0 @{theory})
(convertStmt false (StateMgt_core.get_state_type @{context}) nEnv_0 @{theory} "" (K(NONE,NONE)))
\<comment> \<open>combinator handlicng an individual statement\<close>
ast_stmt \<comment> \<open>C11 ast\<close>
[] \<comment> \<open>mt stack\<close>);
......@@ -730,4 +740,5 @@ val local_thy = Function_Specification_Parser.define_body_core add_bind ret_typ
param_list body;
Function_Specification_Parser.define_body_core add_bind args_ty sty param_list body ctxt
(*Function_Specification_Parser.define_body_main { recursive = false } add_bind ret_typ sty param_list NONE 0 ctxt*)
\<close>
\ No newline at end of file
\<close>
*)
\ No newline at end of file
C11-BackEnds/Clean_wrapper/examples/Coder_Test_TUnits.thy 0 → 100644
View file @ 4f8f5226
theory "Coder_Test_TUnits"
imports
"../src/compiler/Clean_Annotation"
"../src/CleanTranslationHook"
begin
declare [[C\<^sub>e\<^sub>n\<^sub>v\<^sub>0 = last]]
declare [[C\<^sub>r\<^sub>u\<^sub>l\<^sub>e\<^sub>0 = "translation_unit"]]
C\<open>
int foo10(){
int b = 0, d123=4, ex=13;
}
\<close>
C\<open>
int foo11(){
int var1,var2=3,var3, var4;
}
\<close>
C\<open>
int forloop(){
int b=3;
for(int i=0; i<10; i=i+1){
b=b+1;
}
return b;
}
\<close>
find_theorems d123
find_theorems foo10_core
find_theorems forloop_core
text\<open>Apparently currently it is decided based on the stack layout, whether an else branch exists.
So a previous assignment destroys this code.\<close>
C\<open>
int g;
int foo13(){
if(1){
}
if (g>0){
g=1;
}
}
\<close>
C\<open>
int g;
int foo12(){
g = 0;
if (g>0){
g=1;
}
}
\<close>
C\<open>
int foo(int a, int b){
}
int bar(int b){
int a;
a = 2;
}
\<close>
C\<open>
int foo1(unsigned par){
unsigned tmp;
for (tmp = 0; tmp < tmp; tmp=tmp+1) {
}
}
\<close>
text\<open>Assigning numbers to a non-int variable causes issues\<close>
C\<open>
int bar1(){
unsigned tmp;
tmp = tmp+0;
}
\<close>
C\<open>
unsigned glob_nat;
int bar2(){
glob_nat = 3;
}
\<close>
C\<open>
int multiply1(int a, int b){
/*@ pre\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>(1::int) \<ge> 1\<close> */
return a;
}\<close>
term\<open>nat\<close>
C\<open>
int u;
int arrr[];
\<close>
C\<open>
int globvar;
unsigned nat1;
int u;
int fun_with_pre_test(int u){
int localvar;
localvar = u;
/*@ pre\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>u\<close> > 1\<close> */
/*@ post\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<lambda>ret::int.\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>u\<close> > 1 \<and> ret > 0\<close> */
while(localvar>0){
/*@ inv\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>u\<close> \<ge> \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>localvar\<close> \<close> */
/*@ measure\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open> \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>nat1\<close>\<close> */
localvar = localvar -1;
}
return 1;
}\<close>
find_theorems fun_with_pre_test_core
section\<open>Demonstration\<close>
subsection\<open>Global definitions\<close>
C\<open>
int global_integer;
unsigned global_nat;
\<close>
(*variables are declared accordingly*)
find_theorems global_integer
find_theorems global_nat
term\<open>global_integer\<close>
term\<open>global_nat\<close>
subsection\<open>Function definitions\<close>
C\<open>int threefunc(){
return 1+2;
}
int sum5(int p1, int p2){
return p1+p2;
}
void addToGlobalInteger(int value){
global_integer = global_integer+value;
}
\<close>
find_theorems threefunc_core
term\<open>threefunc\<close>
find_theorems sum_core
term\<open>sum\<close>
subsection\<open>And function calls\<close>
C\<open>
void addPlusThree(int val){
int three; /*Init expression currently unsupported*/
three = threefunc();
addToGlobalInteger(three+val);
}
\<close>
text\<open>we compare this to an equivalent definition\<close>
function_spec addPlusThree1(val :: int) returns unit
pre "\<open>True\<close>"
post "\<open>\<lambda>res::unit. True \<close>"
local_vars three :: int
defines "p\<^sub>t\<^sub>m\<^sub>p \<leftarrow> call\<^sub>C threefunc \<open>()\<close> ; assign_local three_update (\<lambda>\<sigma>. p\<^sub>t\<^sub>m\<^sub>p);-
call\<^sub>C addToGlobalInteger \<open>(three + val)\<close>"
find_theorems addPlusThree_core
find_theorems addPlusThree1_core
term\<open>addPlusThree\<close>
term\<open>addPlusThree1\<close>
subsection \<open>Recursive functions\<close>
find_theorems global_integer
rec_function_spec recursive_add1(n::int) returns unit
pre "\<open>True\<close>"
post "\<open>\<lambda>res::unit. True \<close>"
local_vars localvar1 :: int
defines "if\<^sub>C \<open>n > 0\<close>
then (\<open> global_integer := global_integer + 1\<close>);-
call\<^sub>C recursive_add1 \<open>(n-1)\<close>
else skip\<^sub>S\<^sub>E
fi"
C\<open>
void recursive_add(int n){
if(n > 0){
global_integer = global_integer + 1;
recursive_add(n-1);
}
}\<close>
find_theorems recursive_add_core
find_theorems recursive_add1_core
term recursive_add
term recursive_add1
subsection\<open>(multidimensional) arrays are also supported\<close>
C\<open>
int globalArray[][];
int something(){
int localvar;
localvar = globalArray[0][3];
}
\<close>
subsection\<open>A fully annotated program\<close>
text\<open>disclaimer: C_expr antiquotation does not yet work\<close>
C\<open>
int multiply(int a, int b){
/*@ pre\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>(1::int) \<ge> 1\<close> */
/*@ post\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<lambda>ret::int. ret = \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>a*b\<close>\<close> */
int s;
int counter;
int counter_b;
counter = 0;
s = 0;
while(counter < a){
/*@ inv\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>counter*b\<close> = \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>s\<close> \<and> \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>counter\<close> \<le> \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>a\<close>\<close> */
counter_b = 0;
while(counter_b < b){
/*@ inv\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>counter_b\<close> \<le> \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>b\<close>\<close> */
counter_b = counter_b +1;
}
s = s + counter_b;
counter = counter + 1;
}
return s;
}
\<close>
find_theorems multiply_pre
section\<open>Some other tests\<close>
C\<open>
int intarr[][][];
int x;
\<close>
term x
find_theorems x
C\<open>
int sum1(int param1,int param2){
x = threefunc();
intarr[2][3][1] = x + param1 + param2;
return 1;
}
int sum3(int param1,int param2){
int x; // test to override
x = sum1(param1, param2);
return x;
}\<close>
find_theorems x
find_theorems sum1_core
C\<open>
int test_scope(){
x = 1;
return x;
}
\<close>
find_theorems sum3_core
term\<open>intarr\<close>
C\<open>
int a;
int testfunction(int v1, int v2){
global_integer = sum1(v1,v2);
return global_integer;
}
\<close>
C\<open>
int b;
\<close>
text\<open>Now the declaration of local variables\<close>
C\<open>
int funwithlocalvars(){
int localvar1;
localvar1 = threefunc();
return localvar1;
}
\<close>
term localvar1
find_theorems funwithlocalvars_core
term funwithlocalvars_core
ML\<open>
val ast = @{C11_CTranslUnit}
\<close>
ML\<open>
val env = @{C\<^sub>e\<^sub>n\<^sub>v}\<close>
function_spec testfunction1(param1 :: int, param2::int) returns int
pre "\<open>True\<close>"
post "\<open>\<lambda>res::int. True \<close>"
local_vars localvar1 :: int
defines "p\<^sub>t\<^sub>m\<^sub>p \<leftarrow> call\<^sub>C sum1 \<open>(2::int, 3::int)\<close> ; assign_global global_integer_update (\<lambda>\<sigma>. p\<^sub>t\<^sub>m\<^sub>p);-
return\<^bsub>local_testfunction1_state.result_value_update\<^esub> \<open>global_integer\<close>"
find_theorems testfunction1_core
term\<open>testfunction1_core\<close>
(*
Recursions with return values are currently unsupported in CLEAN, but are about to be fixed by someone else
rec_function_spec recursive_function2(n::int) returns int
pre "\<open>True\<close>"
post "\<open>\<lambda>res::int. True \<close>"
local_vars localvar1 :: int
defines "p\<^sub>t\<^sub>m\<^sub>p \<leftarrow> call\<^sub>C recursive_function2 \<open>2::int\<close> ; assign_local localvar1_update (\<lambda>\<sigma>. p\<^sub>t\<^sub>m\<^sub>p);-
return\<^bsub>local_recursive_function2_state.result_value_update\<^esub> \<open>1::int\<close>"
*)
text\<open>Now the pre and post conditions\<close>
C\<open>
int xx;
int fun_with_pre(int u){
int local1;
/*@ pre\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>xx\<close> > 0\<close> */
/*@ post\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<lambda>ret::int.3 > \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>u\<close>\<close> */
return local1;
}
int fun_with_pre2(int u){
/*@ pre\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>u\<close> > 0\<close> */
return 1;
}
\<close>
ML\<open>
val annotation_data = Clean_Annotation.Data_Clean_Annotations.get (Context.Theory @{theory})
\<close>
text\<open>Invariants are more tricky, as there can be several within one function\<close>
text\<open>Lets start with a simple example with two loops,
which computes a*b, given a and b are positive!
The following program is fully annotated with pre-, and postcondition, aswell as 2 invariants\<close>
C\<open>int a;\<close>
C\<open>
int multiply2(int a, int b){
/*@ pre\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>a\<close> > 0\<close> */
/*@ post\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<lambda>ret::int. ret = \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>a*b\<close>\<close> */
int sum;
int counter;
int counter_b;
while(counter < a){
/* here we have a loop without an invariant */
counter = counter + 1;
}
counter = 0;
sum = 0;
while(counter < a){
/*@ inv\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>counter\<close> \<le> \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>a\<close>\<close> */
counter = counter + 1;
}
while(counter > 0){
/* inv\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>\<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>(a-counter)*b\<close> = \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>sum\<close> \<and> \<^C>\<^sub>e\<^sub>x\<^sub>p\<^sub>r\<open>counter\<close> \<ge> 0\<close> */
counter_b = 0;
while(counter_b < b){
/* inv\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n \<open>C\<open>counter_b\<close> \<le> b\<close>*/
counter_b = counter_b +1;
}
sum = sum + counter_b;
counter = counter -1;
}
return sum;
}
\<close>
C\<open>
int globarr[];\<close>
C\<open>
void somefunction123(){
int localArray[];
}\<close>
find_theorems multiply_core
ML\<open>
val annotation_data = Clean_Annotation.Data_Clean_Annotations.get (Context.Theory @{theory})
\<close>
C11-BackEnds/Clean_wrapper/src/.CleanCoder.thy.marks 0 → 100644
View file @ 4f8f5226
!c;26152;26152
C11-BackEnds/Clean_wrapper/src/CleanCoderTypAEnv.thy
View file @ 4f8f5226
......@@ -139,7 +139,7 @@ fun conv_ParseStatus_CDeclSpecS (SOME(C_Env.Parsed S)) = SOME S
|conv_ParseStatus_CDeclSpecS _ = NONE
fun conv_cDeclarationSpecifier_typ (SOME([CTypeSpec0 (CUnsigType0 _)])) = SOME(HOLogic.intT)
fun conv_cDeclarationSpecifier_typ (SOME([CTypeSpec0 (CUnsigType0 _)])) = SOME(HOLogic.natT)
|conv_cDeclarationSpecifier_typ (SOME([CTypeSpec0 (CIntType0 _)])) = SOME(HOLogic.intT)
|conv_cDeclarationSpecifier_typ (SOME([CTypeSpec0 (CLongType0 _),
CTypeSpec0 (CIntType0 _)])) = SOME(HOLogic.intT)
......@@ -244,6 +244,7 @@ signature C_ABS_ENVIRONMENT =
datatype identifier = Identifier of string * Position.T * typ * identType
val parseTranslUnitIdentifiers: C_Ast.nodeInfo C_Ast.cTranslationUnit
-> identifier list
-> identifier list
-> string list Symtab.table
-> identifier list * string list Symtab.table
......@@ -335,6 +336,11 @@ fun getMutuallyRecursiveCalls (Identifier(name, pos, ty, idType) :: s) functionN
else getMutuallyRecursiveCalls s functionName
| getMutuallyRecursiveCalls [] _ = []
fun isCall0
((nc, _) :: R) =
if #tag nc = "CCall0" then true
else isCall0 R
| isCall0 [] = false
fun readCall0
((nc, _) :: R) =
if #tag nc = "CCall0" then R
......@@ -349,6 +355,7 @@ fun parseNodeContent
(HOLType: Basic_Term.typ option)
((nc, ni) :: R)
identList
oldIdents
functionCallList
(idType: identType) =
let val Left(posL, posR) = C_Grammar_Rule_Lib.decode ni
......@@ -356,47 +363,53 @@ fun parseNodeContent
case #tag nc of
"CTypeSpec0" (* this is the start variable declaration list (one or multiple) *)
=> let val HOLType = #sub_tag nc |> str2HOLogic
in parseNodeContent (SOME HOLType) (cutDownTypeSpec (R)) identList functionCallList idType
in parseNodeContent (SOME HOLType) (cutDownTypeSpec (R)) identList oldIdents functionCallList idType
end
| "Ident0"
=> let val name = node_content_parser nc
fun transform_list_type ((r,_)::R) ty = if #tag r = "CArrDeclr0" then HOLogic.listT (transform_list_type R ty) else ty
| transform_list_type [] ty = ty
fun skip_arr_decls ((r,b)::R) = if #tag r = "CArrDeclr0" then skip_arr_decls R else ((r,b)::R)
| skip_arr_decls [] = []
in (debug("(parseNodeContent) parsing: " ^ name);
if (* if the identifier already exists, this is either a reference to a variable
(which we ignore) or a declared function call *)
identifierExists identList name
then if functionIdentifierExists identList name
then parseNodeContent NONE R identList (name :: functionCallList) idType
else parseNodeContent NONE R identList functionCallList idType
else (* otherwise, it is a variable declaration or an undeclared function call *)
(identifierExists (identList@oldIdents) name)
then (if functionIdentifierExists (identList@oldIdents) name (*potential error when function is redefined as variable*)
then parseNodeContent NONE R identList oldIdents (name :: functionCallList) idType
else parseNodeContent NONE R identList oldIdents functionCallList idType)
else (* otherwise, it is a variable declaration or an undeclared function call or a reference to a variable defined elsewhere*)
let val (nc2, ni2) :: R = R
in case #tag nc2 of
"CDeclr0" (* this is the end of one variable declaration *)
=> (debug("(parseNodeContent) this is a DECLARATION: "^name);
parseNodeContent HOLType R (Identifier(node_content_parser nc, posL,
(fn (SOME(a)) => a) HOLType, idType) :: identList) functionCallList idType)
| "CArrDeclr0" (* this is an array variable declaration, thus we INFER that
(fn (SOME(a)) => a) HOLType, idType) :: identList) oldIdents functionCallList idType)
| "CArrDeclr0" (* this is an array variable declaration, thus we count how many ArrDecls are here
#tag (hd R) is "CDeclr0" so we skip it *)
=> parseNodeContent HOLType (tl R) (Identifier(node_content_parser nc, posL,
HOLogic.listT ((fn (SOME(a)) => a) HOLType), idType) :: identList)
=>
parseNodeContent HOLType (skip_arr_decls R) (Identifier(node_content_parser nc, posL,
transform_list_type R (HOLogic.listT (the HOLType)), idType) :: identList) oldIdents
functionCallList idType
| "CTypeSpec0"
=> parseNodeContent HOLType (R) (Identifier(node_content_parser nc, posL,
(fn (SOME(a)) => a) HOLType, idType) :: identList) functionCallList idType
| s (* this is a function call, #tag nc2 is either another Ident0 which is a
(fn (SOME(a)) => a) HOLType, idType) :: identList) oldIdents functionCallList idType
| s =>(* this is a function call, #tag nc2 is either another Ident0 which is a
parameter which we ignore or CCall0 in which the function calls ends *)
=> (debug("function call detected (tag = " ^ s ^ ") : " ^ @{make_string} (R));
parseNodeContent HOLType (readCall0 ((nc2, ni2) :: R)) identList
(node_content_parser nc :: functionCallList) idType)
if (isCall0 ((nc2, ni2) :: R)) then (debug("function call detected (tag = " ^ s ^ ") : " ^ @{make_string} (R));
parseNodeContent HOLType (readCall0 ((nc2, ni2) :: R)) identList oldIdents
(node_content_parser nc :: functionCallList) idType) else
parseNodeContent HOLType R identList oldIdents functionCallList idType
end)
end
| "CDeclr0" (* artifact: list of params have a CDeclr0 at the end, so we ignore this *)
=> parseNodeContent HOLType R identList functionCallList idType
=> parseNodeContent HOLType R identList oldIdents functionCallList idType
| "CCall0" (* artifact: list of params have a CDeclr0 at the end, so we ignore this *)
=> parseNodeContent HOLType R identList functionCallList idType
=> parseNodeContent HOLType R identList oldIdents functionCallList idType
| _
=> error("node content parsing failure: " ^ @{make_string} ((nc, ni) :: R)))
end
| parseNodeContent _ [] identList functionCallList _ =
| parseNodeContent _ [] identList oldIdents functionCallList _ =
(debug("(parseNodeContent) finished: identList--" ^ @{make_string} identList
^ " functionCallList--" ^ @{make_string} functionCallList);
(identList, functionCallList))
......@@ -473,7 +486,7 @@ fun parseFunctionCalls
(functionCategory, identList, functionCallTable)
fun parseParams L (functionName: string) =
let val (identList, _) = parseNodeContent NONE L [] [] (Parameter(functionName))
let val (identList, _) = parseNodeContent NONE L [] [] [] (Parameter(functionName))
in identList end
(* Parses identifiers in a function body.
......@@ -488,9 +501,11 @@ fun parseLocals
(* Table of previous function names with list of function calls *)
(functionCallTable: string list Symtab.table)
(* Previous identifiers *)
(identList: identifier list) =
(identList: identifier list)
(* Identifiers from a previous translation unit (synthesized from env)*)
(oldIdents: identifier list) =
(debug("parsing locals: " ^ @{make_string} L);
let val (identList, functionCalls) = parseNodeContent NONE L identList [] (Local(functionName))
let val (identList, functionCalls) = parseNodeContent NONE L identList oldIdents [] (Local(functionName))
val (functionCategory, identList, functionCallTable) =
parseFunctionCalls functionName identList functionCallTable functionCalls Final
in (identList, functionCategory, functionCallTable) end)
......@@ -501,6 +516,7 @@ fun parseLocals
fun parseExternalDeclaration
(CDeclExt0(declaration : nodeInfo cDeclaration))
identList
oldIdents
functionCallTable =
(* Select Ident0 constructors in a cDeclaration. Here we suppose that there is only 1 *)
let val CDecl0(declarationSpecifierList, _, _) = declaration
......@@ -511,7 +527,7 @@ fun parseExternalDeclaration
val nodeContentList = rev (C11_Ast_Lib.fold_cDeclaration (K I)
(selectFromNodeContent ["Ident0", "CTypeSpec0", "CArrDeclr0", "CDeclr0", "CCall0"])
declaration [])
val (newIdentList, _) = parseNodeContent NONE nodeContentList identList [] Global
val (newIdentList, _) = parseNodeContent NONE nodeContentList identList oldIdents [] Global
in (debug("parsing global variable: " ^ @{make_string} nodeContentList);
(newIdentList, functionCallTable))
end
......@@ -525,6 +541,7 @@ fun parseExternalDeclaration
statement: nodeInfo cStatement,
ndInfo: nodeInfo)))
identList
oldIdents
(functionCallTable: string list Symtab.table) =
let val functionReturnHOLType = conv_cDeclarationSpecifier_typ (SOME(declarationSpecifierList))
|> (fn (SOME(a)) => a)
......@@ -538,27 +555,40 @@ fun parseExternalDeclaration
(selectFromNodeContent ["Ident0", "CTypeSpec0",
"CArrDeclr0", "CDeclr0", "CCall0"])
statement [])
val (newIdentList, functionCategory, newFunctionCallTable) =
(*we need to sort out the local identifiers of previous functions, as they are no longer accessible*)
fun sortIdentifiers [] = ([],[])
|sortIdentifiers (ident::R) = let
val (prev_glob, prev_loc) = sortIdentifiers R
in case ident of Identifier (_,_,_,Global)=> (ident::prev_glob, prev_loc)
|Identifier (_,_,_,FunctionCategory _) => (ident::prev_glob, prev_loc)
|_ => (prev_glob, ident::prev_loc)
end
val (previous_global_identifiers, previous_local_identifiers) = sortIdentifiers (identList)
val (newIdentList', functionCategory, newFunctionCallTable) =
parseLocals statementContentList functionName functionCallTable
(paramIdentifiers @ identList)
(paramIdentifiers@previous_global_identifiers) oldIdents
val newIdentList = newIdentList'@previous_local_identifiers
in (Identifier(functionName, posL, functionReturnHOLType,
FunctionCategory(functionCategory, SOME(statement))) :: newIdentList,
newFunctionCallTable)
end
| parseExternalDeclaration s _ _ = error("Unsupported: " ^ @{make_string} s)
| parseExternalDeclaration s _ _ _= error("Unsupported: " ^ @{make_string} s)
fun parseTranslUnitIdentifiers
(CTranslUnit0(externalDeclaration :: R, translUnitNodeInfo))
identList
oldIdents
(functionCallTable: string list Symtab.table) =
let val (newIdentList, newFunctionCallTable) =
parseExternalDeclaration externalDeclaration identList functionCallTable
parseExternalDeclaration externalDeclaration identList oldIdents functionCallTable
in (debug("newIdentList (parseTranslUnitIdentifiers): " ^ @{make_string} newIdentList);
parseTranslUnitIdentifiers (CTranslUnit0(R, translUnitNodeInfo))
newIdentList newFunctionCallTable)
newIdentList oldIdents newFunctionCallTable)
end
| parseTranslUnitIdentifiers _ identList functionCallTable = (identList, functionCallTable)
| parseTranslUnitIdentifiers _ identList oldIdents functionCallTable = (identList, functionCallTable)
fun printIdentifier (Identifier(name, pos, typ, idType)) =
writeln("Identifier: " ^ name ^ " " ^ Position.here pos ^
......
C11-BackEnds/Clean_wrapper/src/CleanTranslationHook.thy 0 → 100644
View file @ 4f8f5226
theory "CleanTranslationHook"
imports "../src/CleanCoder" (* Coder_Test_Env_AEnv *)
"../src/compiler/Clean_Annotation"
begin
ML\<open>
(*This is an override for the update_Root_Ast function that is registered in C_Command.*)
fun transform_type typ = if typ = HOLogic.intT then "int"
else if typ = HOLogic.natT then "nat"
else if is_listTy typ then (transform_type (dest_listTy typ))^" list"
else if typ = HOLogic.unitT then "unit"
else error "Unknown variable type"
local open C_AbsEnv HOLogic in
fun get_hol_type (C_Env.Parsed ret) params = let
val base_type =the (C11_TypeSpec_2_CleanTyp.conv_cDeclarationSpecifier_typ (SOME ret))
fun transform_type ((C_Ast.CArrDeclr0 _)::R) base_type = listT (transform_type R base_type)
| transform_type [] base_type = base_type
| transform_type ps _ = error ("First type parameter unknown (maybe pointers): "^(@{make_string} ps))
in transform_type params base_type end
|get_hol_type a _ = error ("Can not get type of \""^(@{make_string} a)^"\"")
fun map_env_ident_to_identifier (name,(positions,_,data)) =
let fun get_ident_scope C_Env.Global = Global
|get_ident_scope C_Env.Local = Local ""
|get_ident_scope C_Env.Parameter = Parameter ""
in
case #functionArgs data of C_Ast.None => Identifier(name, if null positions then @{here} else hd positions,get_hol_type (#ret data) (#params data),get_ident_scope (#scope data))
|_=> Identifier(name, @{here},intT,FunctionCategory (Final, NONE)) (*this line is wrong because of different function types*)
end
end
fun declare_function idents name ast ret_ty recursive ctxt =
let val param_idents = filter (fn i => case i of C_AbsEnv.Identifier(_,_,_, C_AbsEnv.Parameter f_name) => f_name = name |_=>false) idents
val local_idents = filter (fn i => case i of C_AbsEnv.Identifier(_,_,_, C_AbsEnv.Local f_name) => f_name = name |_=>false) idents
val global_idents = filter (fn i => case i of C_AbsEnv.Identifier(_,_,_, C_AbsEnv.Global) => true
| C_AbsEnv.Identifier(_,_,_,C_AbsEnv.FunctionCategory _)=>true
| _ => false) idents
(*Obtain the parameters and local variables*)
val params = map (fn C_AbsEnv.Identifier(name,pos,typ, _) => (Binding.make (name, pos), transform_type typ)) (param_idents)
val locals = map (fn C_AbsEnv.Identifier(name,pos,typ, _) => (Binding.make (name, pos), transform_type typ, NoSyn)) (local_idents)
(*This is necessary, as parameters are represented as free variables.
When the Invariants, post- and preconditions are read through the term antiquotations,
Syntax.parse_term (Syntax.read_term does this too) would substitute them by another const,
which could be a local or global variable*)
fun remove_params_from_proof ctx = let
val param_names = List.map (fn C_AbsEnv.Identifier(n,_,_,_) => n) param_idents
fun filter_by_shortname param_names (n, _) =
List.exists (fn ele => ele = Long_Name.base_name n) param_names
val longnames = List.filter (filter_by_shortname param_names) (#constants (Consts.dest (Sign.consts_of (Proof_Context.theory_of ctx))))
val thy0 = Proof_Context.theory_of ctx
val thy' = List.foldl (fn (longname, thy')=> thy' |> Sign.hide_const true longname) thy0 (List.map fst longnames)
in Proof_Context.init_global thy' end
(*Invariants and measuress need to be matched to a loop. This is done by comparing the parse locations of all while loops.
The following are helper methods, to obtain the function get_invariant::positiona \<rightarrow> (context\<rightarrow>term) option*)
val invariants:((string*(Context.generic -> term)*Position.range) list) = List.filter (fn (f_name,_,_) => f_name = name)
(#invariants (Clean_Annotation.Data_Clean_Annotations.get ctxt))
val measures:((string*(Context.generic -> term)*Position.range) list) = List.filter (fn (f_name,_,_) => f_name = name)
(#measures (Clean_Annotation.Data_Clean_Annotations.get ctxt))
val loop_pos =Library.distinct (op =) (C11_Ast_Lib.fold_cStatement (fn a => fn b => a@b) C11_Unit_2_Clean.get_loop_positions ast [])
fun compare_pos ((C_Ast.Position0 (pos1,_,_,_)),(C_Ast.Position0 (pos2,_,_,_))) = Int.compare (pos1,pos2)
|compare_pos a = error ("Unable to compare positions (for invariants and measures): "^(@{make_string} a))
val loop_pos_sorted = Library.sort compare_pos loop_pos
fun range_less_than_pos (range:Position.range) (C_Ast.Position0 (pos,_,_,_)) = the (Position.offset_of (fst range)) < pos
|range_less_than_pos a b = error ("Unable to compare positions (for invariants and measures): "^(@{make_string} (a,b)))
fun get_for_position (((inv,inv_pos)::R_inv): ((Context.generic -> term)*Position.range)list)
(loop_positions: C_Ast.positiona list)
(pos3: C_Ast.positiona)
(* search the first invariant, which is not declared before pos3 *)
= (if range_less_than_pos inv_pos pos3 then get_for_position R_inv loop_positions pos3
else case loop_positions of (* we found the first invariant after pos3 *)
(* Now check, if the next loop definition is after the invariant definition.
Otherwise there is no invariant for the given loop *)
(pos1::pos2::R) => if pos3 = pos1 andalso range_less_than_pos inv_pos pos2 then SOME inv
else get_for_position ((inv,inv_pos)::R_inv) (pos2::R) pos3
| (pos1::_) => if pos3 = pos1 then SOME inv else NONE
| [] => NONE)
|get_for_position [] _ _ = NONE
fun get_invariant pos = (get_for_position (List.map (fn inv => (#2 inv, #3 inv)) invariants) loop_pos_sorted) pos
fun get_measure pos = (get_for_position (List.map (fn inv => (#2 inv, #3 inv)) measures) loop_pos_sorted) pos
fun get_loop_annotations pos = (get_invariant pos, get_measure pos)
(*generic function to get the first ele*)
val get_precond = Option.map (fn (_,e,_) => e) (List.find (fn (a,_,_) => a = name) (#preconditions (Clean_Annotation.Data_Clean_Annotations.get ctxt)))
val get_postcond = Option.map (fn (_,e,_) => e) (List.find (fn (a,_,_) => a = name) (#postconditions (Clean_Annotation.Data_Clean_Annotations.get ctxt)))
(*the translation of the precondition*)
fun get_translation NONE default ctxt= C11_Expr_2_Clean.lifted_term (StateMgt.get_state_type (ctxt)) default
| get_translation (SOME get_term) _ ctxt= let
val term = get_term (Context.Proof (remove_params_from_proof ctxt))
val lifted = C11_Expr_2_Clean.lifted_term (StateMgt.get_state_type ctxt) term
in
Syntax.check_term ctxt lifted
end
(*The actual translation of the loop body*)
fun get_translated_fun_bdy ctx _ = let
val ctx' = remove_params_from_proof ctx
val v = ((C11_Ast_Lib.fold_cStatement
C11_Stmt_2_Clean.regroup
(C11_Stmt_2_Clean.convertStmt false
(StateMgt.get_state_type ctx')
(local_idents@param_idents@global_idents)
(Proof_Context.theory_of ctx')
name get_loop_annotations)
ast []))
in ( hd) v end
val test_function_sem = {binding = Binding.name name,
locals = locals@[(Binding.name "dummylocalvariable","int", NoSyn)], (*There needs to be at least one local variable*)
params = params,
ret_type = transform_type ret_ty,
read_pre = get_translation get_precond (@{term True}),
read_post = get_translation get_postcond (Abs ("ret",ret_ty, @{term True})),
read_variant_opt = NONE,
read_body = get_translated_fun_bdy}
val decl = Function_Specification_Parser.checkNsem_function_spec_gen {recursive = recursive} test_function_sem
in decl end
local open C_AbsEnv HOLogic in
fun handle_declarations translUnit ctxt =
(let
(*get the OLD environment, which simplifies the parseTranslUnitIdentifiers by a lot.*)
val env = (C_Module.Data_Last_Env.get ctxt)
(*First we need to get all previously defined global vars and functions*)
val prev_idents =map map_env_ident_to_identifier (Symtab.dest (#idents(#var_table(env))))
(*the new identifiers are returned in reverse \<rightarrow> thus reverse *)
val (new_idents, call_table) = C_AbsEnv.parseTranslUnitIdentifiers translUnit [] prev_idents Symtab.empty
val identifiers = (rev new_idents)@prev_idents
val map_idents = List.map (fn C_AbsEnv.Identifier(name,_,typ,_) => (Binding.name name, transform_type typ, NoSyn))
fun get_declaration is_global idents = if null idents then I else StateMgt.new_state_record is_global (NONE,idents)
val global_idents = (map_idents (List.filter (fn C_AbsEnv.Identifier(_,_,_,vis) => vis = C_AbsEnv.Global) new_idents))
val global_declaration =get_declaration true global_idents
val fun_asts =
List.map (fn C_AbsEnv.Identifier(name,_,ret_ty,C_AbsEnv.FunctionCategory ast) =>
let fun is_recursive NONE = false
|is_recursive (SOME calls) = List.exists (fn x => x=name) calls
in
(name,the (snd ast),ret_ty, is_recursive (Symtab.lookup call_table name)) end
| ident => error ("Expected function identifier. Instead: "^(@{make_string} ident)))
(List.filter (fn a => case a of C_AbsEnv.Identifier(_,_,_,C_AbsEnv.FunctionCategory _) => true | _ => false) (rev new_idents))
val function_declarations = List.map (fn (name,ast,ret_ty, recursive) => declare_function identifiers name ast ret_ty recursive ctxt) (fun_asts)
val function_decl = fold (fn f => fn acc => f acc) function_declarations
in
Context.map_theory (function_decl o global_declaration) ctxt
end);
end
\<close>
ML\<open>
fun handle_declarations_wrapper ast v2 ctxt =
let val ctx1 = update_Root_Ast SOME ast v2 ctxt (*Note the call to the original callback - this somehow gets overwritten*)
in
case ast of (C_Ast.Left translUnit) => handle_declarations translUnit ctx1
| _ => ctx1
end
\<close>
setup \<open>C_Module.C_Term.map_expression
(fn cexpr => fn _ => fn ctxt => let
val sigma_i = (StateMgt.get_state_type o Context.proof_of )ctxt
val env = C_Module.Data_Surrounding_Env.get ctxt
val idents = (Symtab.dest (#idents(#var_table(env))))
val A_env = List.map map_env_ident_to_identifier idents
val expr = (hd (C11_Ast_Lib.fold_cExpression (K I)
(C11_Expr_2_Clean.convertExpr false sigma_i A_env (Context.theory_of ctxt) "" (K NONE))
cexpr [])) handle ERROR msg => (writeln("ERROR: "^(@{make_string}msg));@{term "1::int"})
in
expr
end)\<close>
setup \<open>Context.theory_map (C_Module.Data_Accept.put (handle_declarations_wrapper))\<close>
(* Note: The hook "C_Module.C_Term.map_translation_unit" is not adequate, as it is
meant for the term antiquotation (its callback returns a term, not a theory/context *)
setup \<open>C_Module.C_Term.map_expression
(fn cexpr => fn _ => fn ctxt => let
val sigma_i = (StateMgt.get_state_type o Context.proof_of )ctxt
val env = C_Module.Data_Surrounding_Env.get ctxt
val idents = (Symtab.dest (#idents(#var_table(env))))
val A_env = List.map map_env_ident_to_identifier idents
val expr = (hd (C11_Ast_Lib.fold_cExpression (K I)
(C11_Expr_2_Clean.convertExpr false sigma_i A_env (Context.theory_of ctxt) "" (K NONE))
cexpr [])) handle ERROR msg => (writeln("ERROR: "^(@{make_string}msg));@{term "1::int"})
in
expr
end)\<close>
end
\ No newline at end of file
C11-BackEnds/Clean_wrapper/src/Clean_Wrapper.thy
View file @ 4f8f5226
(******************************************************************************
* Isabelle/C/Clean
*
* Authors: Frederic Tuong, Burkhart Wolff
* Authors: Frederic Tuong, Lorenz Winkler, Burkhart Wolff
*
* Copyright (c) 2018-2019 Université Paris-Saclay, Univ. Paris-Sud, France
*
......
C11-BackEnds/Clean_wrapper/src/compiler/Clean_Annotation.thy
View file @ 4f8f5226
......@@ -8,7 +8,7 @@
* Redistribution and use in source and binary forms, with or without
* modification, are permitted provided that the following conditions are
* met:
*
* * Redistributions of source code must retain the above copyright
* notice, this list of conditions and the following disclaimer.
*
......@@ -63,20 +63,54 @@ datatype antiq_hol = Invariant of string (* term *)
| End_spec of string (* term *)
| Calls of text_range list
| Owned_by of text_range
| Measure of string
(*In the following data structure the annotations are saved*)
type annotation_data = {
preconditions: (string*(Context.generic -> term)*Position.range) list,
postconditions: (string*(Context.generic -> term)*Position.range) list,
invariants: (string*(Context.generic -> term)*Position.range) list,
measures: (string*(Context.generic -> term)*Position.range) list
}
structure Data_Clean_Annotations = Generic_Data
(type T = annotation_data
val empty = {preconditions=[], postconditions=[], invariants=[], measures=[]}
val merge = K empty)
fun map_context_annotation_declaration annotation_type src range context0 =
let
val current_env =snd (C_Stack.Data_Lang.get' context0) (*important: antiquotation needs current env*)
fun get_fun_name [(SOME (C_Ast.Ident0 (C_Ast.SS_base (C_Ast.ST name), _, _)),_)] = name
| get_fun_name (_::R) = get_fun_name R
| get_fun_name _ = (warning "unable to find name of surrounding function for CLEAN annotation";"")
val term =fn ctxt=>
(*Important change: Syntax.read_term does coerce the types of the terms
constructed by C_Expr antiquotation. Syntax.parse_term does not do that*)
(*It does substitute free variables though, which is quite an issue*)
Syntax.parse_term
(Context.proof_of (C_Module.Data_Surrounding_Env.put current_env ctxt))
(Token.inner_syntax_of src)
val function_name = (get_fun_name o #scopes o snd o C_Stack.Data_Lang.get') context0
val new_data = [(function_name, term, range)]
fun toplevel _ = C_Inner_Toplevel.keep''
val new_context_map = Data_Clean_Annotations.map (fn {preconditions, postconditions, invariants, measures} => {
preconditions = case annotation_type of Spec _ => preconditions@new_data | _ => preconditions,
postconditions = case annotation_type of End_spec _ => postconditions@new_data | _ => postconditions,
invariants =case annotation_type of Invariant _ => invariants@new_data | _ => invariants,
measures =case annotation_type of Measure _ => measures@new_data | _ => measures
})
in new_context_map context0 end
fun bind scan _ ((stack1, (to_delay, stack2)), _) =
fun bind scan context_map ((stack1, (to_delay, stack2)), _) =
C_Parse.range scan
>> (fn (src, range) =>
C_Env.Parsing
( (stack1, stack2)
, ( range
, C_Inner_Syntax.bottom_up
(fn _ => fn context =>
ML_Context.exec
(tap (fn _ => Syntax.read_term (Context.proof_of context) (Token.inner_syntax_of src)))
context)
(fn v1 => fn context =>(
context_map src range context)
)
, Symtab.empty
, to_delay)))
......@@ -92,17 +126,18 @@ user-defined annotations is very similar to the registration of ordinary command
platform.\<close>
ML \<open>local open Clean_Annotation
in fun command keyword f =
in fun command keyword annotation_type =
C_Annotation.command' keyword ""
(C_Token.syntax'
(Parse.token Parse.cartouche)
>>> toplevel f)
end\<close>
>>> map_context_annotation_declaration annotation_type)
end\<close>
setup \<open>let open Clean_Annotation
in command ("pre\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n", \<^here>) Spec
#> command ("post\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n", \<^here>) End_spec
#> command ("inv\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n", \<^here>) Invariant
in command ("pre\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n", \<^here>) (Spec "")
#> command ("post\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n", \<^here>) (End_spec "")
#> command ("inv\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n", \<^here>) (Invariant "")
#> command ("measure\<^sub>C\<^sub>l\<^sub>e\<^sub>a\<^sub>n", \<^here>) (Measure "")
end\<close>
end
C11-FrontEnd/examples/C5.thy 0 → 100644
View file @ 4f8f5226
theory C5
imports "Isabelle_C.C_Main"
begin
(*This file contains some ways to retrieve the C-environment*)
ML\<open>
val SPY_ENV = Unsynchronized.ref(NONE:C_Env.env_lang option);\<close>
declare [[C\<^sub>e\<^sub>n\<^sub>v\<^sub>0 = last]]
declare [[C\<^sub>r\<^sub>u\<^sub>l\<^sub>e\<^sub>0 = "translation_unit"]]
C\<open>
int globalvar1;
void test(int param1){
int localvariable1;
return 12; /*@ \<approx>setup \<open>fn _ => fn _ => fn env =>
(*The environment can be retrieved using the generic setup command*)
((SPY_ENV := SOME env);I) \<close> */;
int localvariable2;
}
int globalvar2;
\<close>
ML\<open>
(*We can see that the saved env in fact has all the current variables*)
val saved_vars = (map (fn (a,(_,_,b)) => (a,#scope b)) (Symtab.dest (
#idents(#var_table(the (!SPY_ENV))))
))
val final_vars = (map (fn (a,(_,_,b)) => (a,#scope b)) (Symtab.dest (
#idents(#var_table(@{C\<^sub>e\<^sub>n\<^sub>v})))))
\<close>
(*There is a second way to achieve the same, using the context*)
C\<open>
int globalvar3;
void test2(int param1){
int localvariable3;
return 12; /*@ \<approx>setup \<open>fn _ => fn _ => fn _ => fn ctx =>
(*The environment can be retrieved using the generic setup command*)
((SPY_ENV := SOME (snd (C_Stack.Data_Lang.get' ctx)));ctx) \<close> */;
int localvariable4;
}
int globalvar4;
\<close>
ML\<open>
(*We can see that the saved env in fact has all the current variables*)
val saved_vars = (map (fn (a,(_,_,b)) => (a,#scope b)) (Symtab.dest (
#idents(#var_table(the (!SPY_ENV))))
))
\<close>
(*Declaring a seperate antiquotation *)
ML\<open>
val env = @{C\<^sub>e\<^sub>n\<^sub>v}\<close>
ML\<open>
Theory.setup
(C_Inner_Syntax.command_no_range
(C_Inner_Toplevel.generic_theory oo C_Inner_Isar_Cmd.setup
\<open>fn ((_, (_, pos1, pos2)) :: _) =>
(fn _ => fn _ =>
tap (fn ctx =>
(SPY_ENV := SOME (snd (C_Stack.Data_Lang.get' ctx));Position.reports_text [((Position.range (pos1, pos2)
|> Position.range_position, Markup.intensify), "")])))
| _ => fn _ => fn _ => I\<close>)
("store_and_highlight", \<^here>, \<^here>))
\<close>
(*this is btw how all previous identifiers can get deleted*)
setup\<open>Context.theory_map (C_Module.Data_In_Env.put C_Env.empty_env_lang)\<close>
C\<open>
int globalvar3;
void test2(int param1){
int localvariable3;/*@ store_and_highlight */
}
\<close>
ML\<open>
val saved_vars = (map (fn (a,(_,_,b)) => (a,#scope b)) (Symtab.dest (
#idents(#var_table(the (!SPY_ENV)))) (*NOTE: localvariable3 is in the environment*)
))\<close>
setup\<open>Context.theory_map (C_Module.Data_In_Env.put C_Env.empty_env_lang)\<close>
C\<open>
int globalvar3;
void test2(int param1){
int localvariable3;/*@@@@@ store_and_highlight */
}
\<close>
ML\<open>
val saved_vars = (map (fn (a,(_,_,b)) => (a,#scope b)) (Symtab.dest (
#idents(#var_table(the (!SPY_ENV)))) (*NOTE: localvariable3 is NOT in the environment*)
))\<close>
\ No newline at end of file
C11-FrontEnd/main/C_Main.thy
View file @ 4f8f5226
......@@ -40,5 +40,7 @@ theory C_Main
begin
text\<open> @{footnote \<open>sdf\<close>}, @{file "$ISABELLE_HOME/src/Pure/ROOT.ML"}\<close>
end
(*>*)
C11-FrontEnd/src/C_Ast.thy
View file @ 4f8f5226
......@@ -875,7 +875,7 @@ and fold_cExpression grp g ast st =
|> g (TT"CCast0") a
| (CUnary0(unop:cUnaryOp, ex: 'a cExpression, a)) =>
st |> fold_cExpression grp g ex
|> g (TT("CUnary0 "^toString_cUnaryOp unop)) a
|> g (TTT"CUnary0" (toString_cUnaryOp unop)) a
| (CSizeofExpr0(ex:'a cExpression, a)) =>
st |> fold_cExpression grp g ex |> g (TT"CSizeofExpr0") a
| (CSizeofType0(decl:'a cDeclaration,a)) =>
......
C11-FrontEnd/src/C_Command.thy
View file @ 4f8f5226
......@@ -39,6 +39,7 @@ section \<open>Interface: Inner and Outer Commands\<close>
theory C_Command
imports C_Eval
"../../C11-BackEnds/Clean/src/Clean"
keywords "C" :: thy_decl % "ML"
and "C_file" :: thy_load % "ML"
and "C_export_boot" :: thy_decl % "ML"
......@@ -153,6 +154,8 @@ signature C_MODULE =
sig
structure Data_Accept : GENERIC_DATA
structure Data_In_Env : GENERIC_DATA
structure Data_Last_Env : GENERIC_DATA
structure Data_Surrounding_Env : GENERIC_DATA
structure Data_In_Source : GENERIC_DATA
structure Data_Term : GENERIC_DATA
......@@ -168,13 +171,13 @@ signature C_MODULE =
val key_external_declaration: Input.source
val key_statement: Input.source
val key_translation_unit: Input.source
val map_default: (C_Grammar_Rule.ast_generic -> C_Env.env_lang -> local_theory -> term) -> theory -> theory
val map_expression: (C_Grammar_Rule_Lib.CExpr -> C_Env.env_lang -> local_theory -> term) -> theory -> theory
val map_default: (C_Grammar_Rule.ast_generic -> C_Env.env_lang -> Context.generic -> term) -> theory -> theory
val map_expression: (C_Grammar_Rule_Lib.CExpr -> C_Env.env_lang -> Context.generic -> term) -> theory -> theory
val map_external_declaration:
(C_Grammar_Rule_Lib.CExtDecl -> C_Env.env_lang -> local_theory -> term) -> theory -> theory
val map_statement: (C_Grammar_Rule_Lib.CStat -> C_Env.env_lang -> local_theory -> term) -> theory -> theory
(C_Grammar_Rule_Lib.CExtDecl -> C_Env.env_lang -> Context.generic -> term) -> theory -> theory
val map_statement: (C_Grammar_Rule_Lib.CStat -> C_Env.env_lang -> Context.generic -> term) -> theory -> theory
val map_translation_unit:
(C_Grammar_Rule_Lib.CTranslUnit -> C_Env.env_lang -> local_theory -> term) -> theory -> theory
(C_Grammar_Rule_Lib.CTranslUnit -> C_Env.env_lang -> Context.generic -> term) -> theory -> theory
val tok0_expression: string * ('a * 'a -> (C_Grammar.Tokens.svalue, 'a) LALR_Parser_Eval.Token.token)
val tok0_external_declaration: string * ('a * 'a -> (C_Grammar.Tokens.svalue, 'a) LALR_Parser_Eval.Token.token)
val tok0_statement: string * ('a * 'a -> (C_Grammar.Tokens.svalue, 'a) LALR_Parser_Eval.Token.token)
......@@ -265,13 +268,23 @@ structure Data_In_Env = Generic_Data
val empty = C_Env.empty_env_lang
val merge = K empty)
structure Data_Last_Env = Generic_Data
(type T = C_Env.env_lang
val empty = C_Env.empty_env_lang
val merge = K empty)
structure Data_Surrounding_Env = Generic_Data
(type T = C_Env.env_lang
val empty = C_Env.empty_env_lang
val merge = K empty)
structure Data_Accept = Generic_Data
(type T = C_Grammar_Rule.ast_generic -> C_Env.env_lang -> Context.generic -> Context.generic
fun empty _ _ = I
val merge = #2)
structure Data_Term = Generic_Data
(type T = (C_Grammar_Rule.ast_generic -> C_Env.env_lang -> local_theory -> term) Symtab.table
(type T = (C_Grammar_Rule.ast_generic -> C_Env.env_lang -> Context.generic -> term) Symtab.table
val empty = Symtab.empty
val merge = #2)
......@@ -348,8 +361,9 @@ fun err0 _ _ pos =
val err = pair () oooo err0
fun accept0 f (env_lang:C_Env.env_lang) ast =
Data_In_Env.put env_lang
#> (fn context => f context ast env_lang (Data_Accept.get context ast env_lang context))
(fn ctx => Data_Last_Env.put (Data_In_Env.get ctx) ctx)
#> Data_In_Env.put env_lang
#> (fn context => (f context ast env_lang (Data_Accept.get context ast env_lang context)))
fun accept (env_lang:C_Env.env_lang) (_, (ast, _, _)) =
pair () o C_Env.map_context (accept0 (K (K (K I))) env_lang ast)
......@@ -373,18 +387,19 @@ fun accept ctxt start_rule =
val (key, pos) = Input.source_content key
in
( start
, fn env_lang => fn (_, (ast, _, _)) =>
, fn env_lang => fn (_, (ast, _, _)) =>((*This env_lang also contains the previous environment,
but returning this would completely override the new env (which would be bad in case of parsing input with ned declarations)*)
C_Env.map_context'
(accept0
(fn context =>
(fn context =>(
pair oo (case Symtab.lookup (Data_Term.get context) key of
NONE => tap (fn _ => warning ("Representation function associated to\
\ \"" ^ key ^ "\"" ^ Position.here pos
^ " not found (returning a dummy term)"))
(fn _ => fn _ => @{term "()"})
| SOME f => fn ast => fn env_lang => f ast env_lang ctxt))
| SOME f => fn ast => fn env_lang => f ast env_lang (Context.Proof ctxt))))
env_lang
ast))
ast)))
end
fun eval_in text context env start_rule =
......@@ -423,9 +438,9 @@ fun parse_translation l = l |>
src
(case Context.get_generic_context () of
NONE => Context.Proof ctxt
| SOME context => Context.mapping I (K ctxt) context)
(C_Stack.Data_Lang.get #> (fn NONE => env0 ctxt
| SOME (_, env_lang) => env_lang))
| SOME context => Context.Proof ctxt)
(fn _ => (C_Stack.Data_Lang.get #> (fn NONE => env0 ctxt (*HERE: This is a "fix" for starting with the current C_Env when parsing antiquotations.*)
| SOME (_, env_lang) => env_lang)) (Context.Proof ctxt))
start_rule
(c_enclose "" "" src)
end
......@@ -931,7 +946,7 @@ fun command_ml environment catch_all debug get_file gthy =
val ML = command_ml "" false;
val SML = command_ml ML_Env.SML true;
end;
\<close>
\<close>
subsubsection \<open>Initialization\<close>
......@@ -1309,6 +1324,7 @@ fun update_Root_Ast filter ast _ ctxt =
end;
fun get_Root_Ast filter thy =
let val ctxt = Context.Theory thy
val thid = Context.theory_long_name(Context.theory_of ctxt)
......
C11-FrontEnd/src/C_Environment.thy
View file @ 4f8f5226
......@@ -59,11 +59,13 @@ signature C_ENV =
type 'a stream = ('a, C_Lex.token) C_Scan.either list
datatype 'a parse_status = Parsed of 'a | Previous_in_stack
datatype variable_scope = Global | Local | Parameter
eqtype markup_global
type markup_ident = {global : markup_global,
type markup_ident = {scope : markup_global,
params : C_Ast.CDerivedDeclr list,
ret : C_Ast.CDeclSpec list parse_status}
ret : C_Ast.CDeclSpec list parse_status,
functionArgs : ((string*(C_Ast.NodeInfo C_Ast.cDeclaration)) list) C_Ast.optiona}
type 'a markup_store = Position.T list * serial * 'a
type var_table = {idents : markup_ident markup_store Symtab.table,
......@@ -200,11 +202,14 @@ type env_directives =
datatype 'a parse_status = Parsed of 'a | Previous_in_stack
type markup_global = bool (*true: global*)
datatype variable_scope = Global | Local | Parameter
type markup_global = variable_scope (*true: global*)
type markup_ident = { global : markup_global
type markup_ident = { scope : markup_global
, params : C_Ast.CDerivedDeclr list
, ret : C_Ast.CDeclSpec list parse_status }
, ret : C_Ast.CDeclSpec list parse_status
, functionArgs : ((string*(C_Ast.NodeInfo C_Ast.cDeclaration)) list) C_Ast.optiona}
type var_table = { tyidents : markup_global markup_store Symtab.table (*ident name*)
Symtab.table (*internal
......@@ -406,9 +411,9 @@ fun map_idents f {tyidents, idents} =
(**)
fun map_var_table f {var_table, scopes, namesupply, stream_ignored, env_directives} =
{var_table = f
({var_table = f
var_table, scopes = scopes, namesupply = namesupply,
stream_ignored = stream_ignored, env_directives = env_directives}
stream_ignored = stream_ignored, env_directives = env_directives})
fun map_scopes f {var_table, scopes, namesupply, stream_ignored, env_directives} =
{var_table = var_table, scopes = f
......@@ -503,7 +508,9 @@ fun string_of (env_lang : env_lang) =
let fun dest0 x f = x |> Symtab.dest |> map f
fun dest {tyidents, idents} =
(dest0 tyidents #1, dest0 idents (fn (i, (_,_,v)) =>
(i, if #global v then "global" else "local")))
(i, case #scope v of Global => "global"
| Local => "local"
| Parameter => "parameter")))
in \<^make_string> ( ("var_table", dest (#var_table env_lang))
, ("scopes", map (fn (id, i) =>
( Option.map (fn C_Ast.Ident0 (i, _, _) =>
......