Qualified path names now start with VST.floyd, VST.veric, etc.,

for any files in these directories: VSTDIRS= msl sepcomp veric floyd progs concurrency ccc26x86 Qualified path names are unchanged to refer to any files in: OTHERDIRS= wand_demo sha fcf hmacfcf tweetnacl20140427 hmacdrbg aes mailbox The reason for doing this is to make it easier to integrate VST with other systems such as FCF, Ramification, etc.
PrincetonUniversity · Aug 15, 2017 · 9a2ac66 · 9a2ac66
1 parent dafb0df
commit 9a2ac66
Show file tree

Hide file tree

Showing 560 changed files with 3,670 additions and 3,680 deletions.
diff --git a/Makefile b/Makefile
@@ -29,12 +29,9 @@ COMPCERT ?= compcert
 
 CC_TARGET=compcert/cfrontend/Clight.vo
 CC_DIRS= lib common cfrontend exportclight
-DIRS= msl sepcomp veric floyd progs wand_demo sha fcf hmacfcf tweetnacl20140427 ccc26x86 hmacdrbg aes mailbox concurrency
-INCLUDE= $(foreach a,$(DIRS),$(if $(wildcard $(a)), -Q $(a) $(a))) -R $(COMPCERT) compcert -as compcert $(if $(MATHCOMP), -Q mathcomp $(MATHCOMP))
-#Replace the INCLUDE above with the following in order to build the linking target:
-#INCLUDE= $(foreach a,$(DIRS),$(if $(wildcard $(a)), -I $(a) -as $(a))) -R $(COMPCERT) -as compcert -I $(SSREFLECT)/src -R $(SSREFLECT)/theories -as Ssreflect \
-#  -R $(MATHCOMP)/theories -as MathComp
-# $(foreach a,$(CC_DIRS), -R $(COMPCERT)/$(a) -as compcert.$(a)) -I $(COMPCERT)/flocq -as compcert.flocq
+VSTDIRS= msl sepcomp veric floyd progs concurrency ccc26x86 
+OTHERDIRS= wand_demo sha fcf hmacfcf tweetnacl20140427 hmacdrbg aes mailbox
+DIRS = $(VSTDIRS) $(OTHERDIRS)
 CONCUR = concurrency
 
 CV1=$(shell cat compcert/VERSION)
@@ -58,13 +55,9 @@ ifdef MATHCOMP
  EXTFLAGS:=$(EXTFLAGS) -R $(MATHCOMP) mathcomp
 endif
 
-COQFLAGS=$(foreach d, $(DIRS), $(if $(wildcard $(d)), -Q $(d) $(d))) $(EXTFLAGS)
+COQFLAGS=$(foreach d, $(VSTDIRS), $(if $(wildcard $(d)), -Q $(d) VST.$(d))) $(foreach d, $(OTHERDIRS), $(if $(wildcard $(d)), -Q $(d) $(d))) $(EXTFLAGS)
 DEPFLAGS:=$(COQFLAGS)
 
-ifdef LIBPREFIX
- COQFLAGS=$(foreach d, $(DIRS), $(if $(wildcard $(d)), -Q $(d) $(LIBPREFIX).$(d))) $(EXTFLAGS)
-endif
-
 COQC=$(COQBIN)coqc -w none
 COQTOP=$(COQBIN)coqtop
 COQDEP=$(COQBIN)coqdep $(DEPFLAGS)
@@ -256,7 +249,7 @@ PROGS_FILES= \
   merge.v verif_merge.v verif_append.v verif_append2.v bst.v bst_oo.v verif_bst.v verif_bst_oo.v \
   verif_bin_search.v verif_floyd_tests.v \
   verif_sumarray2.v verif_switch.v verif_message.v verif_object.v \
-  funcptr.v verif_funcptr.v
+  funcptr.v verif_funcptr.v ghost.v
 # verif_dotprod.v verif_insertion_sort.v
 
 SHA_FILES= \
@@ -358,7 +351,7 @@ AES_FILES = \
 #  verif_hmac_drbg_update.v verif_hmac_drbg_reseed.v verif_hmac_drbg_generate.v
 
 
-C_FILES = reverse.c queue.c queue2.c sumarray.c sumarray2.c message.c object.c insertionsort.c float.c global.c nest3.c nest2.c nest3.c load_demo.c dotprod.c string.c field_loadstore.c ptr_compare.c merge.c append.c bst.c min.c switch.c funcptr.c
+C_FILES = reverse.c queue.c queue2.c sumarray.c sumarray2.c message.c object.c insertionsort.c float.c global.c nest3.c nest2.c nest3.c load_demo.c dotprod.c string.c field_loadstore.c ptr_compare.c merge.c append.c bst.c min.c switch.c funcptr.c store_demo.c floyd_tests.c
 
 FILES = \
  $(MSL_FILES:%=msl/%) \
@@ -568,6 +561,7 @@ dep:
 .depend depend:
 #	$(COQDEP) $(filter $(wildcard *.v */*.v */*/*.v),$(FILES))  > .depend
 	@echo 'coqdep ... >.depend'
+#	$(COQDEP) >.depend `find compcert $(filter $(wildcard *), $(DIRS)) -name "*.v"`
 	-@$(COQDEP) 2>&1 >.depend `find compcert $(filter $(wildcard *), $(DIRS)) -name "*.v"` | grep -v Warning:
 
 depend-paco:

diff --git a/aes/api_specs.v b/aes/api_specs.v
@@ -1,5 +1,5 @@
-Require Export floyd.proofauto.
-Require Export floyd.reassoc_seq.
+Require Export VST.floyd.proofauto.
+Require Export VST.floyd.reassoc_seq.
 Require Export aes.aes.
 Require Export aes.GF_ops_LL.
 Require Export aes.tablesLL.

diff --git a/aes/list_lemmas.v b/aes/list_lemmas.v
@@ -1,7 +1,7 @@
 Require Export aes.list_utils.
 Require Export ZArith.
 Local Open Scope Z_scope.
-Require Export floyd.sublist.
+Require Export VST.floyd.sublist.
 
 Lemma Znth_fill_list: forall {T: Type} (i n: Z) (f: Z -> T) (d: T),
   0 <= i < n ->

diff --git a/aes/list_utils.v b/aes/list_utils.v
@@ -1,7 +1,7 @@
 Require Export List. Export ListNotations.
 Require Import ZArith.
 Local Open Scope Z_scope.
-Require Import floyd.sublist.
+Require Import VST.floyd.sublist.
 
 Fixpoint repeat_op_nat{T: Type}(n: nat)(start: T)(op: T -> T): T := match n with
 | O => start

diff --git a/aes/partially_filled.v b/aes/partially_filled.v
@@ -1,7 +1,7 @@
 Require Import ZArith.
 Local Open Scope Z_scope.
 Require Import Integers.
-Require Import floyd.sublist.
+Require Import VST.floyd.sublist.
 Require Import compcert.common.Values.
 Require Export List. Export ListNotations.
 Require Export aes.list_utils.

diff --git a/aes/spec_AES256_HL.v b/aes/spec_AES256_HL.v
@@ -1,4 +1,4 @@
-Require Export floyd.sublist.
+Require Export VST.floyd.sublist.
 Require Export Integers.
 Require Export Coqlib.
 Require Export List. Import ListNotations.

diff --git a/aes/spec_utils_LL.v b/aes/spec_utils_LL.v
@@ -2,7 +2,7 @@ Require Export List. Export ListNotations.
 Require Export ZArith.
 Local Open Scope Z_scope.
 Require Export Integers.
-Require Export floyd.sublist.
+Require Export VST.floyd.sublist.
 
 Definition Nk := 8. (* number of words in key *)
 Definition Nr := 14. (* number of cipher rounds *)

diff --git a/aes/tablesLL.v b/aes/tablesLL.v
@@ -2,7 +2,7 @@ Require Import List. Import ListNotations.
 Require Import ZArith.
 Local Open Scope Z_scope.
 Require Import Integers.
-Require Import floyd.sublist.
+Require Import VST.floyd.sublist.
 Require Import aes.sbox.
 Require Import aes.GF_ops_LL.
 Require Import aes.list_utils.

diff --git a/ccc26x86/Asm.v b/ccc26x86/Asm.v
@@ -22,9 +22,9 @@ Require Import compcert.common.Memory.
 Require Import compcert.common.Events.
 Require Import compcert.common.Globalenvs.
 Require Import compcert.common.Smallstep.
-Require Import ccc26x86.Locations.
-Require Import ccc26x86.Stacklayout.
-Require Import ccc26x86.Conventions.
+Require Import VST.ccc26x86.Locations.
+Require Import VST.ccc26x86.Stacklayout.
+Require Import VST.ccc26x86.Conventions.
 
 (** * Abstract syntax *)
 

diff --git a/ccc26x86/Asm_coop.v b/ccc26x86/Asm_coop.v
@@ -8,19 +8,19 @@ Require Import compcert.common.Memory.
 Require Import compcert.common.Events.
 Require Import compcert.common.Globalenvs.
 Require Import compcert.common.Smallstep.
-Require Import ccc26x86.Locations.
+Require Import VST.ccc26x86.Locations.
 (*Require Import Stacklayout.*)
-Require Import ccc26x86.Conventions.
+Require Import VST.ccc26x86.Conventions.
 
-Require Import ccc26x86.Asm.
+Require Import VST.ccc26x86.Asm.
 (*LENB: In CompComp, we used a modified Asm.v, called Asm.comp.v*)
 
-Require Import sepcomp.mem_lemmas.
-Require Import sepcomp.semantics.
-Require Import sepcomp.semantics_lemmas.
-Require Import sepcomp.val_casted.
-Require Import ccc26x86.BuiltinEffects.
-Require Import ccc26x86.load_frame.
+Require Import VST.sepcomp.mem_lemmas.
+Require Import VST.sepcomp.semantics.
+Require Import VST.sepcomp.semantics_lemmas.
+Require Import VST.sepcomp.val_casted.
+Require Import VST.ccc26x86.BuiltinEffects.
+Require Import VST.ccc26x86.load_frame.
 
 Notation SP := ESP (only parsing).
 

diff --git a/ccc26x86/Asm_eff.v b/ccc26x86/Asm_eff.v
@@ -7,21 +7,21 @@ Require Export compcert.lib.Maps.
 Require Import compcert.common.Events.
 Require Import compcert.common.Globalenvs.
 Require Import compcert.common.Smallstep.
-Require Import ccc26x86.Locations.
-Require Import ccc26x86.Stacklayout.
-Require Import ccc26x86.Conventions.
+Require Import VST.ccc26x86.Locations.
+Require Import VST.ccc26x86.Stacklayout.
+Require Import VST.ccc26x86.Conventions.
 
 (*LENB: again, in Compcomp we imported the modified Asm_comp*)
-Require Import ccc26x86.Asm.
-Require Import ccc26x86.Asm_coop.
+Require Import VST.ccc26x86.Asm.
+Require Import VST.ccc26x86.Asm_coop.
 
-Require Import sepcomp.mem_lemmas. (*for mem_forward*)
-Require Import sepcomp.semantics.
-Require Import sepcomp.effect_semantics.
-Require Import ccc26x86.BuiltinEffects.
-Require Import ccc26x86.load_frame.
+Require Import VST.sepcomp.mem_lemmas. (*for mem_forward*)
+Require Import VST.sepcomp.semantics.
+Require Import VST.sepcomp.effect_semantics.
+Require Import VST.ccc26x86.BuiltinEffects.
+Require Import VST.ccc26x86.load_frame.
 
-Require Import msl.Extensionality.
+Require Import VST.msl.Extensionality.
 
 Notation SP := ESP (only parsing).
 

diff --git a/ccc26x86/Asm_event.v b/ccc26x86/Asm_event.v
@@ -8,21 +8,21 @@ Require Import compcert.common.Memory.
 Require Import compcert.common.Events.
 Require Import compcert.common.Globalenvs.
 Require Import compcert.common.Smallstep.
-Require Import ccc26x86.Locations.
+Require Import VST.ccc26x86.Locations.
 (*Require Import Stacklayout.*)
-Require Import ccc26x86.Conventions.
+Require Import VST.ccc26x86.Conventions.
 
-Require Import ccc26x86.Asm.
+Require Import VST.ccc26x86.Asm.
 (*LENB: In CompComp, we used a modified Asm.v, called Asm.comp.v*)
 
-Require Import sepcomp.mem_lemmas.
-Require Import sepcomp.semantics.
-Require Import sepcomp.semantics_lemmas.
-Require Import sepcomp.val_casted.
-Require Import ccc26x86.BuiltinEffects.
-Require Import ccc26x86.load_frame.
-Require Import sepcomp.event_semantics.
-Require Import ccc26x86.Asm_coop.
+Require Import VST.sepcomp.mem_lemmas.
+Require Import VST.sepcomp.semantics.
+Require Import VST.sepcomp.semantics_lemmas.
+Require Import VST.sepcomp.val_casted.
+Require Import VST.ccc26x86.BuiltinEffects.
+Require Import VST.ccc26x86.load_frame.
+Require Import VST.sepcomp.event_semantics.
+Require Import VST.ccc26x86.Asm_coop.
 
 Require Import List. Import ListNotations.
 (*

diff --git a/ccc26x86/Asm_nucular.v b/ccc26x86/Asm_nucular.v
@@ -9,27 +9,27 @@ Require Import compcert.common.Memory.
 Require Import compcert.common.Events.
 Require Import compcert.common.Globalenvs.
 Require Import compcert.common.Smallstep.
-Require Import ccc26x86.Locations.
-Require Import ccc26x86.Stacklayout.
-Require Import ccc26x86.Conventions.
+Require Import VST.ccc26x86.Locations.
+Require Import VST.ccc26x86.Stacklayout.
+Require Import VST.ccc26x86.Conventions.
 
-Require Import sepcomp.val_casted.
-Require Import ccc26x86.BuiltinEffects.
-Require Import ccc26x86.load_frame.
+Require Import VST.sepcomp.val_casted.
+Require Import VST.ccc26x86.BuiltinEffects.
+Require Import VST.ccc26x86.load_frame.
 
-Require Import sepcomp.semantics.
-Require Import sepcomp.semantics_lemmas.
+Require Import VST.sepcomp.semantics.
+Require Import VST.sepcomp.semantics_lemmas.
 (*Require Import mem_welldefined.*)
-Require Import sepcomp.mem_wd.
-Require Import sepcomp.mem_lemmas.
-Require Import sepcomp.reach.
-Require Import sepcomp.nucular_semantics.
+Require Import VST.sepcomp.mem_wd.
+Require Import VST.sepcomp.mem_lemmas.
+Require Import VST.sepcomp.reach.
+Require Import VST.sepcomp.nucular_semantics.
 
 (*LENB: Again, in POPL-compcomp we didn't import CompCert's original Asm.v,
 but the modified one*)
 (*Require Import Asm_comp.*)
-Require Import ccc26x86.Asm.
-Require Import ccc26x86.Asm_coop.
+Require Import VST.ccc26x86.Asm.
+Require Import VST.ccc26x86.Asm_coop.
 Notation SP := ESP (only parsing).
 
 (** * CompCert IA32 Asm is [nucular] *)

diff --git a/ccc26x86/Bounds.v b/ccc26x86/Bounds.v
@@ -13,13 +13,13 @@
 (** Computation of resource bounds for Linear code. *)
 
 Require Import FSets FSetAVL.
-Require Import compcert.lib.Coqlib ccc26x86.Ordered.
+Require Import compcert.lib.Coqlib VST.ccc26x86.Ordered.
 Require Intv.
 Require Import compcert.common.AST.
-Require Import ccc26x86.Op.
-Require Import ccc26x86.Machregs ccc26x86.Locations.
-Require Import ccc26x86.Linear.
-Require Import ccc26x86.Conventions.
+Require Import VST.ccc26x86.Op.
+Require Import VST.ccc26x86.Machregs VST.ccc26x86.Locations.
+Require Import VST.ccc26x86.Linear.
+Require Import VST.ccc26x86.Conventions.
 
 Module RegOrd := OrderedIndexed (IndexedMreg).
 Module RegSet := FSetAVL.Make (RegOrd).

diff --git a/ccc26x86/BuiltinEffects.v b/ccc26x86/BuiltinEffects.v
@@ -9,18 +9,18 @@ Require Import compcert.common.Events.
 Require Import compcert.common.Globalenvs.
 
 Require Import compcert.cfrontend.Ctypes. (*for type and access_mode*)
-Require Import sepcomp.mem_lemmas. (*needed for definition of valid_block_dec etc*)
+Require Import VST.sepcomp.mem_lemmas. (*needed for definition of valid_block_dec etc*)
 
-Require Import msl.Axioms.
-Require Import sepcomp.structured_injections.
-Require Import sepcomp.reach.
-Require Import sepcomp.semantics.
-Require Import sepcomp.semantics_lemmas.
-Require Import sepcomp.effect_semantics.
-Require Import sepcomp.effect_properties.
-Require Import sepcomp.globalSep.
+Require Import VST.msl.Axioms.
+Require Import VST.sepcomp.structured_injections.
+Require Import VST.sepcomp.reach.
+Require Import VST.sepcomp.semantics.
+Require Import VST.sepcomp.semantics_lemmas.
+Require Import VST.sepcomp.effect_semantics.
+Require Import VST.sepcomp.effect_properties.
+Require Import VST.sepcomp.globalSep.
 
-Require Import ccc26x86.I64Helpers.
+Require Import VST.ccc26x86.I64Helpers.
 
 Definition memcpy_Effect sz vargs m:=
        match vargs with
@@ -1464,7 +1464,7 @@ destruct ef; simpl in *; try reflexivity.
 contradiction. contradiction.
 Qed.
 *)
-Require Import ccc26x86.Conventions.
+Require Import VST.ccc26x86.Conventions.
 Lemma BuiltinEffect_decode: forall F V (ge: Genv.t F V) ef tls,
  BuiltinEffect ge ef (map tls (loc_arguments (ef_sig ef))) =
  BuiltinEffect ge ef (decode_longs (sig_args (ef_sig ef))

diff --git a/ccc26x86/Clight_coop.v b/ccc26x86/Clight_coop.v
@@ -13,13 +13,13 @@ Require Import Ctypes.
 Require Import Cop.
 
 Require Import compcert.cfrontend.Clight.
-Require Import sepcomp.mem_lemmas.
+Require Import VST.sepcomp.mem_lemmas.
 
-Require Import sepcomp.semantics.
-Require Import sepcomp.semantics_lemmas.
+Require Import VST.sepcomp.semantics.
+Require Import VST.sepcomp.semantics_lemmas.
 
-Require Import ccc26x86.BuiltinEffects.
-Require Import sepcomp.val_casted.
+Require Import VST.ccc26x86.BuiltinEffects.
+Require Import VST.sepcomp.val_casted.
 
 Section CLIGHT_MEM.
 

diff --git a/ccc26x86/Clight_eff.v b/ccc26x86/Clight_eff.v
@@ -7,15 +7,15 @@ Require Export Maps.
 Require Import Events.
 Require Import Globalenvs.
 
-Require Import sepcomp.mem_lemmas. (*for mem_forward*)
-Require Import sepcomp.semantics.
-Require Import sepcomp.effect_semantics.
+Require Import VST.sepcomp.mem_lemmas. (*for mem_forward*)
+Require Import VST.sepcomp.semantics.
+Require Import VST.sepcomp.effect_semantics.
 
 Require Import Cop. (*for sem_cast*)
 Require Import Ctypes. (*for access_mode*)
 Require Import compcert.cfrontend.Clight.
-Require Import ccc26x86.Clight_coop.
-Require Import ccc26x86.BuiltinEffects.
+Require Import VST.ccc26x86.Clight_coop.
+Require Import VST.ccc26x86.BuiltinEffects.
 
 Definition assign_loc_Effect ge (ty:type) (b: block) (ofs: int) : (block -> Z -> bool)  :=
   match access_mode ty with

diff --git a/ccc26x86/Cminor.v b/ccc26x86/Cminor.v
@@ -25,7 +25,7 @@ Require Import compcert.common.Values.
 Require Import compcert.common.Memory.
 Require Import compcert.common.Globalenvs.
 Require Import compcert.common.Smallstep.
-Require Import ccc26x86.Switch.
+Require Import VST.ccc26x86.Switch.
 
 (** * Abstract syntax *)
 

diff --git a/ccc26x86/Conventions.v b/ccc26x86/Conventions.v
@@ -15,8 +15,8 @@
 
 Require Import compcert.lib.Coqlib.
 Require Import compcert.common.AST.
-Require Import ccc26x86.Locations.
-Require Export ccc26x86.Conventions1.
+Require Import VST.ccc26x86.Locations.
+Require Export VST.ccc26x86.Conventions1.
 
 (** The processor-dependent and EABI-dependent definitions are in
     [arch/abi/Conventions1.v].  This file adds various processor-independent

diff --git a/ccc26x86/Conventions1.v b/ccc26x86/Conventions1.v
@@ -14,10 +14,10 @@
     machine registers and stack slots. *)
 
 Require Import compcert.lib.Coqlib.
-Require Import ccc26x86.Decidableplus.
+Require Import VST.ccc26x86.Decidableplus.
 Require Import compcert.common.AST.
 Require Import compcert.common.Events.
-Require Import ccc26x86.Locations.
+Require Import VST.ccc26x86.Locations.
 
 (** * Classification of machine registers *)