Merge branch 'master' into sb/yosys

Author: chameco

heapster-saw/doc/tutorial/tutorial.md

@@ -0,0 +1,17 @@
+#include <stdint.h>
+
+// Simple function that adds it's two inputs.
+uint64_t add (uint64_t x, uint64_t y) { return x + y; }
+
+// A copy of `add`, that we will use to miss-type a function
+uint64_t add_mistyped (uint64_t x, uint64_t y) { return x + y; }
+
+// Simple function that increments the value in a pointer
+void incr_ptr (uint64_t *x) { *x += 1; }
+
+// Struct that represents the three coordinates for a 3D vector
+typedef struct { uint64_t x; uint64_t y; uint64_t z; } vector3d;
+
+// function that computes the norm of a 3D vector
+// || (x,y,z) || = x^2+y^2+z^2
+uint64_t norm_vector (vector3d *v) { return (v->x * v->x + v->y * v->y + v->z * v->z); }

heapster-saw/examples/tutorial_c.bc

@@ -0,0 +1,23 @@
+enable_experimental;
+env <- heapster_init_env "tutorial_c" "tutorial_c.bc";
+print "File loaded";
+
+heapster_define_perm env "int64" " " "llvmptr 64" "exists x:bv 64.eq(llvmword(x))";
+heapster_typecheck_fun env "add" "().arg0:int64<>, arg1:int64<> -o arg0:true, arg1:true, ret:int64<>";
+print "Type checked add.";
+
+heapster_typecheck_fun env "add_mistyped" "().arg0:true, arg1:int64<> -o arg0:true, arg1:true, ret:int64<>";
+print "Type checked add_mistyped. This will produce an error in the output.";
+
+heapster_typecheck_fun env "incr_ptr" "(). arg0:ptr((W,0) |-> int64<>) -o arg0:ptr((W,0) |-> int64<>)";
+print "Type checked incr_ptr.";
+
+heapster_define_perm env "vec3d" "rw:rwmodality" "llvmptr 64" "ptr((rw,0) |-> int64<>) * ptr((rw,8) |-> int64<>) * ptr((rw,16) |-> int64<>)";
+heapster_typecheck_fun env "norm_vector" "(). arg0:vec3d<R> -o arg0:vec3d<R>, ret:int64<>";
+print "Type checked norm_vector.";
+
+heapster_export_coq env "tutorial_c_gen.v";
+print "Export to Coq.";
+
+print "Done.";
+

heapster-saw/examples/tutorial_c.c

@@ -0,0 +1,29 @@
+
+(** Mandatory imports from saw-core-coq *)
+From Coq Require Import Lists.List.
+From Coq Require Import String.
+From Coq Require Import Vectors.Vector.
+From CryptolToCoq Require Import SAWCoreScaffolding.
+From CryptolToCoq Require Import SAWCoreVectorsAsCoqVectors.
+Import ListNotations.
+
+(** Post-preamble section specified by you *)
+From CryptolToCoq Require Import SAWCorePrelude.
+From CryptolToCoq Require Import SAWCoreBitvectors.
+
+(** Code generated by saw-core-coq *)
+
+Module tutorial_c.
+
+Definition add__tuple_fun : CompM.lrtTupleType (CompM.LRT_Cons (CompM.LRT_Fun (SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool) (fun (perm0 : SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool) => let var__0   := SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool in
+  CompM.LRT_Fun var__0 (fun (perm1 : var__0) => CompM.LRT_Ret (SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool)))) CompM.LRT_Nil) :=
+  @CompM.multiFixM (CompM.LRT_Cons (CompM.LRT_Fun (SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool) (fun (perm0 : SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool) => let var__0   := SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool in
+  CompM.LRT_Fun var__0 (fun (perm1 : var__0) => CompM.LRT_Ret (SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool)))) CompM.LRT_Nil) (fun (add : CompM.lrtToType (CompM.LRT_Fun (SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool) (fun (perm0 : SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool) => let var__0   := SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool in
+  CompM.LRT_Fun var__0 (fun (perm1 : var__0) => CompM.LRT_Ret (SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool))))) => pair (fun (p0 : SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool) (p1 : SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool) => let var__0   := SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool in
+  @CompM.letRecM CompM.LRT_Nil var__0 tt (@returnM CompM _ var__0 (SAWCoreVectorsAsCoqVectors.bvAdd 64 p0 p1))) tt).
+
+Definition add : CompM.lrtToType (CompM.LRT_Fun (SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool) (fun (perm0 : SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool) => let var__0   := SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool in
+  CompM.LRT_Fun var__0 (fun (perm1 : var__0) => CompM.LRT_Ret (SAWCoreVectorsAsCoqVectors.Vec 64 SAWCoreScaffolding.Bool)))) :=
+  SAWCoreScaffolding.fst add__tuple_fun.
+
+End tutorial_c.

heapster-saw/examples/tutorial_c.saw

@@ -0,0 +1,40 @@
+From CryptolToCoq Require Import SAWCoreScaffolding.
+From CryptolToCoq Require Import SAWCorePrelude.
+From CryptolToCoq Require Import CompMExtra.
+
+(* The following line enables pretty printing*)
+Import CompMExtraNotation. Open Scope fun_syntax.
+
+Require Import Examples.tutorial_c_gen.
+Import tutorial_c.
+
+
+Lemma no_errors_add
+  : refinesFun add (fun _ _ => noErrorsSpec).
+Proof.
+  unfold add, add__tuple_fun.
+  prove_refinement.
+Qed.
+  
+Lemma no_errors_add_mistyped
+  : refinesFun add_mistyped (fun _ => noErrorsSpec).
+Proof.
+  unfold add_mistyped, add_mistyped__tuple_fun, noErrorsSpec.
+  prove_refinement. 
+  (* Fails to solve the goal. *)
+Abort.
+
+
+Lemma no_errors_incr_ptr
+  : refinesFun incr_ptr (fun _ => noErrorsSpec).
+Proof.
+  unfold incr_ptr, incr_ptr__tuple_fun, noErrorsSpec.
+  prove_refinement.
+Qed.
+  
+Lemma no_errors_norm_vector
+  : refinesFun norm_vector (fun _ _ _ => noErrorsSpec).
+Proof.
+  unfold norm_vector, norm_vector__tuple_fun, noErrorsSpec.
+  prove_refinement.
+Qed.