aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--cfrontend/Cop.v27
-rw-r--r--cparser/Cutil.ml2
-rw-r--r--driver/Driver.ml79
3 files changed, 97 insertions, 11 deletions
diff --git a/cfrontend/Cop.v b/cfrontend/Cop.v
index 8b3421e8..4ac56b04 100644
--- a/cfrontend/Cop.v
+++ b/cfrontend/Cop.v
@@ -644,12 +644,16 @@ Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type)
match v1,v2 with
| Vptr b1 ofs1, Vint n2 =>
Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
+ | Vint n1, Vint n2 =>
+ Some (Vint (Int.add n1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
| _, _ => None
end
| add_case_ip ty => (**r integer plus pointer *)
match v1,v2 with
| Vint n1, Vptr b2 ofs2 =>
Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof cenv ty)) n1)))
+ | Vint n1, Vint n2 =>
+ Some (Vint (Int.add n2 (Int.mul (Int.repr (sizeof cenv ty)) n1)))
| _, _ => None
end
| add_case_pl ty => (**r pointer plus long *)
@@ -657,6 +661,9 @@ Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type)
| Vptr b1 ofs1, Vlong n2 =>
let n2 := Int.repr (Int64.unsigned n2) in
Some (Vptr b1 (Int.add ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
+ | Vint n1, Vlong n2 =>
+ let n2 := Int.repr (Int64.unsigned n2) in
+ Some (Vint (Int.add n1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
| _, _ => None
end
| add_case_lp ty => (**r long plus pointer *)
@@ -664,6 +671,9 @@ Definition sem_add (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type)
| Vlong n1, Vptr b2 ofs2 =>
let n1 := Int.repr (Int64.unsigned n1) in
Some (Vptr b2 (Int.add ofs2 (Int.mul (Int.repr (sizeof cenv ty)) n1)))
+ | Vlong n1, Vint n2 =>
+ let n1 := Int.repr (Int64.unsigned n1) in
+ Some (Vint (Int.add n2 (Int.mul (Int.repr (sizeof cenv ty)) n1)))
| _, _ => None
end
| add_default =>
@@ -697,6 +707,8 @@ Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type)
match v1,v2 with
| Vptr b1 ofs1, Vint n2 =>
Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
+ | Vint n1, Vint n2 =>
+ Some (Vint (Int.sub n1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
| _, _ => None
end
| sub_case_pl ty => (**r pointer minus long *)
@@ -704,6 +716,9 @@ Definition sem_sub (cenv: composite_env) (v1:val) (t1:type) (v2: val) (t2:type)
| Vptr b1 ofs1, Vlong n2 =>
let n2 := Int.repr (Int64.unsigned n2) in
Some (Vptr b1 (Int.sub ofs1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
+ | Vint n1, Vlong n2 =>
+ let n2 := Int.repr (Int64.unsigned n2) in
+ Some (Vint (Int.sub n1 (Int.mul (Int.repr (sizeof cenv ty)) n2)))
| _, _ => None
end
| sub_case_pp ty => (**r pointer minus pointer *)
@@ -1205,25 +1220,25 @@ Proof.
unfold sem_binary_operation; intros; destruct op.
- (* add *)
unfold sem_add in *; destruct (classify_add ty1 ty2).
- + inv H0; inv H1; inv H. TrivialInject.
+ + inv H0; inv H1; inv H. TrivialInject. TrivialInject.
econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
- + inv H0; inv H1; inv H. TrivialInject.
+ + inv H0; inv H1; inv H. TrivialInject. TrivialInject.
econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
- + inv H0; inv H1; inv H. TrivialInject.
+ + inv H0; inv H1; inv H. TrivialInject. TrivialInject.
econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
- + inv H0; inv H1; inv H. TrivialInject.
+ + inv H0; inv H1; inv H. TrivialInject. TrivialInject.
econstructor. eauto. repeat rewrite Int.add_assoc. decEq. apply Int.add_commut.
+ eapply sem_binarith_inject; eauto; intros; exact I.
- (* sub *)
unfold sem_sub in *; destruct (classify_sub ty1 ty2).
- + inv H0; inv H1; inv H. TrivialInject.
+ + inv H0; inv H1; inv H. TrivialInject. TrivialInject.
econstructor. eauto. rewrite Int.sub_add_l. auto.
+ inv H0; inv H1; inv H. TrivialInject.
destruct (eq_block b1 b0); try discriminate. subst b1.
rewrite H0 in H2; inv H2. rewrite dec_eq_true.
destruct (zlt 0 (sizeof cenv ty) && zle (sizeof cenv ty) Int.max_signed); inv H3.
rewrite Int.sub_shifted. TrivialInject.
- + inv H0; inv H1; inv H. TrivialInject.
+ + inv H0; inv H1; inv H. TrivialInject. TrivialInject.
econstructor. eauto. rewrite Int.sub_add_l. auto.
+ eapply sem_binarith_inject; eauto; intros; exact I.
- (* mul *)
diff --git a/cparser/Cutil.ml b/cparser/Cutil.ml
index c82ada26..c15a7adf 100644
--- a/cparser/Cutil.ml
+++ b/cparser/Cutil.ml
@@ -333,7 +333,7 @@ let rec equal_types env t1 t2 =
| None, None -> true
| Some s1, Some s2 -> s1 = s2
| _ -> false end in
- size && a1 = a2 && equal_types env t1 t2
+ size && a1 = a2 && equal_types env ty1 ty2
| TFun(ty1, params1, vararg1, a1), TFun(ty2, params2, vararg2, a2) ->
let params =
match params1, params2 with
diff --git a/driver/Driver.ml b/driver/Driver.ml
index 77bf52a9..bbd949e0 100644
--- a/driver/Driver.ml
+++ b/driver/Driver.ml
@@ -20,6 +20,9 @@ open Timing
let stdlib_path = ref Configuration.stdlib_path
+(* Use standard headers *)
+let use_standard_headers = ref Configuration.has_standard_headers
+
let dump_options = ref false
(* Optional sdump suffix *)
@@ -105,7 +108,7 @@ let preprocess ifile ofile =
let cmd = List.concat [
Configuration.prepro;
["-D__COMPCERT__"];
- (if Configuration.has_standard_headers
+ (if !use_standard_headers
then ["-I" ^ Filename.concat !stdlib_path "include" ]
else []);
List.rev !prepro_options;
@@ -461,11 +464,36 @@ Processing options:
-o <file> Generate output in <file>
Preprocessing options:
-I<dir> Add <dir> to search path for #include files
+ -include <file> Process <file> as if #include \"<file>\" appears at the first
+ line of the primary source file.
-D<symb>=<val> Define preprocessor symbol
-U<symb> Undefine preprocessor symbol
-Wp,<opt> Pass option <opt> to the preprocessor
- -include <file> Process <file> as if #include \"<file>\" appears at the first
- line of the primary source file.
+ -Xpreprocessor <opt> Pass option <opt> to the preprocessor
+ -M (GCC only) Ouput a rule suitable for make describing the
+ dependencies of the main source file
+ -MM (GCC only) Like -M but do not mention system header files
+ -MF <file> (GCC only) Specifies file <file> as output file for -M or -MM
+ -MG (GCC only) Assumes missing header files are generated for -M
+ -MP (GCC only) Add a phony target for each dependency other than
+ the main file
+ -MT <target> (GCC only) Change the target of the rule emitted by dependency
+ generation
+ -MQ <target> (GCC only) Like -MT but quotes <target>
+ -nostdinc (GCC only) Do not search the standard system directories for
+ header files
+ -imacros <file> (GCC only) Like -include but throws output produced by
+ preprocessing of <file> away
+ -idirafter <dir> (GCC only) Search <dir> for header files after all directories
+ specified with -I and the standard system directories
+ -isystem <dir> (GCC only) Search <dir> for header files after all directories
+ specified by -I but before the standard system directories
+ -iquote <dir> (GCC only) Like -isystem but only for headers included with
+ quotes
+ -P (GCC only) Do not generate linemarkers
+ -C (GCC only) Do not discard comments
+ -CC (GCC only) Do not discard comments, including during macro
+ expansion
Language support options (use -fno-<opt> to turn off -f<opt>) :
-fbitfields Emulate bit fields in structs [off]
-flongdouble Treat 'long double' as 'double' [off]
@@ -569,10 +597,36 @@ let optimization_options = [
let set_all opts = List.iter (fun r -> r := true) opts
let unset_all opts = List.iter (fun r -> r := false) opts
-let gnu_linker_opt s =
+
+let gnu_option s =
if Configuration.system <> "diab" then
+ true
+ else begin
+ eprintf "ccomp: warning: option %s only supported for gcc backend\n" s;
+ false
+ end
+
+let gnu_linker_opt s =
+ if gnu_option s then
push_linker_arg s
+(* Add gnu preprocessor list *)
+let gnu_prepro_opt_key key s =
+ if gnu_option s then
+ prepro_options := s::key::!prepro_options
+
+(* Add gnu preprocessor option *)
+let gnu_prepro_opt s =
+ if gnu_option s then
+ prepro_options := s::!prepro_options
+
+(* Add gnu preprocessor option s and the implict -E *)
+let gnu_prepro_opt_e s =
+ if gnu_option s then begin
+ prepro_options := s :: !prepro_options;
+ option_E := true
+ end
+
let num_source_files = ref 0
let num_input_files = ref 0
@@ -605,7 +659,24 @@ let cmdline_actions =
Prefix "-U", Self(fun s -> prepro_options := s :: !prepro_options);
Prefix "-Wp,", Self (fun s ->
prepro_options := List.rev_append (explode_comma_option s) !prepro_options);
+ Exact "-Xpreprocessor", String (fun s ->
+ prepro_options := s :: !prepro_options);
Exact "-include", String (fun s -> prepro_options := s :: "-include" :: !prepro_options);
+ Exact "-M", Self gnu_prepro_opt_e;
+ Exact "-MM", Self gnu_prepro_opt_e;
+ Exact "-MF", String (gnu_prepro_opt_key "-MF");
+ Exact "-MG", Self gnu_prepro_opt;
+ Exact "-MP", Self gnu_prepro_opt;
+ Exact "-MT", String (gnu_prepro_opt_key "-MT");
+ Exact "-MQ", String (gnu_prepro_opt_key "-MQ");
+ Exact "-nostdinc", Self (fun s -> gnu_prepro_opt s; use_standard_headers := false);
+ Exact "-imacros", String (gnu_prepro_opt_key "-imacros");
+ Exact "-idirafter", String (gnu_prepro_opt_key "-idirafter");
+ Exact "-isystem", String (gnu_prepro_opt_key "-isystem");
+ Exact "-iquote", String (gnu_prepro_opt_key "-iquore");
+ Exact "-P", Self gnu_prepro_opt;
+ Exact "-C", Self gnu_prepro_opt;
+ Exact "-CC", Self gnu_prepro_opt;
(* Language support options -- more below *)
Exact "-fall", Self (fun _ -> set_all language_support_options);
Exact "-fnone", Self (fun _ -> unset_all language_support_options);
generated by cgit (git 2.34.1) at 2024-07-13 13:28:36 +0000