[WIP] Add partial semantics for the C AST

_CoqProject

@@ -24,6 +24,7 @@ src/Arithmetic.v
 src/BoundsPipeline.v
 src/CLI.v
 src/COperationSpecifications.v
+src/CSemantics.v
 src/CStringification.v
 src/CompilersTestCases.v
 src/Demo.v

src/CSemantics.v

@@ -0,0 +1,269 @@
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.MSets.MSetPositive.
+Require Import Coq.FSets.FMapPositive.
+Require Import Coq.Strings.String.
+Require Import Coq.Lists.List.
+Require Import Crypto.Util.Strings.StringMap.
+Require Import Crypto.Util.ZRange.
+Require Import Crypto.Util.ZRange.Operations.
+Require Import Crypto.Util.Option.
+(*
+Require Import Coq.Strings.Ascii.
+Require Import Coq.Bool.Bool.
+Require Import Crypto.Util.ListUtil Coq.Lists.List.
+Require Crypto.Util.Strings.String.
+Require Import Crypto.Util.Strings.Decimal.
+Require Import Crypto.Util.Strings.HexString.
+Require Import Crypto.Util.Strings.Show.
+Require Import Crypto.Util.ZRange.Show.
+Require Import Crypto.Util.Option.
+Require Import Crypto.Util.OptionList.
+Require Import Crypto.Language.
+Require Import Crypto.AbstractInterpretation.
+*)
+Require Import Crypto.CStringification.
+Require Import Crypto.Util.ZUtil.Definitions.
+(*
+Require Import Crypto.Util.Bool.Equality.
+Require Import Crypto.Util.Notations.
+
+ *)
+Import ListNotations. Local Open Scope zrange_scope. Local Open Scope Z_scope.
+
+Module Compilers.
+  (*
+  Local Set Boolean Equality Schemes.
+  Local Set Decidable Equality Schemes.
+  Export Language.Compilers.
+  Export AbstractInterpretation.Compilers.
+   *)
+  Export CStringification.Compilers.
+  (*
+  Import invert_expr.
+  Import defaults.
+   *)
+
+  Module ToString.
+    Export CStringification.Compilers.ToString.
+
+    Module C.
+      Export CStringification.Compilers.ToString.C.
+      Export CStringification.Compilers.ToString.C.int.Notations.
+
+      Module int.
+        Record int (r : zrange)
+          := Build_int' { value : Z ; bounded : is_bounded_by_bool value r = true }.
+        Global Arguments value {r} _.
+
+        (** A version that always gives [eq_refl] on concrete values in the second component *)
+        Definition Build_int (r : zrange) (value : Z) (bounded : is_bounded_by_bool value r = true)
+          : int r
+          := Build_int' r value
+                        (match is_bounded_by_bool value r as b return b = true -> b = true with
+                         | true => fun _ => eq_refl
+                         | false => fun pf => pf
+                         end bounded).
+
+        Definition maybe_Build_int (r : zrange) (value : Z) : option (int r)
+          := match is_bounded_by_bool value r as b return is_bounded_by_bool value r = b -> option (int r) with
+             | true => fun pf => Some (Build_int' r value pf)
+             | false => fun _ => None
+             end eq_refl.
+
+        Definition interp (t : int.type) := int (int.to_zrange t).
+      End int.
+
+      Module primitive.
+        Definition interp (t : type.primitive) : Type
+          := match t with
+             | type.Z => { sz : int.type & int.interp sz }
+             | type.Zptr => string
+             end.
+      End primitive.
+
+      Module type.
+        Fixpoint interp (t : type)
+          := match t with
+             | type.type_primitive t => primitive.interp t
+             | type.prod A B => interp A * interp B
+             | type.unit => unit
+             end%type.
+      End type.
+
+      Inductive memory_value :=
+      | mem_int (sz : int.type) (v : int.interp sz)
+      | mem_int_array (sz : int.type) (v : list (int.interp sz)).
+
+      Lemma literal_good {v}
+        : is_bounded_by_bool v (int.to_zrange (int.of_zrange_relaxed r[v ~> v])) = true.
+      Proof using Type.
+        (* XXX TODO *)
+      Admitted.
+
+      Definition make_Literal (v : Z) : option {sz : int.type & int.interp sz}
+        := Some (existT _ (int.of_zrange_relaxed r[v~>v])
+                        (int.Build_int' _ v literal_good)).
+
+      Axiom proof_admitted : False.
+      Local Notation admit := match proof_admitted with end.
+
+      Fixpoint interp_arith_expr
+               (ctx : StringMap.t memory_value) (* name -> value *)
+               {t : type} (e : arith_expr t)
+        : option (type.interp t * StringMap.t memory_value).
+      Proof.
+        refine match e in arith_expr t return option (type.interp t * StringMap.t memory_value) with
+               | AppIdent s d idc arg
+                 => arg_value_ctx <- @interp_arith_expr ctx s arg;
+                      let '(arg_value, ctx) := arg_value_ctx in
+                      (** Here is where we define most of the C semantics *)
+                      match idc in ident s d return arith_expr s -> type.interp s -> option (type.interp d * StringMap.t memory_value) with
+                      | literal v
+                        => fun _ _
+                           => res <- make_Literal v;
+                                Some (res, ctx)
+                      | List_nth n
+                        => fun _ ptr
+                           => val <- StringMap.find ptr ctx;
+                                match val with
+                                | mem_int_array sz ls
+                                  => val' <- nth_error ls n;
+                                       Some (existT _ _ val', ctx)
+                                | mem_int _ _ => None
+                                end
+                      | Addr
+                        => fun arg _
+                           => match arg with
+                              | Var type.Z name => Some (name, ctx)
+                              | _ => None
+                              end
+                      | Dereference
+                        => fun _ ptr
+                           => val <- StringMap.find ptr ctx;
+                                match val with
+                                | mem_int sz v
+                                  => Some (existT _ sz v, ctx)
+                                | mem_int_array _ _ => None
+                                end
+                      | Z_shiftr offset
+                        => fun _ '(existT sz x)
+                           => let res := Z.shiftr (int.value x) offset in
+                              (* TODO: Perform type promotion on the integer type [sz] *)
+                              let sz_out := admit in
+                              res' <- int.maybe_Build_int (int.to_zrange sz_out) res;
+                                (* TODO: decide what type [res] should go in, figure out whether or not behavior is undefined, etc; return [None] if needed *)
+                                Some (existT _ _ res', ctx)
+                      | Z_shiftl offset
+                        => fun _ '(existT sz x)
+                           => let res := Z.shiftl (int.value x) offset in
+                              (* TODO: Perform type promotion on the integer type [sz] *)
+                              let sz_out := admit in
+                              res' <- int.maybe_Build_int (int.to_zrange sz_out) res;
+                                (* TODO: decide what type [res] should go in, figure out whether or not behavior is undefined, etc; return [None] if needed *)
+                                Some (existT _ _ res', ctx)
+                      | Z_land
+                        => fun _ '(existT x_sz x, existT y_sz y)
+                           => let res := Z.land (int.value x) (int.value y) in
+                              (* TODO: Perform type promotion on the integer type [sz] *)
+                              let sz_out := admit in
+                              res' <- int.maybe_Build_int (int.to_zrange sz_out) res;
+                                (* TODO: decide what type [res] should go in, figure out whether or not behavior is undefined, etc; return [None] if needed *)
+                                Some (existT _ _ res', ctx)
+                      | Z_lor
+                        => fun _ '(existT x_sz x, existT y_sz y)
+                           => let res := Z.lor (int.value x) (int.value y) in
+                              (* TODO: Perform type promotion on the integer type [sz] *)
+                              let sz_out := admit in
+                              res' <- int.maybe_Build_int (int.to_zrange sz_out) res;
+                                (* TODO: decide what type [res] should go in, figure out whether or not behavior is undefined, etc; return [None] if needed *)
+                                Some (existT _ _ res', ctx)
+                      | Z_add
+                        => fun _ '(existT x_sz x, existT y_sz y)
+                           => let res := Z.add (int.value x) (int.value y) in
+                              (* TODO: Perform type promotion on the integer type [sz] *)
+                              let sz_out := admit in
+                              res' <- int.maybe_Build_int (int.to_zrange sz_out) res;
+                                (* TODO: decide what type [res] should go in, figure out whether or not behavior is undefined, etc; return [None] if needed *)
+                                Some (existT _ _ res', ctx)
+                      | Z_mul
+                        => fun _ '(existT x_sz x, existT y_sz y)
+                           => let res := Z.mul (int.value x) (int.value y) in
+                              (* TODO: Perform type promotion on the integer type [sz] *)
+                              let sz_out := admit in
+                              res' <- int.maybe_Build_int (int.to_zrange sz_out) res;
+                                (* TODO: decide what type [res] should go in, figure out whether or not behavior is undefined, etc; return [None] if needed *)
+                                Some (existT _ _ res', ctx)
+                      | Z_sub
+                        => fun _ '(existT x_sz x, existT y_sz y)
+                           => let res := Z.sub (int.value x) (int.value y) in
+                              (* TODO: Perform type promotion on the integer type [sz] *)
+                              let sz_out := admit in
+                              res' <- int.maybe_Build_int (int.to_zrange sz_out) res;
+                                (* TODO: decide what type [res] should go in, figure out whether or not behavior is undefined, etc; return [None] if needed *)
+                                Some (existT _ _ res', ctx)
+                      | Z_opp
+                        => fun _ '(existT x_sz x)
+                           => let res := Z.opp (int.value x) in
+                              (* TODO: Perform type promotion on the integer type [sz] *)
+                              let sz_out := admit in
+                              res' <- int.maybe_Build_int (int.to_zrange sz_out) res;
+                                (* TODO: decide what type [res] should go in, figure out whether or not behavior is undefined, etc; return [None] if needed *)
+                                Some (existT _ _ res', ctx)
+                      | Z_lnot ty
+                        => fun _ '(existT x_sz x)
+                           => (** TODO: figure out what to do here *)
+                             admit
+                      | Z_bneg
+                        => fun _ '(existT x_sz x)
+                           => (** TODO: figure out what to do here *)
+                             admit
+                      | Z_mul_split lgs => admit
+                      | Z_add_with_get_carry lgs => admit
+                      | Z_sub_with_get_borrow lgs => admit
+                      | Z_zselect ty => admit
+                      | Z_add_modulo => admit
+                      | Z_static_cast ty => admit
+                      end arg arg_value
+               | Var type.Z v
+                 => v' <- StringMap.find v ctx;
+                      match v' with
+                      | mem_int sz v'' => Some (existT _ sz v'', ctx)
+                      | mem_int_array _ _ => None
+                      end
+               | Var type.Zptr v => Some (v, ctx)
+               | Pair A B a b
+                 => a' <- @interp_arith_expr ctx A a;
+                      let '(a', ctx) := a' in
+                      b' <- @interp_arith_expr ctx B b;
+                        let '(b', ctx) := b' in
+                        Some ((a', b'), ctx)
+               | TT => Some (tt, ctx)
+               end%option;
+          cbn [type.interp primitive.interp] in *; cbv [primitive.interp] in *.
+      Defined.
+
+      Definition interp_stmt
+                 (code : stmt)
+        : StringMap.t memory_value -> option (StringMap.t memory_value).
+        refine match code with
+               | Call val => _
+               | Assign declare t sz name val => _
+               | AssignZPtr name sz val => _
+               | DeclareVar t sz name => _
+               | AssignNth name n val => _
+               end.
+      Admitted.
+
+      Fixpoint interp_expr
+               (ctx : StringMap.t memory_value)
+               (e : expr)
+        : option (StringMap.t memory_value)
+        := match e with
+           | nil => Some ctx
+           | code :: rest
+             => ctx' <- interp_stmt code ctx;
+                  interp_expr ctx' rest
+           end%option.
+    End C.
+  End ToString.
+End Compilers.