diff options
author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-28 12:51:16 +0000 |
---|---|---|
committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2011-07-28 12:51:16 +0000 |
commit | 4af1682d04244bab9f793e00eb24090153a36a0f (patch) | |
tree | a9a70d236c06a78aa9b607c6a41e09b80651aa51 /cparser/StructAssign.ml | |
parent | d8d1bf1aa09373f64aa1b1e6cdfb914c23a910be (diff) | |
download | compcert-4af1682d04244bab9f793e00eb24090153a36a0f.tar.gz compcert-4af1682d04244bab9f793e00eb24090153a36a0f.zip |
Added animation of the CompCert C semantics (ccomp -interp)
test/regression: int main() so that interpretation works
Revised once more implementation of __builtin_memcpy (to check for PPC & ARM)
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@1688 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
Diffstat (limited to 'cparser/StructAssign.ml')
-rw-r--r-- | cparser/StructAssign.ml | 50 |
1 files changed, 23 insertions, 27 deletions
diff --git a/cparser/StructAssign.ml b/cparser/StructAssign.ml index edf88213..6d38b551 100644 --- a/cparser/StructAssign.ml +++ b/cparser/StructAssign.ml @@ -50,20 +50,17 @@ let default_memcpy () = memcpy_decl := Some id; (id, memcpy_type) -let rec find_memcpy env = function - | [] -> - default_memcpy() - | name :: rem -> - try lookup_function env name with Env.Error _ -> find_memcpy env rem - -let memcpy_1_ident env = - find_memcpy env ["__builtin_memcpy"; "memcpy"] -let memcpy_2_ident env = - find_memcpy env ["__builtin_memcpy_al2"; "__builtin_memcpy"; "memcpy"] -let memcpy_4_ident env = - find_memcpy env ["__builtin_memcpy_al4"; "__builtin_memcpy"; "memcpy"] -let memcpy_8_ident env = - find_memcpy env ["__builtin_memcpy_al8"; "__builtin_memcpy"; "memcpy"] +let find_memcpy env = + try + (lookup_function env "__builtin_memcpy_aligned", true) + with Env.Error _ -> + try + (lookup_function env "__builtin_memcpy", false) + with Env.Error _ -> + try + (lookup_function env "memcpy", false) + with Env.Error _ -> + (default_memcpy(), false) (* Smart constructor for "," expressions *) @@ -84,20 +81,19 @@ let rec addrof e = [lhs] and [rhs] must be l-values. *) let transf_assign env lhs rhs = - let (al, sz) = - match Cutil.alignof env lhs.etyp, Cutil.sizeof env lhs.etyp with - | Some al, Some sz -> (al, sz) - | _, _ -> (1, 1) in - let (ident, ty) = - if al mod 8 = 0 && sz mod 8 = 0 then memcpy_8_ident env - else if al mod 4 = 0 && sz mod 4 = 0 then memcpy_4_ident env - else if al mod 2 = 0 && sz mod 2 = 0 then memcpy_2_ident env - else memcpy_1_ident env in + let al = + match Cutil.alignof env lhs.etyp with Some al -> al | None -> 1 in + let ((ident, ty), four_args) = find_memcpy env in let memcpy = {edesc = EVar(ident); etyp = ty} in - let e_lhs = addrof lhs in - let e_rhs = addrof rhs in - let e_size = {edesc = ESizeof(lhs.etyp); etyp = TInt(size_t_ikind, [])} in - {edesc = ECall(memcpy, [e_lhs; e_rhs; e_size]); etyp = TVoid[]} + let e_lhs = addrof lhs + and e_rhs = addrof rhs + and e_size = {edesc = ESizeof(lhs.etyp); etyp = TInt(size_t_ikind, [])} + and e_align = intconst (Int64.of_int al) size_t_ikind in + let args = + if four_args + then [e_lhs; e_rhs; e_size; e_align] + else [e_lhs; e_rhs; e_size] in + {edesc = ECall(memcpy, args); etyp = TVoid[]} (* Detect invariant l-values *) |