//# 1 errors, 76 messages
//#
/*
    //#PreviewThemeImageServlet.java:1:1: class: org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet
 * Licensed to the Apache Software Foundation (ASF) under one or more
 *  contributor license agreements.  The ASF licenses this file to You
 * under the Apache License, Version 2.0 (the "License"); you may not
 * use this file except in compliance with the License.
 * You may obtain a copy of the License at
 *
 *     http://www.apache.org/licenses/LICENSE-2.0
 *
 * Unless required by applicable law or agreed to in writing, software
 * distributed under the License is distributed on an "AS IS" BASIS,
 * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
 * See the License for the specific language governing permissions and
 * limitations under the License.  For additional information regarding
 * copyright in this work, please see the NOTICE file in the top level
 * directory of this distribution.
 */

package org.apache.roller.weblogger.ui.rendering.servlets;

import java.io.IOException;
import java.io.InputStream;
import java.io.OutputStream;
import javax.servlet.ServletConfig;
import javax.servlet.ServletContext;
import javax.servlet.ServletException;
import javax.servlet.http.HttpServlet;
import javax.servlet.http.HttpServletRequest;
import javax.servlet.http.HttpServletResponse;
import org.apache.commons.logging.Log;
import org.apache.commons.logging.LogFactory;
import org.apache.roller.weblogger.business.WebloggerFactory;
import org.apache.roller.weblogger.business.themes.SharedTheme;
import org.apache.roller.weblogger.business.themes.ThemeManager;
import org.apache.roller.weblogger.pojos.ThemeResource;
import org.apache.roller.weblogger.ui.rendering.util.ModDateHeaderUtil;

/**
 * Special previewing servlet which serves files uploaded by users as well as 
 * static resources in shared themes.  This servlet differs from the normal
 * ResourceServlet because it can accept urls parameters which affect how it
 * behaves which are used for previewing.
 */
public class PreviewThemeImageServlet extends HttpServlet {
    //#PreviewThemeImageServlet.java:44: method: void org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet.org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet()
    //#input(void org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet()): this
    //#output(void org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet()): this.context
    //#post(void org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet()): this.context == null

    private static Log log = LogFactory.getLog(PreviewThemeImageServlet.class);
    //#PreviewThemeImageServlet.java:46: method: org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet.org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet__static_init
    //#PreviewThemeImageServlet.java:46: Warning: method not available
    //#    -- call on Log org.apache.commons.logging.LogFactory:getLog(Class)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet
    //#    method: org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet__static_init
    //#    unanalyzed callee: Log org.apache.commons.logging.LogFactory:getLog(Class)
    //#output(org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet__static_init): __Descendant_Table[org/apache/roller/weblogger/ui/rendering/servlets/PreviewThemeImageServlet]
    //#output(org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet__static_init): __Dispatch_Table.doGet(Ljavax/servlet/http/HttpServletRequest;Ljavax/servlet/http/HttpServletResponse;)V
    //#output(org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet__static_init): __Dispatch_Table.init(Ljavax/servlet/ServletConfig;)V
    //#output(org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet__static_init): log
    //#post(org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet__static_init): __Descendant_Table[org/apache/roller/weblogger/ui/rendering/servlets/PreviewThemeImageServlet] == &__Dispatch_Table
    //#post(org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet__static_init): __Dispatch_Table.doGet(Ljavax/servlet/http/HttpServletRequest;Ljavax/servlet/http/HttpServletResponse;)V == &doGet
    //#post(org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet__static_init): __Dispatch_Table.init(Ljavax/servlet/ServletConfig;)V == &init
    //#post(org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet__static_init): init'ed(log)
    //#PreviewThemeImageServlet.java:46: end of method: org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet.org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet__static_init
    
    private ServletContext context = null;
    //#PreviewThemeImageServlet.java:48: end of method: void org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet.org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet()


    public void init(ServletConfig config) throws ServletException {

        super.init(config);
    //#PreviewThemeImageServlet.java:53: method: void org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet.init(ServletConfig)
    //#input(void init(ServletConfig)): config
    //#input(void init(ServletConfig)): log
    //#input(void init(ServletConfig)): this
    //#output(void init(ServletConfig)): this.context
    //#pre[1] (void init(ServletConfig)): config != null
    //#pre[2] (void init(ServletConfig)): log != null
    //#post(void init(ServletConfig)): init'ed(this.context)

        log.info("Initializing PreviewThemeImageServlet");
    //#PreviewThemeImageServlet.java:55: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:info(Object)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet
    //#    method: void init(ServletConfig)
    //#    unanalyzed callee: void org.apache.commons.logging.Log:info(Object)
        
        this.context = config.getServletContext();
    }
    //#PreviewThemeImageServlet.java:58: end of method: void org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet.init(ServletConfig)


    /**
     * Handles requests for user uploaded resources.
     */
    public void doGet(HttpServletRequest request, HttpServletResponse response)
            throws ServletException, IOException {
        
        String theme = request.getParameter("theme");
    //#PreviewThemeImageServlet.java:67: method: void org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet.doGet(HttpServletRequest, HttpServletResponse)
    //#input(void doGet(HttpServletRequest, HttpServletResponse)): "NOT MODIFIED "._tainted
    //#input(void doGet(HttpServletRequest, HttpServletResponse)): "Theme requested ["._tainted
    //#input(void doGet(HttpServletRequest, HttpServletResponse)): "Unable to get theme preview for theme - "._tainted
    //#input(void doGet(HttpServletRequest, HttpServletResponse)): "]"._tainted
    //#input(void doGet(HttpServletRequest, HttpServletResponse)): "last mod date (trucated to seconds) = "._tainted
    //#input(void doGet(HttpServletRequest, HttpServletResponse)): "since date = "._tainted
    //#input(void doGet(HttpServletRequest, HttpServletResponse)): log
    //#input(void doGet(HttpServletRequest, HttpServletResponse)): org/apache/roller/weblogger/ui/rendering/util/ModDateHeaderUtil.log
    //#input(void doGet(HttpServletRequest, HttpServletResponse)): request
    //#input(void doGet(HttpServletRequest, HttpServletResponse)): response
    //#input(void doGet(HttpServletRequest, HttpServletResponse)): this
    //#input(void doGet(HttpServletRequest, HttpServletResponse)): this.context
    //#pre[1] (void doGet(HttpServletRequest, HttpServletResponse)): log != null
    //#pre[2] (void doGet(HttpServletRequest, HttpServletResponse)): request != null
    //#pre[3] (void doGet(HttpServletRequest, HttpServletResponse)): (soft) response != null
    //#pre[5] (void doGet(HttpServletRequest, HttpServletResponse)): (soft) this.context != null
    //#presumption(void doGet(HttpServletRequest, HttpServletResponse)): javax.servlet.http.HttpServletResponse:getOutputStream(...)@116 != null
    //#presumption(void doGet(HttpServletRequest, HttpServletResponse)): org.apache.roller.weblogger.business.Weblogger:getThemeManager(...)@77 != null
    //#presumption(void doGet(HttpServletRequest, HttpServletResponse)): org.apache.roller.weblogger.business.WebloggerFactory:getWeblogger(...)@77 != null
    //#presumption(void doGet(HttpServletRequest, HttpServletResponse)): org.apache.roller.weblogger.business.themes.ThemeManager:getTheme(...)@78 != null
    //#unanalyzed(void doGet(HttpServletRequest, HttpServletResponse)): Effects-of-calling:javax.servlet.http.HttpServletRequest:getDateHeader
    //#unanalyzed(void doGet(HttpServletRequest, HttpServletResponse)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(void doGet(HttpServletRequest, HttpServletResponse)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(void doGet(HttpServletRequest, HttpServletResponse)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(void doGet(HttpServletRequest, HttpServletResponse)): Effects-of-calling:org.apache.commons.logging.Log:debug
    //#unanalyzed(void doGet(HttpServletRequest, HttpServletResponse)): Effects-of-calling:javax.servlet.http.HttpServletRequest:getRequestURL
    //#unanalyzed(void doGet(HttpServletRequest, HttpServletResponse)): Effects-of-calling:javax.servlet.http.HttpServletResponse:setStatus
    //#unanalyzed(void doGet(HttpServletRequest, HttpServletResponse)): Effects-of-calling:java.lang.Throwable:__curr_excep_obj
    //#unanalyzed(void doGet(HttpServletRequest, HttpServletResponse)): Effects-of-calling:javax.servlet.http.HttpServletResponse:setDateHeader
    //#test_vector(void doGet(HttpServletRequest, HttpServletResponse)): java.io.InputStream:read(...)@117: {-2_147_483_648..0}, {1..4_294_967_295}
    //#test_vector(void doGet(HttpServletRequest, HttpServletResponse)): org.apache.roller.weblogger.business.themes.SharedTheme:getPreviewImage(...)@79: Addr_Set{null}, Inverse{null}
        
        log.debug("Theme requested ["+theme+"]");
    //#PreviewThemeImageServlet.java:69: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:debug(Object)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet
    //#    method: void doGet(HttpServletRequest, HttpServletResponse)
    //#    unanalyzed callee: void org.apache.commons.logging.Log:debug(Object)
        
        long resourceLastMod = 0;
        InputStream resourceStream = null;
        String previewImagePath = null;
        
        // try looking up selected theme
        try {
            ThemeManager tmgr = WebloggerFactory.getWeblogger().getThemeManager();
    //#PreviewThemeImageServlet.java:77: Warning: method not available
    //#    -- call on Weblogger org.apache.roller.weblogger.business.WebloggerFactory:getWeblogger()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet
    //#    method: void doGet(HttpServletRequest, HttpServletResponse)
    //#    unanalyzed callee: Weblogger org.apache.roller.weblogger.business.WebloggerFactory:getWeblogger()
    //#PreviewThemeImageServlet.java:77: Warning: method not available
    //#    -- call on ThemeManager org.apache.roller.weblogger.business.Weblogger:getThemeManager()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet
    //#    method: void doGet(HttpServletRequest, HttpServletResponse)
    //#    unanalyzed callee: ThemeManager org.apache.roller.weblogger.business.Weblogger:getThemeManager()
            SharedTheme previewTheme = tmgr.getTheme(theme);
    //#PreviewThemeImageServlet.java:78: Warning: method not available
    //#    -- call on SharedTheme org.apache.roller.weblogger.business.themes.ThemeManager:getTheme(String)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet
    //#    method: void doGet(HttpServletRequest, HttpServletResponse)
    //#    unanalyzed callee: SharedTheme org.apache.roller.weblogger.business.themes.ThemeManager:getTheme(String)
            ThemeResource previewImage = previewTheme.getPreviewImage();
    //#PreviewThemeImageServlet.java:79: Warning: method not available
    //#    -- call on ThemeResource org.apache.roller.weblogger.business.themes.SharedTheme:getPreviewImage()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet
    //#    method: void doGet(HttpServletRequest, HttpServletResponse)
    //#    unanalyzed callee: ThemeResource org.apache.roller.weblogger.business.themes.SharedTheme:getPreviewImage()
            if(previewImage != null) {
                previewImagePath = previewImage.getPath();
    //#PreviewThemeImageServlet.java:81: Warning: method not available
    //#    -- call on String org.apache.roller.weblogger.pojos.ThemeResource:getPath()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet
    //#    method: void doGet(HttpServletRequest, HttpServletResponse)
    //#    unanalyzed callee: String org.apache.roller.weblogger.pojos.ThemeResource:getPath()
                resourceLastMod = previewImage.getLastModified();
    //#PreviewThemeImageServlet.java:82: Warning: method not available
    //#    -- call on long org.apache.roller.weblogger.pojos.ThemeResource:getLastModified()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet
    //#    method: void doGet(HttpServletRequest, HttpServletResponse)
    //#    unanalyzed callee: long org.apache.roller.weblogger.pojos.ThemeResource:getLastModified()
                resourceStream = previewImage.getInputStream();
    //#PreviewThemeImageServlet.java:83: Warning: method not available
    //#    -- call on InputStream org.apache.roller.weblogger.pojos.ThemeResource:getInputStream()
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet
    //#    method: void doGet(HttpServletRequest, HttpServletResponse)
    //#    unanalyzed callee: InputStream org.apache.roller.weblogger.pojos.ThemeResource:getInputStream()
            }
        } catch (Exception ex) {
            log.debug("error looking up preview image", ex);
    //#PreviewThemeImageServlet.java:86: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:debug(Object, Throwable)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet
    //#    method: void doGet(HttpServletRequest, HttpServletResponse)
    //#    unanalyzed callee: void org.apache.commons.logging.Log:debug(Object, Throwable)
            response.sendError(HttpServletResponse.SC_NOT_FOUND);
            return;
        }
        
        // if we don't have a stream to the file then we can't continue
        if(resourceStream == null) {
            log.debug("Unable to get theme preview for theme - "+theme);
    //#PreviewThemeImageServlet.java:93: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:debug(Object)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet
    //#    method: void doGet(HttpServletRequest, HttpServletResponse)
    //#    unanalyzed callee: void org.apache.commons.logging.Log:debug(Object)
            response.sendError(HttpServletResponse.SC_NOT_FOUND);
            return;
        }
        
        // Respond with 304 Not Modified if it is not modified.
        if (ModDateHeaderUtil.respondIfNotModified(request, response, resourceLastMod)) {
    //#PreviewThemeImageServlet.java:99: ?precondition failure
    //#    org/apache/roller/weblogger/ui/rendering/util/ModDateHeaderUtil.respondIfNotModified: (soft) lastModifiedTimeMillis%1_000 - lastModifiedTimeMillis in -18_446_744_073_709_551_615..9_223_372_036_854_775_808
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet
    //#    method: void doGet(HttpServletRequest, HttpServletResponse)
    //#    basic block: bb_8
    //#    assertion: (soft) resourceLastMod - resourceLastMod%1_000 in -9_223_372_036_854_775_808..18_446_744_073_709_551_615
    //#    callee: bool org/apache/roller/weblogger/ui/rendering/util/ModDateHeaderUtil.respondIfNotModified(HttpServletRequest, HttpServletResponse, long)
    //#    callee assertion: (soft) lastModifiedTimeMillis%1_000 - lastModifiedTimeMillis in -18_446_744_073_709_551_615..9_223_372_036_854_775_808
    //#    callee file: ModDateHeaderUtil.java
    //#    callee precondition index: [3]
    //#    callee srcpos: 53
    //#    VN: -(resourceLastMod - resourceLastMod%1_000)
    //#    Expected: {-18_446_744_073_709_551_615..9_223_372_036_854_775_808}
    //#    Bad: {-18_446_744_073_709_552_614..-18_446_744_073_709_551_616, 9_223_372_036_854_775_809..9_223_372_036_854_776_807}
    //#    Attribs:  Int  Soft  Bad < Exp  Bad > Exp
            return;
        } else {
            // set last-modified date
            ModDateHeaderUtil.setLastModifiedHeader(response, resourceLastMod);
        }
        
        log.debug("Everything is cool, sending image");
    //#PreviewThemeImageServlet.java:106: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:debug(Object)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet
    //#    method: void doGet(HttpServletRequest, HttpServletResponse)
    //#    unanalyzed callee: void org.apache.commons.logging.Log:debug(Object)
        
        // set the content type based on whatever is in our web.xml mime defs
        response.setContentType(this.context.getMimeType(previewImagePath));
        
        OutputStream out = null;
    //#PreviewThemeImageServlet.java:111: Warning: unused assignment
    //#    unused assignment into out
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet
    //#    method: void doGet(HttpServletRequest, HttpServletResponse)
    //#    Attribs:  Uncertain
        try {
            // ok, lets serve up the file
            byte[] buf = new byte[8192];
            int length = 0;
    //#PreviewThemeImageServlet.java:115: Warning: unused assignment
    //#    unused assignment into length
    //#    severity: SUPPRESSED
    //#    class: org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet
    //#    method: void doGet(HttpServletRequest, HttpServletResponse)
    //#    Attribs:  Uncertain
            out = response.getOutputStream();
            while((length = resourceStream.read(buf)) > 0) {
                out.write(buf, 0, length);
            }
            
            // cleanup
            out.close();
            resourceStream.close();
            
        } catch (Exception ex) {
            log.error("Error writing resource file", ex);
    //#PreviewThemeImageServlet.java:126: Warning: method not available
    //#    -- call on void org.apache.commons.logging.Log:error(Object, Throwable)
    //#    severity: INFORMATIONAL
    //#    class: org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet
    //#    method: void doGet(HttpServletRequest, HttpServletResponse)
    //#    unanalyzed callee: void org.apache.commons.logging.Log:error(Object, Throwable)
            if(!response.isCommitted()) {
                response.reset();
                response.sendError(HttpServletResponse.SC_INTERNAL_SERVER_ERROR);
            }
        }

    }
    //#PreviewThemeImageServlet.java:133: end of method: void org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet.doGet(HttpServletRequest, HttpServletResponse)

}
    //#PreviewThemeImageServlet.java:: end of class: org.apache.roller.weblogger.ui.rendering.servlets.PreviewThemeImageServlet
